:: by Micha{\l} Muzalewski and Wojciech Skaba

::

:: Received October 15, 1990

:: Copyright (c) 1990-2016 Association of Mizar Users

definition

attr c_{1} is strict ;

struct TernaryFieldStr -> ZeroOneStr ;

aggr TernaryFieldStr(# carrier, ZeroF, OneF, TernOp #) -> TernaryFieldStr ;

sel TernOp c_{1} -> TriOp of the carrier of c_{1};

end;
struct TernaryFieldStr -> ZeroOneStr ;

aggr TernaryFieldStr(# carrier, ZeroF, OneF, TernOp #) -> TernaryFieldStr ;

sel TernOp c

:: The following definitions let us simplify the notation

definition

let F be non empty TernaryFieldStr ;

let a, b, c be Scalar of F;

correctness

coherence

the TernOp of F . (a,b,c) is Scalar of F;

;

end;
let a, b, c be Scalar of F;

correctness

coherence

the TernOp of F . (a,b,c) is Scalar of F;

;

:: deftheorem defines Tern ALGSTR_3:def 1 :

for F being non empty TernaryFieldStr

for a, b, c being Scalar of F holds Tern (a,b,c) = the TernOp of F . (a,b,c);

for F being non empty TernaryFieldStr

for a, b, c being Scalar of F holds Tern (a,b,c) = the TernOp of F . (a,b,c);

:: The following definition specifies a ternary operation that

:: will be used in the forthcoming example: TernaryFieldEx

:: as its TriOp function.

:: will be used in the forthcoming example: TernaryFieldEx

:: as its TriOp function.

definition

ex b_{1} being TriOp of REAL st

for a, b, c being Real holds b_{1} . (a,b,c) = (a * b) + c

for b_{1}, b_{2} being TriOp of REAL st ( for a, b, c being Real holds b_{1} . (a,b,c) = (a * b) + c ) & ( for a, b, c being Real holds b_{2} . (a,b,c) = (a * b) + c ) holds

b_{1} = b_{2}
end;

func ternaryreal -> TriOp of REAL means :Def2: :: ALGSTR_3:def 2

for a, b, c being Real holds it . (a,b,c) = (a * b) + c;

existence for a, b, c being Real holds it . (a,b,c) = (a * b) + c;

ex b

for a, b, c being Real holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines ternaryreal ALGSTR_3:def 2 :

for b_{1} being TriOp of REAL holds

( b_{1} = ternaryreal iff for a, b, c being Real holds b_{1} . (a,b,c) = (a * b) + c );

for b

( b

:: Now comes the definition of example structure called: TernaryFieldEx.

:: This example will be used to prove the existence of the Ternary-Field mode.

:: This example will be used to prove the existence of the Ternary-Field mode.

definition

coherence

TernaryFieldStr(# REAL,(In (0,REAL)),(In (1,REAL)),ternaryreal #) is strict TernaryFieldStr ;

;

end;

func TernaryFieldEx -> strict TernaryFieldStr equals :: ALGSTR_3:def 3

TernaryFieldStr(# REAL,(In (0,REAL)),(In (1,REAL)),ternaryreal #);

correctness TernaryFieldStr(# REAL,(In (0,REAL)),(In (1,REAL)),ternaryreal #);

coherence

TernaryFieldStr(# REAL,(In (0,REAL)),(In (1,REAL)),ternaryreal #) is strict TernaryFieldStr ;

;

:: deftheorem defines TernaryFieldEx ALGSTR_3:def 3 :

TernaryFieldEx = TernaryFieldStr(# REAL,(In (0,REAL)),(In (1,REAL)),ternaryreal #);

TernaryFieldEx = TernaryFieldStr(# REAL,(In (0,REAL)),(In (1,REAL)),ternaryreal #);

registration
end;

:: On the contrary to the Tern() (starting with uppercase), this definition

:: allows for the use of the currently specified example ternary field.

:: allows for the use of the currently specified example ternary field.

definition

let a, b, c be Scalar of TernaryFieldEx;

coherence

the TernOp of TernaryFieldEx . (a,b,c) is Scalar of TernaryFieldEx;

;

end;
func tern (a,b,c) -> Scalar of TernaryFieldEx equals :: ALGSTR_3:def 4

the TernOp of TernaryFieldEx . (a,b,c);

correctness the TernOp of TernaryFieldEx . (a,b,c);

coherence

the TernOp of TernaryFieldEx . (a,b,c) is Scalar of TernaryFieldEx;

;

:: deftheorem defines tern ALGSTR_3:def 4 :

for a, b, c being Scalar of TernaryFieldEx holds tern (a,b,c) = the TernOp of TernaryFieldEx . (a,b,c);

for a, b, c being Scalar of TernaryFieldEx holds tern (a,b,c) = the TernOp of TernaryFieldEx . (a,b,c);

theorem :: ALGSTR_3:2

reconsider jj = 1, zz = 0 as Real ;

Lm1: for a being Scalar of TernaryFieldEx holds Tern (a,(1. TernaryFieldEx),(0. TernaryFieldEx)) = a

proof end;

Lm2: for a being Scalar of TernaryFieldEx holds Tern ((1. TernaryFieldEx),a,(0. TernaryFieldEx)) = a

proof end;

Lm3: for a, b being Scalar of TernaryFieldEx holds Tern (a,(0. TernaryFieldEx),b) = b

proof end;

Lm4: for a, b being Scalar of TernaryFieldEx holds Tern ((0. TernaryFieldEx),a,b) = b

proof end;

Lm5: for u, a, b being Scalar of TernaryFieldEx ex v being Scalar of TernaryFieldEx st Tern (u,a,v) = b

proof end;

Lm6: for u, a, v, v9 being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u,a,v9) holds

v = v9

proof end;

Lm7: for a, a9 being Scalar of TernaryFieldEx st a <> a9 holds

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

Lm8: for u, u9 being Scalar of TernaryFieldEx st u <> u9 holds

for v, v9 being Scalar of TernaryFieldEx ex a being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u9,a,v9)

proof end;

Lm9: for a, a9, u, u9, v, v9 being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) & not a = a9 holds

u = u9

proof end;

definition

let IT be non empty TernaryFieldStr ;

end;
attr IT is Ternary-Field-like means :Def5: :: 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 st Tern (u,a,v) = Tern (u,a,v9) holds

v = v9 ) & ( for a, a9 being Scalar of IT st a <> a9 holds

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 st u <> u9 holds

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 st Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) & not a = a9 holds

u = u9 ) );

( 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 st Tern (u,a,v) = Tern (u,a,v9) holds

v = v9 ) & ( for a, a9 being Scalar of IT st a <> a9 holds

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 st u <> u9 holds

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 st Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) & not a = a9 holds

u = u9 ) );

:: deftheorem Def5 defines Ternary-Field-like ALGSTR_3:def 5 :

for IT being non empty TernaryFieldStr holds

( IT is Ternary-Field-like iff ( 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 st Tern (u,a,v) = Tern (u,a,v9) holds

v = v9 ) & ( for a, a9 being Scalar of IT st a <> a9 holds

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 st u <> u9 holds

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 st Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) & not a = a9 holds

u = u9 ) ) );

