:: Ternary Fields
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received October 15, 1990
:: Copyright (c) 1990-2026 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;
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;