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