Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Ternary Fields

**by****Michal Muzalewski, and****Wojciech Skaba**- Received October 15, 1990
- MML identifier: ALGSTR_3

- [ Mizar article, MML identifier index ]

environ vocabulary VECTSP_1, MULTOP_1, FUNCT_1, ARYTM_1, RLVECT_1, ARYTM_3, ALGSTR_3; notation XBOOLE_0, SUBSET_1, NUMBERS, STRUCT_0, RLVECT_1, REAL_1, MULTOP_1; constructors RLVECT_1, REAL_1, MULTOP_1, MEMBERED, XBOOLE_0; clusters STRUCT_0, MEMBERED, ZFMISC_1, XBOOLE_0; 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(ZeroStr) TernaryFieldStr (# carrier -> set, Zero, unity -> Element of the carrier, ternary -> TriOp of the carrier #); end; definition cluster non empty 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 ternary of F).(a,b,c); end; definition let F; canceled; func 1_ F -> Scalar of F equals :: ALGSTR_3:def 3 the unity of F; 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 4 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 5 TernaryFieldStr (# REAL, 0, 1, ternaryreal #); end; definition 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 6 (the ternary of TernaryFieldEx).(a,b,c); end; canceled 2; theorem :: ALGSTR_3:3 for u,u',v,v' being Real holds u <> u' implies ex x being Real st u*x+v = u'*x+v'; canceled; theorem :: ALGSTR_3:5 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:6 0 = 0.TernaryFieldEx; :: The 1 defined in TeranaryFieldEx structure is equal to :: the ordinary 1 of real numbers. theorem :: ALGSTR_3:7 1 = 1_ TernaryFieldEx; definition let IT be non empty TernaryFieldStr; attr IT is Ternary-Field-like means :: ALGSTR_3:def 7 (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; definition cluster strict Ternary-Field-like (non empty TernaryFieldStr); 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 :: ALGSTR_3:8 a<>a' & Tern(u,a,v) = Tern(u',a,v') & Tern(u,a',v) = Tern(u',a',v') implies u=u' & v=v'; canceled 2; theorem :: ALGSTR_3:11 a<>0.F implies for b,c ex x st Tern(a,x,b) = c; theorem :: ALGSTR_3:12 a<>0.F & Tern(a,x,b) = Tern(a,x',b) implies x=x'; theorem :: ALGSTR_3:13 a<>0.F implies for b,c ex x st Tern(x,a,b) = c; theorem :: ALGSTR_3:14 a<>0.F & Tern(x,a,b) = Tern(x',a,b) implies x=x';

Back to top