:: Ternary Fields
::  by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received October 15, 1990
:: Copyright (c) 1990 Association of Mizar Users

environ

 vocabularies VECTSP_1, MULTOP_1, FUNCT_1, ARYTM_1, RLVECT_1, ARYTM_3,
      ALGSTR_3, STRUCT_0, GROUP_1, ARYTM;
 notations XBOOLE_0, SUBSET_1, NUMBERS, STRUCT_0, REAL_1, MULTOP_1;
 constructors REAL_1, MEMBERED, MULTOP_1, RLVECT_1;
 registrations NUMBERS, MEMBERED, STRUCT_0;
 requirements NUMERALS, SUBSET, ARITHM, BOOLE;
 definitions STRUCT_0;
 theorems MULTOP_1, XCMPLX_1;
 schemes MULTOP_1;

begin

:: TERNARY FIELDS
:: This few lines define the basic algebraic structure (F, 0, 1, T)
:: used in the whole article.

definition
  struct(ZeroOneStr) TernaryFieldStr (# carrier -> set,
    ZeroF, OneF -> Element of the carrier, TernOp -> TriOp of the carrier #);
end;

registration
  cluster non empty TernaryFieldStr;
  existence
  proof
    consider A being non empty set, Z,u being Element of A,
    t being TriOp of A;
    take TernaryFieldStr(#A,Z,u,t#);
    thus the carrier of TernaryFieldStr(#A,Z,u,t#) is non empty;
  end;
end;

reserve F for non empty TernaryFieldStr;

:: The following definitions let us simplify the notation

definition
  let F;
  mode Scalar of F is Element of F;
end;

reserve a,b,c for Scalar of F;

definition
  let F,a,b,c;
  func Tern(a,b,c) -> Scalar of F equals

  (the TernOp of F).(a,b,c);
  correctness;
end;

:: The following definition specifies a ternary operation that
:: will be used in the forthcoming example: TernaryFieldEx
:: as its TriOp function.

definition
  canceled 2;
  func ternaryreal -> TriOp of REAL means
  :Def4:
  for a,b,c being Real holds it.(a,b,c) = a*b + c;
  existence
  proof
    deffunc F(Real,Real,Real) = $1*$2 + $3;
    ex X being TriOp of REAL st
    for a,b,c being Real holds X.(a,b,c) = F(a,b,c) from MULTOP_1:sch 4;
    hence thesis;
  end;
  uniqueness
  proof
    let o1,o2 be TriOp of REAL;
    assume that
A1: for a,b,c being Real holds o1.(a,b,c) = a*b + c and
A2: for a,b,c being Real holds o2.(a,b,c) = a*b + c;
    for a,b,c being Real holds o1.(a,b,c) = o2.(a,b,c)
    proof
      let a,b,c be Real;
      thus o1.(a,b,c) = a*b + c by A1
        .= o2.(a,b,c) by A2;
    end;
    hence o1 = o2 by MULTOP_1:4;
  end;
end;

:: Now comes the definition of example structure called: TernaryFieldEx.
:: This example will be used to prove the existence of the Ternary-Field mode.

definition
  func TernaryFieldEx -> strict TernaryFieldStr equals
  TernaryFieldStr (# REAL, 0, 1, ternaryreal #);
  correctness;
end;

registration
  cluster TernaryFieldEx -> non empty;
  coherence
  proof
    thus the carrier of TernaryFieldEx is non empty;
  end;
end;

:: On the contrary to the Tern() (starting with uppercase), this definition
:: allows for the use of the currently specified example ternary field.

definition
  let a,b,c be Scalar of TernaryFieldEx;
  func tern(a,b,c) -> Scalar of TernaryFieldEx equals
  (the TernOp of TernaryFieldEx).(a,b,c);
  correctness;
end;

canceled 2;

theorem Th3:
  for u,u',v,v' being Real holds
  u <> u' implies ex x being Real st u*x+v = u'*x+v'
proof
  let u,u',v,v' be Real;
  assume
A1: u <> u';
  set x = (v' - v)/(u - u');
  u - u' <> 0 by A1;
  then
A2: (u - u')*x = v' - v by XCMPLX_1:88;
  reconsider x as Real;
  take x;
  thus thesis by A2;
end;

canceled;

theorem
  for u,a,v being Scalar of TernaryFieldEx for z,x,y being Real holds
  u=z & a=x & v=y implies Tern(u,a,v) = z*x + y by Def4;

:: The 1 defined in TeranaryFieldEx structure is equal to
:: the ordinary 1 of real numbers.

canceled;

theorem
  1 = 1.TernaryFieldEx;

Lm1: for a being Scalar of TernaryFieldEx holds
Tern(a, 1.TernaryFieldEx, 0.TernaryFieldEx) = a
proof
  let a be Scalar of TernaryFieldEx;
  reconsider x=a as Real;
  thus Tern(a, 1.TernaryFieldEx, 0.TernaryFieldEx) = x*1 + 0 by Def4
    .= a;
end;

Lm2: for a being Scalar of TernaryFieldEx holds
Tern(1.TernaryFieldEx, a, 0.TernaryFieldEx) = a
proof
  let a be Scalar of TernaryFieldEx;
  reconsider x=a as Real;
  thus Tern(1.TernaryFieldEx, a, 0.TernaryFieldEx) = x*1 + 0 by Def4
    .= a;
end;

Lm3: for a,b being Scalar of TernaryFieldEx holds
Tern(a, 0.TernaryFieldEx, b) = b
proof
  let a,b be Scalar of TernaryFieldEx;
  reconsider x=a, y=b as Real;
  thus Tern(a, 0.TernaryFieldEx, b) = x*0 + y by Def4
    .= b;
end;

Lm4: for a,b being Scalar of TernaryFieldEx holds
Tern(0.TernaryFieldEx, a, b) = b
proof
  let a,b be Scalar of TernaryFieldEx;
  reconsider x=a, y=b as Real;
  thus Tern(0.TernaryFieldEx, a, b) = 0*x + y by Def4
    .= b;
end;

Lm5: for u,a,b being Scalar of TernaryFieldEx
ex v being Scalar of TernaryFieldEx st Tern(u,a,v) = b
proof
  let u,a,b be Scalar of TernaryFieldEx;
  reconsider z=u, x=a, y=b as Real;
  reconsider t = y - z*x as Real;
A1: y = z*x + t;
  reconsider v=t as Scalar of TernaryFieldEx;
  take v;
  thus Tern(u, a, v) = b by A1,Def4;
end;

Lm6: for u,a,v,v' being Scalar of TernaryFieldEx holds
Tern(u,a,v) = Tern(u,a,v') implies v = v'
proof
  let u,a,v,v' be Scalar of TernaryFieldEx;
  reconsider z=u, x=a, y=v, y'=v' as Real;
A1: Tern(u, a, v) = z*x + y by Def4;
  Tern(u, a, v') = z*x + y' by Def4;
  hence thesis by A1;
end;

Lm7: for a,a' being Scalar of TernaryFieldEx holds a <> a' implies
for b,b' being Scalar of TernaryFieldEx
ex u,v being Scalar of TernaryFieldEx st Tern(u,a,v) = b & Tern(u,a',v) = b'
proof
  let a, a' be Scalar of TernaryFieldEx;
  assume
A1: a<>a';
  let b, b' be Scalar of TernaryFieldEx;
  reconsider x=a, x'=a', y=b, y'=b' as Real;
  set s = (y'-y)/(x'-x);
  set t = y - x*s;
  reconsider u=s, v=t as Scalar of TernaryFieldEx;
  take u,v;
  thus Tern(u,a,v) = s*x + ((-s*x) + y) by Def4
    .= b;
A2: x'-x <> 0 by A1;
  thus Tern(u,a',v) = ((y'-y)/(x'-x))*x' + ((- x*((y'-y)/(x'-x))) + y) by Def4
    .= (((y'-y)/(x'-x))*(x'-x)) + y
    .= y'-y + y by A2,XCMPLX_1:88
    .= b';
end;

Lm8: for u,u' being Scalar of TernaryFieldEx holds u <> u' implies
for v,v' being Scalar of TernaryFieldEx
ex a being Scalar of TernaryFieldEx st Tern(u,a,v) = Tern(u',a,v')
proof
  let u,u' be Scalar of TernaryFieldEx;
  assume
A1: u <> u';
  let v,v' be Scalar of TernaryFieldEx;
  reconsider uu = u, uu' = u', vv = v, vv' = v' as Real;
  consider aa being Real such that
A2: uu*aa+vv = uu'*aa+vv' by A1,Th3;
  reconsider a = aa as Scalar of TernaryFieldEx;
  Tern(u,a,v) = uu*aa+vv & Tern(u',a,v') = uu'*aa+vv' by Def4;
  hence thesis by A2;
end;

Lm9: for a,a',u,u',v,v' being Scalar of TernaryFieldEx holds
Tern(u,a, v) = Tern(u',a, v') & Tern(u,a',v) = Tern(u',a',v')
implies a = a' or u = u'
proof
  let a,a',u,u',v,v' be Scalar of TernaryFieldEx;
  assume that
A1: Tern(u,a, v) = Tern(u',a, v') and
A2: Tern(u,a',v) = Tern(u',a',v');
  reconsider aa=a,aa'=a',uu=u,uu'=u',vv=v,vv'=v' as Real;
  Tern(u,a, v) = uu*aa + vv & Tern(u',a, v') = uu'*aa + vv'
  & Tern(u,a',v) = uu*aa' + vv & Tern(u',a',v') = uu'*aa' + vv' by Def4;
  then uu*(aa - aa') = uu'*(aa - aa') by A1,A2;
  then uu = uu' or aa - aa' = 0 by XCMPLX_1:5;
  hence thesis;
end;

definition
  let IT be non empty TernaryFieldStr;
  attr IT is Ternary-Field-like means
  :Def7:
  (0.IT <> 1.IT)
  & (for a being Scalar of IT holds Tern(a, 1.IT, 0.IT) = a)
  & (for a being Scalar of IT holds Tern(1.IT, a, 0.IT) = a)
  & (for a,b being Scalar of IT holds Tern(a, 0.IT, b ) = b)
  & (for a,b being Scalar of IT holds Tern(0.IT, a, b ) = b)
  & (for u,a,b being Scalar of IT ex v being Scalar of IT st Tern(u,a,v) = b)
  & (for u,a,v,v' being Scalar of IT holds Tern(u,a,v) = Tern(u,a,v')
  implies v = v') & (for a,a' being Scalar of IT holds a <> a' implies
  for b,b' being Scalar of IT ex u,v being Scalar of IT st
  Tern(u,a,v) = b & Tern(u,a',v) = b') & (for u,u' being Scalar of IT holds
  u <> u' implies for v,v' being Scalar of IT ex a being Scalar of IT st
  Tern(u,a,v) = Tern(u',a,v')) & (for a,a',u,u',v,v' being Scalar of IT holds
  Tern(u,a,v) = Tern(u',a,v') & Tern(u,a',v) = Tern(u',a',v')
  implies a = a' or u = u');
end;

registration
  cluster strict Ternary-Field-like (non empty TernaryFieldStr);
  existence
  proof
    TernaryFieldEx is Ternary-Field-like
    by Def7,Lm1,Lm2,Lm3,Lm4,Lm5,Lm6,Lm7,Lm8,Lm9;
    hence thesis;
  end;
end;

definition
  mode Ternary-Field is Ternary-Field-like (non empty TernaryFieldStr);
end;

reserve F for Ternary-Field;
reserve a,a',b,c,x,x',u,u',v,v',z for Scalar of F;

theorem
  a<>a' & Tern(u,a,v) = Tern(u',a,v') & Tern(u,a',v) = Tern(u',a',v')
  implies u=u' & v=v'
proof
  assume that
A1: a<>a' and
A2: Tern(u,a,v) = Tern(u',a,v') and
A3: Tern(u,a',v) = Tern(u',a',v');
  u = u' by A1,A2,A3,Def7;
  hence thesis by A2,Def7;
end;

canceled 2;

theorem
  a<>0.F implies for b,c ex x st Tern(a,x,b) = c
proof
  assume
A1: a <> 0.F;
  let b,c;
  consider x such that
A2: Tern(a,x,b) = Tern(0.F,x,c) by A1,Def7;
  take x;
  thus thesis by A2,Def7;
end;

theorem
  a<>0.F & Tern(a,x,b) = Tern(a,x',b) implies x=x'
proof
  assume that
A1: a<>0.F and
A2: Tern(a,x,b) = Tern(a,x',b);
  set c = Tern(a,x,b);
  Tern(a,x,b) = Tern(0.F,x,c) & Tern(a,x',b) = Tern(0.F,x',c) by A2,Def7;
  hence thesis by A1,Def7;
end;

theorem
  a<>0.F implies for b,c ex x st Tern(x,a,b) = c
proof
  assume
A1: a <> 0.F;
  let b,c;
  consider x,z such that
A2: Tern(x,a,z) = c & Tern(x,0.F,z) = b by A1,Def7;
  take x;
  thus thesis by A2,Def7;
end;

theorem
  a<>0.F & Tern(x,a,b) = Tern(x',a,b) implies x=x'
proof
  assume
A1: a<>0.F & Tern(x,a,b) = Tern(x',a,b);
  Tern(x,0.F,b) = b & Tern(x',0.F,b) = b by Def7;
  hence thesis by A1,Def7;
end;