for IT being non empty TernaryFieldStr holds

( IT is Ternary-Field-like iff ( 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 st Tern (u,a,v) = Tern (u,a,v9) holds

v = v9 ) & ( for a, a9 being Scalar of IT st a <> a9 holds

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 st u <> u9 holds

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 st Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) & not a = a9 holds

u = u9 ) ) );

registration

existence

ex b_{1} being non empty TernaryFieldStr st

( b_{1} is strict & b_{1} is Ternary-Field-like )
by Def5, Lm1, Lm2, Lm3, Lm4, Lm5, Lm6, Lm7, Lm8, Lm9;

end;
ex b

( b

theorem :: ALGSTR_3:4

for F being Ternary-Field

for a, a9, u, u9, v, v9 being Scalar of F st a <> a9 & Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) holds

( u = u9 & v = v9 )

for a, a9, u, u9, v, v9 being Scalar of F st a <> a9 & Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) holds

( u = u9 & v = v9 )

proof end;

theorem :: ALGSTR_3:5

for F being Ternary-Field

for a being Scalar of F st a <> 0. F holds

for b, c being Scalar of F ex x being Scalar of F st Tern (a,x,b) = c

for a being Scalar of F st a <> 0. F holds

for b, c being Scalar of F ex x being Scalar of F st Tern (a,x,b) = c

proof end;

theorem :: ALGSTR_3:6

for F being Ternary-Field

for a, b, x, x9 being Scalar of F st a <> 0. F & Tern (a,x,b) = Tern (a,x9,b) holds

x = x9

for a, b, x, x9 being Scalar of F st a <> 0. F & Tern (a,x,b) = Tern (a,x9,b) holds

x = x9

proof end;

theorem :: ALGSTR_3:7

for F being Ternary-Field

for a being Scalar of F st a <> 0. F holds

for b, c being Scalar of F ex x being Scalar of F st Tern (x,a,b) = c

for a being Scalar of F st a <> 0. F holds

for b, c being Scalar of F ex x being Scalar of F st Tern (x,a,b) = c

proof end;

theorem :: ALGSTR_3:8

for F being Ternary-Field

for a, b, x, x9 being Scalar of F st a <> 0. F & Tern (x,a,b) = Tern (x9,a,b) holds

x = x9

for a, b, x, x9 being Scalar of F st a <> 0. F & Tern (x,a,b) = Tern (x9,a,b) holds

x = x9

proof end;

:: This few lines define the basic algebraic structure (F, 0, 1, T)

:: used in the whole article.