:: Ternary Fields
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received October 15, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

definition

attr c₁ is strict ;
struct TernaryFieldStr -> ZeroOneStr ;
aggr TernaryFieldStr(# carrier, ZeroF, OneF, TernOp #) -> TernaryFieldStr ;
sel TernOp c₁ -> TriOp of the carrier of c₁;

end;

registration

cluster non empty TernaryFieldStr ;
existence
not for b₁ being TernaryFieldStr holds b₁ is empty

proof end;

end;

definition

let F be non empty TernaryFieldStr ;
mode Scalar of F is Element of F;

end;

definition

let F be non empty TernaryFieldStr ;
let a, b, c be Scalar of F;
func Tern (a,b,c) -> Scalar of F equals :: ALGSTR_3:def 1
the TernOp of F . (a,b,c);
correctness
coherence
the TernOp of F . (a,b,c) is Scalar of F;
;

end;

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

definition

canceled;
canceled;
func ternaryreal -> TriOp of REAL means :Def4: :: ALGSTR_3:def 4
for a, b, c being Real holds it . (a,b,c) = (a * b) + c;
existence
ex b₁ being TriOp of REAL st
for a, b, c being Real holds b₁ . (a,b,c) = (a * b) + c

proof end;

uniqueness
for b₁, b₂ being TriOp of REAL st ( for a, b, c being Real holds b₁ . (a,b,c) = (a * b) + c ) & ( for a, b, c being Real holds b₂ . (a,b,c) = (a * b) + c ) holds
b₁ = b₂

proof end;

end;

:: deftheorem ALGSTR_3:def 2 :
canceled;

:: deftheorem ALGSTR_3:def 3 :
canceled;

:: deftheorem Def4 defines ternaryreal ALGSTR_3:def 4 :
for b₁ being TriOp of REAL holds
( b₁ = ternaryreal iff for a, b, c being Real holds b₁ . (a,b,c) = (a * b) + c );

definition

func TernaryFieldEx -> strict TernaryFieldStr equals :: ALGSTR_3:def 5
TernaryFieldStr(# REAL,0,1,ternaryreal #);
correctness
coherence
TernaryFieldStr(# REAL,0,1,ternaryreal #) is strict TernaryFieldStr ;
;

end;

:: deftheorem defines TernaryFieldEx ALGSTR_3:def 5 :
TernaryFieldEx = TernaryFieldStr(# REAL,0,1,ternaryreal #);

registration

cluster TernaryFieldEx -> non empty strict ;
coherence
not TernaryFieldEx is empty ;

end;

definition

let a, b, c be Scalar of TernaryFieldEx;
func tern (a,b,c) -> Scalar of TernaryFieldEx equals :: ALGSTR_3:def 6
the TernOp of TernaryFieldEx . (a,b,c);
correctness
coherence
the TernOp of TernaryFieldEx . (a,b,c) is Scalar of TernaryFieldEx;
;

end;

:: deftheorem defines tern ALGSTR_3:def 6 :
for a, b, c being Scalar of TernaryFieldEx holds tern (a,b,c) = the TernOp of TernaryFieldEx . (a,b,c);

theorem :: ALGSTR_3:1

canceled;

theorem :: ALGSTR_3:2

canceled;

theorem Th3: :: ALGSTR_3:3

for u, u9, v, v9 being Real st u <> u9 holds
ex x being Real st (u * x) + v = (u9 * x) + v9

proof end;

theorem :: ALGSTR_3:4

canceled;

theorem :: ALGSTR_3:5

for u, a, v being Scalar of TernaryFieldEx
for z, x, y being Real st u = z & a = x & v = y holds
Tern (u,a,v) = (z * x) + y by Def4;

theorem :: ALGSTR_3:6

canceled;

theorem :: ALGSTR_3:7

1 = 1. TernaryFieldEx ;

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 ;
attr IT is Ternary-Field-like means :Def7: :: 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, 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 ) );

end;

:: deftheorem Def7 defines Ternary-Field-like ALGSTR_3:def 7 :
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

cluster non empty strict Ternary-Field-like TernaryFieldStr ;
existence
ex b₁ being non empty TernaryFieldStr st
( b₁ is strict & b₁ is Ternary-Field-like )

proof end;

end;

definition

mode Ternary-Field is non empty Ternary-Field-like TernaryFieldStr ;

end;

theorem :: ALGSTR_3:8

for F being Ternary-Field
for a, a9, u, v, u9, 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:9

canceled;

theorem :: ALGSTR_3:10

canceled;

theorem :: ALGSTR_3:11

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

proof end;

theorem :: ALGSTR_3:12

for F being Ternary-Field
for a, x, b, 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:13

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

proof end;

theorem :: ALGSTR_3:14

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

proof end;