:: ALGSTR_3 semantic presentation

begin

definition
attrc1 is strict ;
struct TernaryFieldStr  ->  ZeroOneStr ;
aggrTernaryFieldStr(# carrier, ZeroF, OneF, TernOp #) ->  TernaryFieldStr ;
sel TernOp c1 ->  TriOp of the carrier of c1;
end;

registration
cluster non empty for TernaryFieldStr ;
existence
 not for b1 being TernaryFieldStr holds b1 is empty
proof
set A = the non empty set ;
set Z = the Element of the non empty set ;
set t = the TriOp of the non empty set ;
take  TernaryFieldStr(# the non empty set , the Element of the non empty set , the Element of the non empty set , the TriOp of the non empty set #) ; ::_thesis: not TernaryFieldStr(# the non empty set , the Element of the non empty set , the Element of the non empty set , the TriOp of the non empty set #) is empty
thus  not the carrier of TernaryFieldStr(# the non empty set , the Element of the non empty set , the Element of the non empty set , the TriOp of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
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
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
 ex b1 being TriOp of REAL st
for a, b, c being Real holds b1 . (a,b,c) = (a * b) + c
proof
deffunc H1( Real, Real, Real) ->  Element of REAL = ($1 * $2) + $3;
 ex X being TriOp of REAL st
for a, b, c being Real holds X . (a,b,c) = H1(a,b,c) from MULTOP_1:sch_4();
hence  ex b1 being TriOp of REAL st
for a, b, c being Real holds b1 . (a,b,c) = (a * b) + c ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being TriOp of REAL st ( for a, b, c being Real holds b1 . (a,b,c) = (a * b) + c ) & ( for a, b, c being Real holds b2 . (a,b,c) = (a * b) + c ) holds
b1 = b2
proof
let o1, o2 be TriOp of REAL; ::_thesis: ( ( for a, b, c being Real holds o1 . (a,b,c) = (a * b) + c ) & ( for a, b, c being Real holds o2 . (a,b,c) = (a * b) + c ) implies o1 = o2 )
assume that
A1: for a, b, c being Real holds o1 . (a,b,c) = (a * b) + c and
A2: for a, b, c being Real holds o2 . (a,b,c) = (a * b) + c ; ::_thesis: o1 = o2
 for a, b, c being Real holds o1 . (a,b,c) = o2 . (a,b,c)
proof
let a, b, c be Real; ::_thesis: o1 . (a,b,c) = o2 . (a,b,c)
thus o1 . (a,b,c) = (a * b) + c by A1
.= o2 . (a,b,c) by A2 ; ::_thesis: verum
end;
hence  o1 = o2 by MULTOP_1:3; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines ternaryreal ALGSTR_3:def_2_:_
 for b1 being TriOp of REAL holds
( b1 = ternaryreal iff for a, b, c being Real holds b1 . (a,b,c) = (a * b) + c );

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

:: deftheorem  defines TernaryFieldEx ALGSTR_3:def_3_:_
 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 4
 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_4_:_
 for a, b, c being Scalar of TernaryFieldEx holds tern (a,b,c) = the TernOp of TernaryFieldEx . (a,b,c);

theorem Th1: :: ALGSTR_3:1
for u, u9, v, v9 being Real st u <> u9 holds
ex x being Real st (u * x) + v = (u9 * x) + v9
proof
let u, u9, v, v9 be Real; ::_thesis: ( u <> u9 implies ex x being Real st (u * x) + v = (u9 * x) + v9 )
set x = (v9 - v) / (u - u9);
assume  u <> u9 ; ::_thesis: ex x being Real st (u * x) + v = (u9 * x) + v9
then  u - u9 <> 0 ;
then A1: (u - u9) * ((v9 - v) / (u - u9)) = v9 - v by XCMPLX_1:87;
reconsider x = (v9 - v) / (u - u9) as Real ;
take  x ; ::_thesis: (u * x) + v = (u9 * x) + v9
thus  (u * x) + v = (u9 * x) + v9 by A1; ::_thesis: verum
end;

theorem :: ALGSTR_3:2
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 Def2;

theorem :: ALGSTR_3:3
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; ::_thesis: Tern (a,(1. TernaryFieldEx),(0. TernaryFieldEx)) = a
reconsider x = a as Real ;
thus  Tern (a,(1. TernaryFieldEx),(0. TernaryFieldEx)) = (x * 1) + 0 by Def2
.= a ; ::_thesis: verum
end;

Lm2:  for a being Scalar of TernaryFieldEx holds Tern ((1. TernaryFieldEx),a,(0. TernaryFieldEx)) = a
proof
let a be Scalar of TernaryFieldEx; ::_thesis: Tern ((1. TernaryFieldEx),a,(0. TernaryFieldEx)) = a
reconsider x = a as Real ;
thus  Tern ((1. TernaryFieldEx),a,(0. TernaryFieldEx)) = (x * 1) + 0 by Def2
.= a ; ::_thesis: verum
end;

Lm3:  for a, b being Scalar of TernaryFieldEx holds Tern (a,(0. TernaryFieldEx),b) = b
proof
let a, b be Scalar of TernaryFieldEx; ::_thesis: Tern (a,(0. TernaryFieldEx),b) = b
reconsider x = a, y = b as Real ;
thus  Tern (a,(0. TernaryFieldEx),b) = (x * 0) + y by Def2
.= b ; ::_thesis: verum
end;

Lm4:  for a, b being Scalar of TernaryFieldEx holds Tern ((0. TernaryFieldEx),a,b) = b
proof
let a, b be Scalar of TernaryFieldEx; ::_thesis: Tern ((0. TernaryFieldEx),a,b) = b
reconsider x = a, y = b as Real ;
thus  Tern ((0. TernaryFieldEx),a,b) = (0 * x) + y by Def2
.= b ; ::_thesis: verum
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; ::_thesis: ex v being Scalar of TernaryFieldEx st Tern (u,a,v) = b
reconsider z = u, x = a, y = b as Real ;
reconsider t = y - (z * x) as Real ;
reconsider v = t as Scalar of TernaryFieldEx ;
take  v ; ::_thesis: Tern (u,a,v) = b
 y = (z * x) + t ;
hence  Tern (u,a,v) = b by Def2; ::_thesis: verum
end;

Lm6:  for u, a, v, v9 being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u,a,v9) holds
v = v9
proof
let u, a, v, v9 be Scalar of TernaryFieldEx; ::_thesis: ( Tern (u,a,v) = Tern (u,a,v9) implies v = v9 )
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  ( Tern (u,a,v) = Tern (u,a,v9) implies v = v9 ) ; ::_thesis: verum
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
let a, a9 be Scalar of TernaryFieldEx; ::_thesis: ( 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 ) )
assume A1: a <> a9 ; ::_thesis: 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 )
let b, b9 be Scalar of TernaryFieldEx; ::_thesis: ex u, v being Scalar of TernaryFieldEx st
( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )
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 * ((y9 - y) / (x9 - x)));
reconsider u = (y9 - y) / (x9 - x), v = y - (x * ((y9 - y) / (x9 - x))) as Scalar of TernaryFieldEx ;
take  u ; ::_thesis: ex v being Scalar of TernaryFieldEx st
( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )
take  v ; ::_thesis: ( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )
thus  Tern (u,a,v) = (((y9 - y) / (x9 - x)) * x) + ((- (((y9 - y) / (x9 - x)) * x)) + y) by Def2
.= b ; ::_thesis: Tern (u,a9,v) = b9
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 ; ::_thesis: verum
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
let u, u9 be Scalar of TernaryFieldEx; ::_thesis: ( 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) )
assume A1: u <> u9 ; ::_thesis: for v, v9 being Scalar of TernaryFieldEx ex a being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u9,a,v9)
let v, v9 be Scalar of TernaryFieldEx; ::_thesis: ex a being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u9,a,v9)
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 ;
 ( Tern (u,a,v) = (uu * aa) + vv & Tern (u9,a,v9) = (uu9 * aa) + vv9 ) by Def2;
