Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Ternary Fields

by
Michal Muzalewski, and
Wojciech Skaba

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';
```