:: ALGSTR_3 semantic presentation
:: deftheorem defines Tern ALGSTR_3:def 1 :
:: deftheorem ALGSTR_3:def 2 :
canceled;
:: deftheorem defines 1_ ALGSTR_3:def 3 :
definition
func ternaryreal -> TriOp of
REAL means :
E1:
:: ALGSTR_3:def 4
for b
1, b
2, b
3 being
Real holds a
1 . b
1,b
2,b
3 = (b1 * b2) + b
3;
existence
ex b1 being TriOp of REAL st
for b2, b3, b4 being Real holds b1 . b2,b3,b4 = (b2 * b3) + b4
proof
deffunc H
1(
Real,
Real,
Real)
-> Element of
REAL =
(a1 * a2) + a
3;
ex b
1 being
TriOp of
REAL st
for b
2, b
3, b
4 being
Real holds b
1 . b
2,b
3,b
4 = H
1(b
2,b
3,b
4)
from MULTOP_1:sch 4();
hence
ex b
1 being
TriOp of
REAL st
for b
2, b
3, b
4 being
Real holds b
1 . b
2,b
3,b
4 = (b2 * b3) + b
4
;
end;
uniqueness
for b1, b2 being TriOp of REAL holds
( ( for b3, b4, b5 being Real holds b1 . b3,b4,b5 = (b3 * b4) + b5 & for b3, b4, b5 being Real holds b2 . b3,b4,b5 = (b3 * b4) + b5 ) implies ( b1 = b2 ) )
proof
let c
1, c
2 be
TriOp of
REAL ;
assume that
E1:
for b
1, b
2, b
3 being
Real holds c
1 . b
1,b
2,b
3 = (b1 * b2) + b
3
and
E2:
for b
1, b
2, b
3 being
Real holds c
2 . b
1,b
2,b
3 = (b1 * b2) + b
3
;
for b
1, b
2, b
3 being
Real holds c
1 . b
1,b
2,b
3 = c
2 . b
1,b
2,b
3
proof
let c
3, c
4, c
5 be
Real;
thus c
1 . c
3,c
4,c
5 =
(c3 * c4) + c
5
by E1
.=
c
2 . c
3,c
4,c
5
by E2
;
end;
hence
c
1 = c
2
by MULTOP_1:4;
end;
end;
:: deftheorem E1 defines ternaryreal ALGSTR_3:def 4 :
:: deftheorem defines TernaryFieldEx ALGSTR_3:def 5 :
:: deftheorem defines tern ALGSTR_3:def 6 :
theorem :: ALGSTR_3:1
canceled;
theorem :: ALGSTR_3:2
canceled;
theorem E2: :: ALGSTR_3:3
for b
1, b
2, b
3, b
4 being
Real holds
not ( b
1 <> b
2 & for b
5 being
Real holds
not
(b1 * b5) + b
3 = (b2 * b5) + b
4 )
proof
let c
1, c
2, c
3, c
4 be
Real;
assume E3:
c
1 <> c
2
;
set c
5 =
(c4 - c3) / (c1 - c2);
c
1 - c
2 <> 0
by E3;
then E4:
(c1 - c2) * ((c4 - c3) / (c1 - c2)) = c
4 - c
3
by XCMPLX_1:88;
reconsider c
6 =
(c4 - c3) / (c1 - c2) as
Real ;
(c1 * c6) - (c2 * c6) = c
4 - c
3
by E4;
then
(c1 * c6) + (- (c2 * c6)) = c
4 - c
3
;
then E5: c
1 * c
6 =
(c4 - c3) - (- (c2 * c6))
.=
((c2 * c6) + c4) + (- c3)
;
take
c
6
;
thus
(c1 * c6) + c
3 = (c2 * c6) + c
4
by E5;
end;
theorem :: ALGSTR_3:4
canceled;
theorem E3: :: ALGSTR_3:5
theorem E4: :: ALGSTR_3:6
theorem :: ALGSTR_3:7
E5:
for b1 being Scalar of TernaryFieldEx holds Tern b1,(1_ TernaryFieldEx ),(0. TernaryFieldEx ) = b1
E6:
for b1 being Scalar of TernaryFieldEx holds Tern (1_ TernaryFieldEx ),b1,(0. TernaryFieldEx ) = b1
E7:
for b1, b2 being Scalar of TernaryFieldEx holds Tern b1,(0. TernaryFieldEx ),b2 = b2
E8:
for b1, b2 being Scalar of TernaryFieldEx holds Tern (0. TernaryFieldEx ),b1,b2 = b2
E9:
for b1, b2, b3 being Scalar of TernaryFieldEx holds
ex b4 being Scalar of TernaryFieldEx st Tern b1,b2,b4 = b3
E10:
for b1, b2, b3, b4 being Scalar of TernaryFieldEx holds
( Tern b1,b2,b3 = Tern b1,b2,b4 implies b3 = b4 )
proof
let c
1, c
2, c
3, c
4 be
Scalar of
TernaryFieldEx ;
reconsider c
5 = c
1, c
6 = c
2, c
7 = c
3, c
8 = c
4 as
Real ;
E11:
Tern c
1,c
2,c
3 = (c5 * c6) + c
7
by E3;
Tern c
1,c
2,c
4 = (c5 * c6) + c
8
by E3;
hence
(
Tern c
1,c
2,c
3 = Tern c
1,c
2,c
4 implies c
3 = c
4 )
by E11, XCMPLX_1:2;
end;
E11:
for b1, b2 being Scalar of TernaryFieldEx holds
( b1 <> b2 implies for b3, b4 being Scalar of TernaryFieldEx holds
ex b5, b6 being Scalar of TernaryFieldEx st
( Tern b5,b1,b6 = b3 & Tern b5,b2,b6 = b4 ) )
proof
let c
1, c
2 be
Scalar of
TernaryFieldEx ;
assume E12:
c
1 <> c
2
;
let c
3, c
4 be
Scalar of
TernaryFieldEx ;
reconsider c
5 = c
1, c
6 = c
2, c
7 = c
3, c
8 = c
4 as
Real ;
set c
9 =
(c8 - c7) / (c6 - c5);
set c
10 = c
7 - (c5 * ((c8 - c7) / (c6 - c5)));
reconsider c
11 =
(c8 - c7) / (c6 - c5), c
12 = c
7 - (c5 * ((c8 - c7) / (c6 - c5))) as
Scalar of
TernaryFieldEx ;
take
c
11
;
take
c
12
;
thus Tern c
11,c
1,c
12 =
ternaryreal . ((c8 - c7) / (c6 - c5)),c
5,
(c7 - (c5 * ((c8 - c7) / (c6 - c5))))
.=
(((c8 - c7) / (c6 - c5)) * c5) + ((- (((c8 - c7) / (c6 - c5)) * c5)) + c7)
by E1
.=
c
7 + 0
.=
c
3
;
E13:
c
6 - c
5 <> 0
by E12;
thus Tern c
11,c
2,c
12 =
ternaryreal . ((c8 - c7) / (c6 - c5)),c
6,
(c7 - (c5 * ((c8 - c7) / (c6 - c5))))
.=
(((c8 - c7) / (c6 - c5)) * c6) + ((- (c5 * ((c8 - c7) / (c6 - c5)))) + c7)
by E1
.=
(((c8 - c7) / (c6 - c5)) * (c6 - c5)) + c
7
.=
(c8 - c7) + c
7
by E13, XCMPLX_1:88
.=
c
4
;
end;
E12:
for b1, b2 being Scalar of TernaryFieldEx holds
( b1 <> b2 implies for b3, b4 being Scalar of TernaryFieldEx holds
ex b5 being Scalar of TernaryFieldEx st Tern b1,b5,b3 = Tern b2,b5,b4 )
proof
let c
1, c
2 be
Scalar of
TernaryFieldEx ;
assume E13:
c
1 <> c
2
;
let c
3, c
4 be
Scalar of
TernaryFieldEx ;
reconsider c
5 = c
1, c
6 = c
2, c
7 = c
3, c
8 = c
4 as
Real ;
consider c
9 being
Real such that
E14:
(c5 * c9) + c
7 = (c6 * c9) + c
8
by E13, E2;
reconsider c
10 = c
9 as
Scalar of
TernaryFieldEx ;
(
Tern c
1,c
10,c
3 = (c5 * c9) + c
7 &
Tern c
2,c
10,c
4 = (c6 * c9) + c
8 )
by E3;
hence
ex b
1 being
Scalar of
TernaryFieldEx st
Tern c
1,b
1,c
3 = Tern c
2,b
1,c
4
by E14;
end;
E13:
for b1, b2, b3, b4, b5, b6 being Scalar of TernaryFieldEx holds
not ( Tern b3,b1,b5 = Tern b4,b1,b6 & Tern b3,b2,b5 = Tern b4,b2,b6 & not b1 = b2 & not b3 = b4 )
proof
let c
1, c
2, c
3, c
4, c
5, c
6 be
Scalar of
TernaryFieldEx ;
assume that
E14:
Tern c
3,c
1,c
5 = Tern c
4,c
1,c
6
and
E15:
Tern c
3,c
2,c
5 = Tern c
4,c
2,c
6
;
reconsider c
7 = c
1, c
8 = c
2, c
9 = c
3, c
10 = c
4, c
11 = c
5, c
12 = c
6 as
Real ;
(
Tern c
3,c
1,c
5 = (c9 * c7) + c
11 &
Tern c
4,c
1,c
6 = (c10 * c7) + c
12 &
Tern c
3,c
2,c
5 = (c9 * c8) + c
11 &
Tern c
4,c
2,c
6 = (c10 * c8) + c
12 )
by E3;
then
(c9 * c7) + (c11 - ((c9 * c8) + c11)) = ((c10 * c7) + c12) - ((c10 * c8) + c12)
by E14, E15, XCMPLX_1:29;
then
(c9 * c7) + (- (c9 * c8)) = (c10 * c7) + (- (c10 * c8))
;
then
(c9 * c7) - (c9 * c8) = (c10 * c7) - (c10 * c8)
;
then
c
9 * (c7 - c8) = c
10 * (c7 - c8)
;
then
( c
9 = c
10 or c
7 - c
8 = 0 )
by XCMPLX_1:5;
hence
not ( not c
1 = c
2 & not c
3 = c
4 )
;
end;
definition
let c
1 be non
empty TernaryFieldStr ;
attr a
1 is
Ternary-Field-like means :
E14:
:: ALGSTR_3:def 7
(
0. a
1 <> 1_ a
1 & for b
1 being
Scalar of a
1 holds
Tern b
1,
(1_ a1),
(0. a1) = b
1 & for b
1 being
Scalar of a
1 holds
Tern (1_ a1),b
1,
(0. a1) = b
1 & for b
1, b
2 being
Scalar of a
1 holds
Tern b
1,
(0. a1),b
2 = b
2 & for b
1, b
2 being
Scalar of a
1 holds
Tern (0. a1),b
1,b
2 = b
2 & for b
1, b
2, b
3 being
Scalar of a
1 holds
ex b
4 being
Scalar of a
1 st
Tern b
1,b
2,b
4 = b
3 & for b
1, b
2, b
3, b
4 being
Scalar of a
1 holds
(
Tern b
1,b
2,b
3 = Tern b
1,b
2,b
4 implies b
3 = b
4 ) & for b
1, b
2 being
Scalar of a
1 holds
( b
1 <> b
2 implies for b
3, b
4 being
Scalar of a
1 holds
ex b
5, b
6 being
Scalar of a
1 st
(
Tern b
5,b
1,b
6 = b
3 &
Tern b
5,b
2,b
6 = b
4 ) ) & for b
1, b
2 being
Scalar of a
1 holds
( b
1 <> b
2 implies for b
3, b
4 being
Scalar of a
1 holds
ex b
5 being
Scalar of a
1 st
Tern b
1,b
5,b
3 = Tern b
2,b
5,b
4 ) & for b
1, b
2, b
3, b
4, b
5, b
6 being
Scalar of a
1 holds
not (
Tern b
3,b
1,b
5 = Tern b
4,b
1,b
6 &
Tern b
3,b
2,b
5 = Tern b
4,b
2,b
6 & not b
1 = b
2 & not b
3 = b
4 ) );
end;
:: deftheorem E14 defines Ternary-Field-like ALGSTR_3:def 7 :
for b
1 being non
empty TernaryFieldStr holds
( b
1 is
Ternary-Field-like iff (
0. b
1 <> 1_ b
1 & for b
2 being
Scalar of b
1 holds
Tern b
2,
(1_ b1),
(0. b1) = b
2 & for b
2 being
Scalar of b
1 holds
Tern (1_ b1),b
2,
(0. b1) = b
2 & for b
2, b
3 being
Scalar of b
1 holds
Tern b
2,
(0. b1),b
3 = b
3 & for b
2, b
3 being
Scalar of b
1 holds
Tern (0. b1),b
2,b
3 = b
3 & for b
2, b
3, b
4 being
Scalar of b
1 holds
ex b
5 being
Scalar of b
1 st
Tern b
2,b
3,b
5 = b
4 & for b
2, b
3, b
4, b
5 being
Scalar of b
1 holds
(
Tern b
2,b
3,b
4 = Tern b
2,b
3,b
5 implies b
4 = b
5 ) & for b
2, b
3 being
Scalar of b
1 holds
( b
2 <> b
3 implies for b
4, b
5 being
Scalar of b
1 holds
ex b
6, b
7 being
Scalar of b
1 st
(
Tern b
6,b
2,b
7 = b
4 &
Tern b
6,b
3,b
7 = b
5 ) ) & for b
2, b
3 being
Scalar of b
1 holds
( b
2 <> b
3 implies for b
4, b
5 being
Scalar of b
1 holds
ex b
6 being
Scalar of b
1 st
Tern b
2,b
6,b
4 = Tern b
3,b
6,b
5 ) & for b
2, b
3, b
4, b
5, b
6, b
7 being
Scalar of b
1 holds
not (
Tern b
4,b
2,b
6 = Tern b
5,b
2,b
7 &
Tern b
4,b
3,b
6 = Tern b
5,b
3,b
7 & not b
2 = b
3 & not b
4 = b
5 ) ) );
registration
cluster non
empty strict Ternary-Field-like TernaryFieldStr ;
existence
ex b1 being non empty TernaryFieldStr st
( b1 is strict & b1 is Ternary-Field-like )
proof
TernaryFieldEx is
Ternary-Field-like
by E14, E5, E6, E7, E8, E9, E10, E11, E12, E13, E4;
hence
ex b
1 being non
empty TernaryFieldStr st
( b
1 is
strict & b
1 is
Ternary-Field-like )
;
end;
end;
theorem :: ALGSTR_3:8
for b
1 being
Ternary-Fieldfor b
2, b
3, b
4, b
5, b
6, b
7 being
Scalar of b
1 holds
( (
Tern b
4,b
2,b
5 = Tern b
6,b
2,b
7 &
Tern b
4,b
3,b
5 = Tern b
6,b
3,b
7 ) implies ( not b
2 <> b
3 or ( b
4 = b
6 & b
5 = b
7 ) ) )
proof
let c
1 be
Ternary-Field;
let c
2, c
3, c
4, c
5, c
6, c
7 be
Scalar of c
1;
assume that
E15:
c
2 <> c
3
and
E16:
Tern c
4,c
2,c
5 = Tern c
6,c
2,c
7
and
E17:
Tern c
4,c
3,c
5 = Tern c
6,c
3,c
7
;
c
4 = c
6
by E15, E16, E17, E14;
hence
( c
4 = c
6 & c
5 = c
7 )
by E16, E14;
end;
theorem :: ALGSTR_3:9
canceled;
theorem :: ALGSTR_3:10
canceled;
theorem :: ALGSTR_3:11
theorem :: ALGSTR_3:12
proof
let c
1 be
Ternary-Field;
let c
2, c
3, c
4, c
5 be
Scalar of c
1;
assume that
E15:
c
2 <> 0. c
1
and
E16:
Tern c
2,c
3,c
4 = Tern c
2,c
5,c
4
;
set c
6 =
Tern c
2,c
3,c
4;
(
Tern c
2,c
3,c
4 = Tern (0. c1),c
3,
(Tern c2,c3,c4) &
Tern c
2,c
5,c
4 = Tern (0. c1),c
5,
(Tern c2,c3,c4) )
by E16, E14;
hence
c
3 = c
5
by E15, E14;
end;
theorem :: ALGSTR_3:13
proof
let c
1 be
Ternary-Field;
let c
2 be
Scalar of c
1;
assume E15:
c
2 <> 0. c
1
;
let c
3, c
4 be
Scalar of c
1;
consider c
5, c
6 being
Scalar of c
1 such that
E16:
(
Tern c
5,c
2,c
6 = c
4 &
Tern c
5,
(0. c1),c
6 = c
3 )
by E15, E14;
take
c
5
;
thus
Tern c
5,c
2,c
3 = c
4
by E16, E14;
end;
theorem :: ALGSTR_3:14
proof
let c
1 be
Ternary-Field;
let c
2, c
3, c
4, c
5 be
Scalar of c
1;
assume E15:
( c
2 <> 0. c
1 &
Tern c
3,c
2,c
4 = Tern c
5,c
2,c
4 )
;
(
Tern c
3,
(0. c1),c
4 = c
4 &
Tern c
5,
(0. c1),c
4 = c
4 )
by E14;
hence
c
3 = c
5
by E15, E14;
end;