hence  ex a being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u9,a,v9) by A2; ::_thesis: verum
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
let a, a9, u, u9, v, v9 be Scalar of TernaryFieldEx; ::_thesis: ( Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) & not a = a9 implies u = u9 )
assume A1: ( Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) ) ; ::_thesis: ( a = a9 or u = u9 )
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  ( a = a9 or u = u9 ) ; ::_thesis: verum
end;

definition
let IT be non empty TernaryFieldStr ;
attrIT 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 ) );
end;

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

registration
cluster non empty strict Ternary-Field-like for TernaryFieldStr ;
existence
 ex b1 being non empty TernaryFieldStr st
( b1 is strict & b1 is Ternary-Field-like )
proof
 TernaryFieldEx is Ternary-Field-like by Def5, Lm1, Lm2, Lm3, Lm4, Lm5, Lm6, Lm7, Lm8, Lm9;
hence  ex b1 being non empty TernaryFieldStr st
( b1 is strict & b1 is Ternary-Field-like ) ; ::_thesis: verum
end;
end;

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


theorem :: ALGSTR_3:4
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
let F be Ternary-Field; ::_thesis: 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 )
let a, a9, u, v, u9, v9 be Scalar of F; ::_thesis: ( a <> a9 & Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) implies ( u = u9 & v = v9 ) )
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) ; ::_thesis: ( u = u9 & v = v9 )
 u = u9 by A1, A2, A3, Def5;
