:: Ternary Fields :: by Micha{\l} Muzalewski and Wojciech Skaba :: :: Received October 15, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin :: TERNARY FIELDS :: This few lines define the basic algebraic structure (F, 0, 1, T) :: used in the whole article. definition attrc1 is strict ; struct TernaryFieldStr -> ZeroOneStr ; aggrTernaryFieldStr(# carrier, ZeroF, OneF, TernOp #) -> TernaryFieldStr ; sel TernOp c1 -> TriOp of the carrier of c1; end; registration cluster non empty for TernaryFieldStr ; existence not for b1 being TernaryFieldStr holds b1 is empty proofend; end; :: The following definitions let us simplify the notation definition let F be non empty TernaryFieldStr ; mode Scalar of F is Element of F; end; definition let F be non empty TernaryFieldStr ; let a, b, c be Scalar of F; func Tern (a,b,c) -> Scalar of F equals :: ALGSTR_3:def 1 the TernOp of F . (a,b,c); correctness coherence the TernOp of F . (a,b,c) is Scalar of F; ; end; :: deftheorem defines Tern ALGSTR_3:def_1_:_ for F being non empty TernaryFieldStr for a, b, c being Scalar of F holds Tern (a,b,c) = the TernOp of F . (a,b,c); :: 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: :: ALGSTR_3:def 2 for a, b, c being Real holds it . (a,b,c) = (a * b) + c; existence ex b1 being TriOp of REAL st for a, b, c being Real holds b1 . (a,b,c) = (a * b) + c proofend; uniqueness for b1, b2 being TriOp of REAL st ( for a, b, c being Real holds b1 . (a,b,c) = (a * b) + c ) & ( for a, b, c being Real holds b2 . (a,b,c) = (a * b) + c ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines ternaryreal ALGSTR_3:def_2_:_ for b1 being TriOp of REAL holds ( b1 = ternaryreal iff for a, b, c being Real holds b1 . (a,b,c) = (a * b) + c ); :: 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 :: ALGSTR_3:def 3 TernaryFieldStr(# REAL,0,1,ternaryreal #); correctness coherence TernaryFieldStr(# REAL,0,1,ternaryreal #) is strict TernaryFieldStr ; ; end; :: deftheorem defines TernaryFieldEx ALGSTR_3:def_3_:_ TernaryFieldEx = TernaryFieldStr(# REAL,0,1,ternaryreal #); registration cluster TernaryFieldEx -> non empty strict ; coherence not TernaryFieldEx is empty ; 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 :: ALGSTR_3:def 4 the TernOp of TernaryFieldEx . (a,b,c); correctness coherence the TernOp of TernaryFieldEx . (a,b,c) is Scalar of TernaryFieldEx; ; end; :: deftheorem defines tern ALGSTR_3:def_4_:_ for a, b, c being Scalar of TernaryFieldEx holds tern (a,b,c) = the TernOp of TernaryFieldEx . (a,b,c); theorem Th1: :: ALGSTR_3:1 for u, u9, v, v9 being Real st u <> u9 holds ex x being Real st (u * x) + v = (u9 * x) + v9 proofend; theorem :: ALGSTR_3:2 for u, a, v being Scalar of TernaryFieldEx for z, x, y being Real st u = z & a = x & v = y holds Tern (u,a,v) = (z * x) + y by Def2; :: The 1 defined in TeranaryFieldEx structure is equal to :: the ordinary 1 of real numbers. theorem :: ALGSTR_3:3 1 = 1. TernaryFieldEx ; Lm1: for a being Scalar of TernaryFieldEx holds Tern (a,(1. TernaryFieldEx),(0. TernaryFieldEx)) = a proofend; Lm2: for a being Scalar of TernaryFieldEx holds Tern ((1. TernaryFieldEx),a,(0. TernaryFieldEx)) = a proofend; Lm3: for a, b being Scalar of TernaryFieldEx holds Tern (a,(0. TernaryFieldEx),b) = b proofend; Lm4: for a, b being Scalar of TernaryFieldEx holds Tern ((0. TernaryFieldEx),a,b) = b proofend; Lm5: for u, a, b being Scalar of TernaryFieldEx ex v being Scalar of TernaryFieldEx st Tern (u,a,v) = b proofend; Lm6: for u, a, v, v9 being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u,a,v9) holds v = v9 proofend; Lm7: for a, a9 being Scalar of TernaryFieldEx st a <> a9 holds 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 ) proofend; Lm8: for u, u9 being Scalar of TernaryFieldEx st u <> u9 holds for v, v9 being Scalar of TernaryFieldEx ex a being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u9,a,v9) proofend; Lm9: for a, a9, u, u9, v, v9 being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) & not a = a9 holds u = u9 proofend; definition let IT be non empty TernaryFieldStr ; attrIT is Ternary-Field-like means :Def5: :: ALGSTR_3:def 5 ( 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 st Tern (u,a,v) = Tern (u,a,v9) holds v = v9 ) & ( for a, a9 being Scalar of IT st a <> a9 holds 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 st u <> u9 holds 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 st Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) & not a = a9 holds u = u9 ) ); end; :: deftheorem Def5 defines Ternary-Field-like ALGSTR_3:def_5_:_ for IT being non empty TernaryFieldStr holds ( IT is Ternary-Field-like iff ( 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 st Tern (u,a,v) = Tern (u,a,v9) holds v = v9 ) & ( for a, a9 being Scalar of IT st a <> a9 holds 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 st u <> u9 holds 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 st Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) & not a = a9 holds u = u9 ) ) ); registration cluster non empty strict Ternary-Field-like for TernaryFieldStr ; existence ex b1 being non empty TernaryFieldStr st ( b1 is strict & b1 is Ternary-Field-like ) proofend; end; definition mode Ternary-Field is non empty Ternary-Field-like TernaryFieldStr ; end; theorem :: ALGSTR_3:4 for F being Ternary-Field for a, a9, u, v, u9, v9 being Scalar of F st a <> a9 & Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) holds ( u = u9 & v = v9 ) proofend; theorem :: ALGSTR_3:5 for F being Ternary-Field for a being Scalar of F st a <> 0. F holds for b, c being Scalar of F ex x being Scalar of F st Tern (a,x,b) = c proofend; theorem :: ALGSTR_3:6 for F being Ternary-Field for a, x, b, x9 being Scalar of F st a <> 0. F & Tern (a,x,b) = Tern (a,x9,b) holds x = x9 proofend; theorem :: ALGSTR_3:7 for F being Ternary-Field for a being Scalar of F st a <> 0. F holds for b, c being Scalar of F ex x being Scalar of F st Tern (x,a,b) = c proofend; theorem :: ALGSTR_3:8 for F being Ternary-Field for a, x, b, x9 being Scalar of F st a <> 0. F & Tern (x,a,b) = Tern (x9,a,b) holds x = x9 proofend;