:: Ternary Fields :: by Micha{\l} Muzalewski and Wojciech Skaba :: :: Received October 15, 1990 :: Copyright (c) 1990-2021 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; 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; 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 :: ALGSTR_3:def 1 (the TernOp of F).(a,b,c); 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 :: ALGSTR_3:def 2 for a,b,c being Real holds it.(a,b,c) = a*b + c; 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 :: ALGSTR_3:def 3 TernaryFieldStr (# REAL,In(0,REAL),In(1,REAL), ternaryreal #); end; registration cluster TernaryFieldEx -> non 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); end; theorem :: ALGSTR_3:1 for u,u9,v,v9 being Real holds u <> u9 implies ex x being Real st u*x+v = u9*x+v9; theorem :: ALGSTR_3:2 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; theorem :: ALGSTR_3:3 1 = 1.TernaryFieldEx; definition let IT be non empty TernaryFieldStr; attr IT is Ternary-Field-like means :: 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 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; 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 :: ALGSTR_3:4 a<>a9 & Tern(u,a,v) = Tern(u9,a,v9) & Tern(u,a9,v) = Tern(u9,a9,v9) implies u=u9 & v=v9; theorem :: ALGSTR_3:5 a<>0.F implies for b,c ex x st Tern(a,x,b) = c; theorem :: ALGSTR_3:6 a<>0.F & Tern(a,x,b) = Tern(a,x9,b) implies x=x9; theorem :: ALGSTR_3:7 a<>0.F implies for b,c ex x st Tern(x,a,b) = c; theorem :: ALGSTR_3:8 a<>0.F & Tern(x,a,b) = Tern(x9,a,b) implies x=x9;