:: Ternary Fields :: by Micha{\l} Muzalewski and Wojciech Skaba :: :: Received October 15, 1990 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies STRUCT_0, SUBSET_1, MULTOP_1, XBOOLE_0, VECTSP_1, FUNCT_1, NUMBERS, REAL_1, RELAT_1, ARYTM_3, CARD_1, ARYTM_1, MESFUNC1, SUPINF_2, ALGSTR_3, FUNCT_7; notations XBOOLE_0, SUBSET_1, FUNCT_7, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, STRUCT_0, REAL_1, MULTOP_1; constructors REAL_1, MEMBERED, MULTOP_1, RLVECT_1, FUNCT_7; registrations NUMBERS, MEMBERED, STRUCT_0, XREAL_0, RELSET_1; requirements NUMERALS, SUBSET, ARITHM, BOOLE; definitions STRUCT_0; equalities STRUCT_0; theorems MULTOP_1, XCMPLX_1, XREAL_0; 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 for TernaryFieldStr; existence proof set A = the non empty set,Z = the Element of A,t = the TriOp of A; take TernaryFieldStr(#A,Z,Z,t#); thus the carrier of TernaryFieldStr(#A,Z,Z,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 func ternaryreal -> TriOp of REAL means :Def2: for a,b,c being Real holds it.(a,b,c) = a*b + c; existence proof deffunc F(Real,Real,Real) = In(\$1*\$2 + \$3,REAL); consider X being TriOp of REAL such that A1: for a,b,c being Element of REAL holds X.(a,b,c) = F(a,b,c) from MULTOP_1:sch 4; take X; let a,b,c be Real; reconsider a,b,c as Element of REAL by XREAL_0:def 1; X.(a,b,c) = F(a,b,c) by A1; hence thesis; end; uniqueness proof let o1,o2 be TriOp of REAL; assume that A2: for a,b,c being Real holds o1.(a,b,c) = a*b + c and A3: for a,b,c being Real holds o2.(a,b,c) = a*b + c; for a,b,c being Element of REAL holds o1.(a,b,c) = o2.(a,b,c) proof let a,b,c be Element of REAL; thus o1.(a,b,c) = a*b + c by A2 .= o2.(a,b,c) by A3; end; hence thesis by MULTOP_1:3; 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,In(0,REAL),In(1,REAL), ternaryreal #); correctness; end; registration cluster TernaryFieldEx -> non empty; coherence; 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; theorem Th1: for u,u9,v,v9 being Real holds u <> u9 implies ex x being Real st u*x+v = u9*x+v9 proof let u,u9,v,v9 be Real; set x = (v9 - v)/(u - u9); assume u <> u9; then u - u9 <> 0; then A1: (u - u9)*x = v9 - v by XCMPLX_1:87; reconsider x as Real; take x; thus thesis by A1; end; 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 Def2; :: The 1 defined in TeranaryFieldEx structure is equal to :: the ordinary 1 of real numbers. reconsider jj=1, zz=0 as Real; 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*jj + zz by Def2 .= 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) = ternaryreal.(jj, x, zz) .= x*1 + 0 by Def2 .= 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 Def2 .= 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 Def2 .= 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 Element of REAL by XREAL_0:def 1; reconsider v=t as Scalar of TernaryFieldEx; take v; y = z*x + t; hence thesis by Def2; end; Lm6: for u,a,v,v9 being Scalar of TernaryFieldEx holds Tern(u,a,v) = Tern(u,a, v9) implies v = v9 proof let u,a,v,v9 be Scalar of TernaryFieldEx; reconsider z=u, x=a, y=v, y9=v9 as Real; Tern(u, a, v) = z*x + y & Tern(u, a, v9) = z*x + y9 by Def2; hence thesis; end; Lm7: for a,a9 being Scalar of TernaryFieldEx holds a <> a9 implies for b,b9 being Scalar of TernaryFieldEx ex u,v being Scalar of TernaryFieldEx st Tern(u, a,v) = b & Tern(u,a9,v) = b9 proof let a, a9 be Scalar of TernaryFieldEx; assume A1: a<>a9; let b, b9 be Scalar of TernaryFieldEx; reconsider x=a, x9=a9, y=b, y9=b9 as Real; A2: x9-x <> 0 by A1; set s = (y9-y)/(x9-x); set t = y - x*s; reconsider u=s, v=t as Scalar of TernaryFieldEx by XREAL_0:def 1; take u,v; thus Tern(u,a,v) = s*x + ((-s*x) + y) by Def2 .= b; thus Tern(u,a9,v) = ((y9-y)/(x9-x))*x9 + ((- x*((y9-y)/(x9-x))) + y) by Def2 .= (((y9-y)/(x9-x))*(x9-x)) + y .= y9-y + y by A2,XCMPLX_1:87 .= b9; end; Lm8: for u,u9 being Scalar of TernaryFieldEx holds u <> u9 implies for v,v9 being Scalar of TernaryFieldEx ex a being Scalar of TernaryFieldEx st Tern(u,a, v) = Tern(u9,a,v9) proof let u,u9 be Scalar of TernaryFieldEx; assume A1: u <> u9; let v,v9 be Scalar of TernaryFieldEx; reconsider uu = u, uu9 = u9, vv = v, vv9 = v9 as Real; consider aa being Real such that A2: uu*aa+vv = uu9*aa+vv9 by A1,Th1; reconsider a = aa as Scalar of TernaryFieldEx by XREAL_0:def 1; Tern(u,a,v) = uu*aa+vv & Tern(u9,a,v9) = uu9*aa+vv9 by Def2; hence thesis by A2; end; Lm9: for a,a9,u,u9,v,v9 being Scalar of TernaryFieldEx holds Tern(u,a, v) = Tern(u9,a, v9) & Tern(u,a9,v) = Tern(u9,a9,v9) implies a = a9 or u = u9 proof let a,a9,u,u9,v,v9 be Scalar of TernaryFieldEx; assume A1: Tern(u,a, v) = Tern(u9,a, v9) & Tern(u,a9,v) = Tern(u9,a9,v9); reconsider aa=a,aa9=a9,uu=u,uu9=u9,vv=v,vv9=v9 as Real; A2: Tern(u,a9,v) = uu*aa9 + vv & Tern(u9,a9,v9) = uu9*aa9 + vv9 by Def2; Tern(u,a, v) = uu*aa + vv & Tern(u9,a, v9) = uu9*aa + vv9 by Def2; then uu*(aa - aa9) = uu9*(aa - aa9) by A1,A2; then uu = uu9 or aa - aa9 = 0 by XCMPLX_1:5; hence thesis; end; definition let IT be non empty TernaryFieldStr; attr IT is Ternary-Field-like means :Def5: 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,v9 being Scalar of IT holds Tern(u,a,v) = Tern(u,a,v9) implies v = v9) & (for a,a9 being Scalar of IT holds a <> a9 implies for b,b9 being Scalar of IT ex u,v being Scalar of IT st Tern(u,a,v) = b & Tern(u,a9,v) = b9) & (for u,u9 being Scalar of IT holds u <> u9 implies for v,v9 being Scalar of IT ex a being Scalar of IT st Tern(u,a,v) = Tern(u9,a,v9)) & for a,a9,u,u9,v,v9 being Scalar of IT holds Tern(u,a,v) = Tern(u9,a,v9) & Tern(u,a9,v) = Tern(u9,a9,v9) implies a = a9 or u = u9; end; registration cluster strict Ternary-Field-like for non empty TernaryFieldStr; existence by Def5,Lm1,Lm2,Lm3,Lm4,Lm5,Lm6,Lm7,Lm8,Lm9; end; definition mode Ternary-Field is Ternary-Field-like non empty TernaryFieldStr; end; reserve F for Ternary-Field; reserve a,a9,b,c,x,x9,u,u9,v,v9,z for Scalar of F; theorem a<>a9 & Tern(u,a,v) = Tern(u9,a,v9) & Tern(u,a9,v) = Tern(u9,a9,v9) implies u=u9 & v=v9 proof assume that A1: a<>a9 and A2: Tern(u,a,v) = Tern(u9,a,v9) and A3: Tern(u,a9,v) = Tern(u9,a9,v9); u = u9 by A1,A2,A3,Def5; hence thesis by A2,Def5; end; 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,Def5; take x; thus thesis by A2,Def5; end; theorem a<>0.F & Tern(a,x,b) = Tern(a,x9,b) implies x=x9 proof assume that A1: a<>0.F and A2: Tern(a,x,b) = Tern(a,x9,b); set c = Tern(a,x,b); A3: Tern(a,x,b) = Tern(0.F,x,c) by Def5; Tern(a,x9,b) = Tern(0.F,x9,c) by A2,Def5; hence thesis by A1,A3,Def5; 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,Def5; take x; thus thesis by A2,Def5; end; theorem a<>0.F & Tern(x,a,b) = Tern(x9,a,b) implies x=x9 proof assume A1: a<>0.F & Tern(x,a,b) = Tern(x9,a,b); Tern(x,0.F,b) = b & Tern(x9,0.F,b) = b by Def5; hence thesis by A1,Def5; end;