:: 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;