hence  ( u = u9 & v = v9 ) by A2, Def5; ::_thesis: verum
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
proof
let F be Ternary-Field; ::_thesis: 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
let a be Scalar of F; ::_thesis: ( a <> 0. F implies for b, c being Scalar of F ex x being Scalar of F st Tern (a,x,b) = c )
assume A1: a <> 0. F ; ::_thesis: for b, c being Scalar of F ex x being Scalar of F st Tern (a,x,b) = c
let b, c be Scalar of F; ::_thesis: ex x being Scalar of F st Tern (a,x,b) = c
consider x being Scalar of F such that
A2: Tern (a,x,b) = Tern ((0. F),x,c) by A1, Def5;
take  x ; ::_thesis: Tern (a,x,b) = c
thus  Tern (a,x,b) = c by A2, Def5; ::_thesis: verum
end;

theorem :: ALGSTR_3:6
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
let F be Ternary-Field; ::_thesis: for a, x, b, x9 being Scalar of F st a <> 0. F & Tern (a,x,b) = Tern (a,x9,b) holds
x = x9
let a, x, b, x9 be Scalar of F; ::_thesis: ( a <> 0. F & Tern (a,x,b) = Tern (a,x9,b) implies x = x9 )
assume that
A1: a <> 0. F and
A2: Tern (a,x,b) = Tern (a,x9,b) ; ::_thesis: x = x9
set c = Tern (a,x,b);
A3: Tern (a,x,b) = Tern ((0. F),x,(Tern (a,x,b))) by Def5;
 Tern (a,x9,b) = Tern ((0. F),x9,(Tern (a,x,b))) by A2, Def5;
hence  x = x9 by A1, A3, Def5; ::_thesis: verum
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
proof
let F be Ternary-Field; ::_thesis: 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
let a be Scalar of F; ::_thesis: ( a <> 0. F implies for b, c being Scalar of F ex x being Scalar of F st Tern (x,a,b) = c )
assume A1: a <> 0. F ; ::_thesis: for b, c being Scalar of F ex x being Scalar of F st Tern (x,a,b) = c
let b, c be Scalar of F; ::_thesis: ex x being Scalar of F st Tern (x,a,b) = c
consider x, z being Scalar of F such that
A2: ( Tern (x,a,z) = c & Tern (x,(0. F),z) = b ) by A1, Def5;
take  x ; ::_thesis: Tern (x,a,b) = c
thus  Tern (x,a,b) = c by A2, Def5; ::_thesis: verum
end;

theorem :: ALGSTR_3:8
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
let F be Ternary-Field; ::_thesis: for a, x, b, x9 being Scalar of F st a <> 0. F & Tern (x,a,b) = Tern (x9,a,b) holds
x = x9
let a, x, b, x9 be Scalar of F; ::_thesis: ( a <> 0. F & Tern (x,a,b) = Tern (x9,a,b) implies x = x9 )
assume A1: ( a <> 0. F & Tern (x,a,b) = Tern (x9,a,b) ) ; ::_thesis: x = x9
 ( Tern (x,(0. F),b) = b & Tern (x9,(0. F),b) = b ) by Def5;
hence  x = x9 by A1, Def5; ::_thesis: verum
end;