:: MOD_2 semantic presentation

E1: op0 = {} by TARSKI:def 1
.= Extract {} by ALGSTR_1:def 3 ;

Lemma2: for b1 being Ring holds VectSpStr(# {{} },op2 ,op0 ,(pr2 the carrier of b1,{{} }) #) is strict LeftMod of b1
proof end;

definition
let c1 be Ring;
canceled;
func TrivialLMod c1 -> strict LeftMod of a1 equals :: MOD_2:def 2
 VectSpStr(# {{} },op2 ,op0 ,(pr2 the carrier of a1,{{} }) #);
coherence
VectSpStr(# {{} },op2 ,op0 ,(pr2 the carrier of c1,{{} }) #) is strict LeftMod of c1 by Lemma2;
end;

:: deftheorem Def1 MOD_2:def 1 :
canceled;

:: deftheorem Def2 defines TrivialLMod MOD_2:def 2 :
for b1 being Ring holds TrivialLMod b1 = VectSpStr(# {{} },op2 ,op0 ,(pr2 the carrier of b1,{{} }) #);

theorem Th1: :: MOD_2:1
for b1 being Ring
for b2 being Vector of (TrivialLMod b1) holds b2 = 0. (TrivialLMod b1) by Lemma1, ALGSTR_1:def 4, GRCAT_1:8;

definition
let c1 be non empty doubleLoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Function of c2,c3;
canceled;
canceled;
attr a4 is linear means :Def5: :: MOD_2:def 5
( ( for b1, b2 being Vector of a2 holds a4 . (b1 + b2) = (a4 . b1) + (a4 . b2) ) & ( for b1 being Scalar of a1
for b2 being Vector of a2 holds a4 . (b1 * b2) = b1 * (a4 . b2) ) );
end;

:: deftheorem Def3 MOD_2:def 3 :
canceled;

:: deftheorem Def4 MOD_2:def 4 :
canceled;

:: deftheorem Def5 defines linear MOD_2:def 5 :
for b1 being non empty doubleLoopStr
for b2, b3 being non empty VectSpStr of b1
for b4 being Function of b2,b3 holds
( b4 is linear iff ( ( for b5, b6 being Vector of b2 holds b4 . (b5 + b6) = (b4 . b5) + (b4 . b6) ) & ( for b5 being Scalar of b1
for b6 being Vector of b2 holds b4 . (b5 * b6) = b5 * (b4 . b6) ) ) );

theorem Th2: :: MOD_2:2
canceled;

theorem Th3: :: MOD_2:3
canceled;

theorem Th4: :: MOD_2:4
for b1 being Ring
for b2, b3 being non empty VectSpStr of b1
for b4 being Function of b2,b3 st b4 is linear holds
b4 is additive
proof end;

theorem Th5: :: MOD_2:5
canceled;

theorem Th6: :: MOD_2:6
for b1 being Ring
for b2, b3, b4 being non empty VectSpStr of b1
for b5 being Function of b2,b3
for b6 being Function of b3,b4 st b5 is linear & b6 is linear holds
b6 * b5 is linear
proof end;

theorem Th7: :: MOD_2:7
canceled;

theorem Th8: :: MOD_2:8
for b1 being Ring
for b2, b3 being LeftMod of b1 holds ZeroMap b2,b3 is linear
proof end;

definition
let c1 be Ring;
attr a2 is strict;
struct LModMorphismStr of c1 -> ;
aggr LModMorphismStr(# Dom, Cod, Fun #) -> LModMorphismStr of a1;
sel Dom c2 -> LeftMod of a1;
sel Cod c2 -> LeftMod of a1;
sel Fun c2 -> Function of the Dom of a2,the Cod of a2;
end;

definition
let c1 be Ring;
let c2 be LModMorphismStr of c1;
func dom c2 -> LeftMod of a1 equals :: MOD_2:def 6
the Dom of a2;
correctness
coherence
the Dom of c2 is LeftMod of c1;
;
func cod c2 -> LeftMod of a1 equals :: MOD_2:def 7
the Cod of a2;
correctness
coherence
the Cod of c2 is LeftMod of c1;
;
end;

:: deftheorem Def6 defines dom MOD_2:def 6 :
for b1 being Ring
for b2 being LModMorphismStr of b1 holds dom b2 = the Dom of b2;

:: deftheorem Def7 defines cod MOD_2:def 7 :
for b1 being Ring
for b2 being LModMorphismStr of b1 holds cod b2 = the Cod of b2;

definition
let c1 be Ring;
let c2 be LModMorphismStr of c1;
func fun c2 -> Function of (dom a2),(cod a2) equals :: MOD_2:def 8
the Fun of a2;
coherence
the Fun of c2 is Function of (dom c2),(cod c2) ;
end;

:: deftheorem Def8 defines fun MOD_2:def 8 :
for b1 being Ring
for b2 being LModMorphismStr of b1 holds fun b2 = the Fun of b2;

theorem Th9: :: MOD_2:9
for b1 being Ring
for b2, b3 being LeftMod of b1
for b4 being LModMorphismStr of b1
for b5 being Function of b2,b3 st b4 = LModMorphismStr(# b2,b3,b5 #) holds
( dom b4 = b2 & cod b4 = b3 & fun b4 = b5 ) ;

definition
let c1 be Ring;
let c2, c3 be LeftMod of c1;
func ZERO c2,c3 -> strict LModMorphismStr of a1 equals :: MOD_2:def 9
 LModMorphismStr(# a2,a3,(ZeroMap a2,a3) #);
correctness
coherence
LModMorphismStr(# c2,c3,(ZeroMap c2,c3) #) is strict LModMorphismStr of c1;
;
end;

:: deftheorem Def9 defines ZERO MOD_2:def 9 :
for b1 being Ring
for b2, b3 being LeftMod of b1 holds ZERO b2,b3 = LModMorphismStr(# b2,b3,(ZeroMap b2,b3) #);

definition
let c1 be Ring;
let c2 be LModMorphismStr of c1;
attr a2 is LModMorphism-like means :Def10: :: MOD_2:def 10
 fun a2 is linear;
end;

:: deftheorem Def10 defines LModMorphism-like MOD_2:def 10 :
for b1 being Ring
for b2 being LModMorphismStr of b1 holds
( b2 is LModMorphism-like iff fun b2 is linear );

registration
let c1 be Ring;
cluster strict LModMorphism-like LModMorphismStr of a1;
existence
ex b1 being LModMorphismStr of c1 st
( b1 is strict & b1 is LModMorphism-like )
proof end;
end;

definition
let c1 be Ring;
mode LModMorphism of a1 is LModMorphism-like LModMorphismStr of a1;
end;

theorem Th10: :: MOD_2:10
for b1 being Ring
for b2 being LModMorphism of b1 holds the Fun of b2 is linear
proof end;

registration
let c1 be Ring;
let c2, c3 be LeftMod of c1;
cluster ZERO a2,a3 -> strict LModMorphism-like ;
coherence
ZERO c2,c3 is LModMorphism-like
proof end;
end;

definition
let c1 be Ring;
let c2, c3 be LeftMod of c1;
mode Morphism of c2,c3 -> LModMorphism of a1 means :Def11: :: MOD_2:def 11
( dom a4 = a2 & cod a4 = a3 );
existence
ex b1 being LModMorphism of c1 st
( dom b1 = c2 & cod b1 = c3 )
proof end;
end;

:: deftheorem Def11 defines Morphism MOD_2:def 11 :
for b1 being Ring
for b2, b3 being LeftMod of b1
for b4 being LModMorphism of b1 holds
( b4 is Morphism of b2,b3 iff ( dom b4 = b2 & cod b4 = b3 ) );

registration
let c1 be Ring;
let c2, c3 be LeftMod of c1;
cluster strict Morphism of a2,a3;
existence
ex b1 being Morphism of c2,c3 st b1 is strict
proof end;
end;

theorem Th11: :: MOD_2:11
for b1 being Ring
for b2, b3 being LeftMod of b1
for b4 being LModMorphismStr of b1 st dom b4 = b2 & cod b4 = b3 & fun b4 is linear holds
b4 is Morphism of b2,b3
proof end;

theorem Th12: :: MOD_2:12
for b1 being Ring
for b2, b3 being LeftMod of b1
for b4 being Function of b2,b3 st b4 is linear holds
LModMorphismStr(# b2,b3,b4 #) is strict Morphism of b2,b3
proof end;

theorem Th13: :: MOD_2:13
for b1 being Ring
for b2 being LeftMod of b1 holds id b2 is linear
proof end;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
func ID c2 -> strict Morphism of a2,a2 equals :: MOD_2:def 12
 LModMorphismStr(# a2,a2,(id a2) #);
coherence
LModMorphismStr(# c2,c2,(id c2) #) is strict Morphism of c2,c2
proof end;
end;

:: deftheorem Def12 defines ID MOD_2:def 12 :
for b1 being Ring
for b2 being LeftMod of b1 holds ID b2 = LModMorphismStr(# b2,b2,(id b2) #);

definition
let c1 be Ring;
let c2, c3 be LeftMod of c1;
redefine func ZERO as ZERO c2,c3 -> strict Morphism of a2,a3;
coherence
ZERO c2,c3 is strict Morphism of c2,c3
proof end;
end;

theorem Th14: :: MOD_2:14
for b1 being Ring
for b2, b3 being LeftMod of b1
for b4 being Morphism of b2,b3 ex b5 being Function of b2,b3 st
( LModMorphismStr(# the Dom of b4,the Cod of b4,the Fun of b4 #) = LModMorphismStr(# b2,b3,b5 #) & b5 is linear )
proof end;

theorem Th15: :: MOD_2:15
for b1 being Ring
for b2, b3 being LeftMod of b1
for b4 being strict Morphism of b2,b3 ex b5 being Function of b2,b3 st b4 = LModMorphismStr(# b2,b3,b5 #)
proof end;

theorem Th16: :: MOD_2:16
for b1 being Ring
for b2 being LModMorphism of b1 ex b3, b4 being LeftMod of b1 st b2 is Morphism of b3,b4
proof end;

theorem Th17: :: MOD_2:17
for b1 being Ring
for b2 being strict LModMorphism of b1 ex b3, b4 being LeftMod of b1ex b5 being Function of b3,b4 st
( b2 is strict Morphism of b3,b4 & b2 = LModMorphismStr(# b3,b4,b5 #) & b5 is linear )
proof end;

theorem Th18: :: MOD_2:18
for b1 being Ring
for b2, b3 being LModMorphism of b1 st dom b2 = cod b3 holds
ex b4, b5, b6 being LeftMod of b1 st
( b2 is Morphism of b5,b6 & b3 is Morphism of b4,b5 )
proof end;

definition
let c1 be Ring;
let c2, c3 be LModMorphism of c1;
assume E17: dom c2 = cod c3 ;
func c2 * c3 -> strict LModMorphism of a1 means :Def13: :: MOD_2:def 13
for b1, b2, b3 being LeftMod of a1
for b4 being Function of b2,b3
for b5 being Function of b1,b2 st LModMorphismStr(# the Dom of a2,the Cod of a2,the Fun of a2 #) = LModMorphismStr(# b2,b3,b4 #) & LModMorphismStr(# the Dom of a3,the Cod of a3,the Fun of a3 #) = LModMorphismStr(# b1,b2,b5 #) holds
a4 = LModMorphismStr(# b1,b3,(b4 * b5) #);
existence
ex b1 being strict LModMorphism of c1 st
for b2, b3, b4 being LeftMod of c1
for b5 being Function of b3,b4
for b6 being Function of b2,b3 st LModMorphismStr(# the Dom of c2,the Cod of c2,the Fun of c2 #) = LModMorphismStr(# b3,b4,b5 #) & LModMorphismStr(# the Dom of c3,the Cod of c3,the Fun of c3 #) = LModMorphismStr(# b2,b3,b6 #) holds
b1 = LModMorphismStr(# b2,b4,(b5 * b6) #)
proof end;
uniqueness
for b1, b2 being strict LModMorphism of c1 st ( for b3, b4, b5 being LeftMod of c1
for b6 being Function of b4,b5
for b7 being Function of b3,b4 st LModMorphismStr(# the Dom of c2,the Cod of c2,the Fun of c2 #) = LModMorphismStr(# b4,b5,b6 #) & LModMorphismStr(# the Dom of c3,the Cod of c3,the Fun of c3 #) = LModMorphismStr(# b3,b4,b7 #) holds
b1 = LModMorphismStr(# b3,b5,(b6 * b7) #) ) & ( for b3, b4, b5 being LeftMod of c1
for b6 being Function of b4,b5
for b7 being Function of b3,b4 st LModMorphismStr(# the Dom of c2,the Cod of c2,the Fun of c2 #) = LModMorphismStr(# b4,b5,b6 #) & LModMorphismStr(# the Dom of c3,the Cod of c3,the Fun of c3 #) = LModMorphismStr(# b3,b4,b7 #) holds
b2 = LModMorphismStr(# b3,b5,(b6 * b7) #) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines * MOD_2:def 13 :
for b1 being Ring
for b2, b3 being LModMorphism of b1 st dom b2 = cod b3 holds
for b4 being strict LModMorphism of b1 holds
( b4 = b2 * b3 iff for b5, b6, b7 being LeftMod of b1
for b8 being Function of b6,b7
for b9 being Function of b5,b6 st LModMorphismStr(# the Dom of b2,the Cod of b2,the Fun of b2 #) = LModMorphismStr(# b6,b7,b8 #) & LModMorphismStr(# the Dom of b3,the Cod of b3,the Fun of b3 #) = LModMorphismStr(# b5,b6,b9 #) holds
b4 = LModMorphismStr(# b5,b7,(b8 * b9) #) );

theorem Th19: :: MOD_2:19
canceled;

theorem Th20: :: MOD_2:20
for b1 being Ring
for b2, b3, b4 being LeftMod of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b4,b2 holds b5 * b6 is strict Morphism of b4,b3
proof end;

definition
let c1 be Ring;
let c2, c3, c4 be LeftMod of c1;
let c5 be Morphism of c3,c4;
let c6 be Morphism of c2,c3;
func c5 *' c6 -> strict Morphism of a2,a4 equals :: MOD_2:def 14
a5 * a6;
coherence
c5 * c6 is strict Morphism of c2,c4 by Th20;
end;

:: deftheorem Def14 defines *' MOD_2:def 14 :
for b1 being Ring
for b2, b3, b4 being LeftMod of b1
for b5 being Morphism of b3,b4
for b6 being Morphism of b2,b3 holds b5 *' b6 = b5 * b6;

theorem Th21: :: MOD_2:21
for b1 being Ring
for b2, b3, b4 being LeftMod of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b4,b2
for b7 being Function of b2,b3
for b8 being Function of b4,b2 st b5 = LModMorphismStr(# b2,b3,b7 #) & b6 = LModMorphismStr(# b4,b2,b8 #) holds
( b5 *' b6 = LModMorphismStr(# b4,b3,(b7 * b8) #) & b5 * b6 = LModMorphismStr(# b4,b3,(b7 * b8) #) )
proof end;

theorem Th22: :: MOD_2:22
for b1 being Ring
for b2, b3 being strict LModMorphism of b1 st dom b3 = cod b2 holds
ex b4, b5, b6 being LeftMod of b1ex b7 being Function of b4,b5ex b8 being Function of b5,b6 st
( b2 = LModMorphismStr(# b4,b5,b7 #) & b3 = LModMorphismStr(# b5,b6,b8 #) & b3 * b2 = LModMorphismStr(# b4,b6,(b8 * b7) #) )
proof end;

theorem Th23: :: MOD_2:23
for b1 being Ring
for b2, b3 being strict LModMorphism of b1 st dom b3 = cod b2 holds
( dom (b3 * b2) = dom b2 & cod (b3 * b2) = cod b3 )
proof end;

theorem Th24: :: MOD_2:24
for b1 being Ring
for b2, b3, b4, b5 being LeftMod of b1
for b6 being strict Morphism of b2,b3
for b7 being strict Morphism of b3,b4
for b8 being strict Morphism of b4,b5 holds b8 * (b7 * b6) = (b8 * b7) * b6
proof end;

theorem Th25: :: MOD_2:25
for b1 being Ring
for b2, b3, b4 being strict LModMorphism of b1 st dom b4 = cod b3 & dom b3 = cod b2 holds
b4 * (b3 * b2) = (b4 * b3) * b2
proof end;

theorem Th26: :: MOD_2:26
for b1 being Ring
for b2 being LeftMod of b1 holds
( dom (ID b2) = b2 & cod (ID b2) = b2 & ( for b3 being strict LModMorphism of b1 st cod b3 = b2 holds
(ID b2) * b3 = b3 ) & ( for b3 being strict LModMorphism of b1 st dom b3 = b2 holds
b3 * (ID b2) = b3 ) )
proof end;

registration
let c1, c2, c3 be set ;
cluster {a1,a2,a3} -> non empty ;
coherence
not {c1,c2,c3} is empty by ENUMSET1:def 1;
end;

theorem Th27: :: MOD_2:27
canceled;

theorem Th28: :: MOD_2:28
for b1 being Universe
for b2, b3, b4 being Element of b1 holds {b2,b3,b4} is Element of b1
proof end;

theorem Th29: :: MOD_2:29
for b1 being Universe
for b2 being Element of b1 holds succ b2 is Element of b1
proof end;

theorem Th30: :: MOD_2:30
for b1 being Universe holds
( 0 is Element of b1 & 1 is Element of b1 & 2 is Element of b1 )
proof end;

Lemma25: ex b1 being Element of {0,1,2} st b1 = 0
proof end;

Lemma26: ex b1 being Element of {0,1,2} st b1 = 1
proof end;

Lemma27: ex b1 being Element of {0,1,2} st b1 = 2
proof end;

definition
let c1 be Element of {0,1,2};
func - c1 -> Element of {0,1,2} equals :Def15: :: MOD_2:def 15
0 if a1 = 0
2 if a1 = 1
1 if a1 = 2
;
coherence
( ( c1 = 0 implies 0 is Element of {0,1,2} ) & ( c1 = 1 implies 2 is Element of {0,1,2} ) & ( c1 = 2 implies 1 is Element of {0,1,2} ) ) by Lemma26, Lemma27;
consistency
for b1 being Element of {0,1,2} holds
( ( c1 = 0 & c1 = 1 implies ( b1 = 0 iff b1 = 2 ) ) & ( c1 = 0 & c1 = 2 implies ( b1 = 0 iff b1 = 1 ) ) & ( c1 = 1 & c1 = 2 implies ( b1 = 2 iff b1 = 1 ) ) ) ;
let c2 be Element of {0,1,2};
func c1 + c2 -> Element of {0,1,2} equals :Def16: :: MOD_2:def 16
a2 if a1 = 0
a1 if a2 = 0
2 if ( a1 = 1 & a2 = 1 )
0 if ( a1 = 1 & a2 = 2 )
0 if ( a1 = 2 & a2 = 1 )
1 if ( a1 = 2 & a2 = 2 )
;
coherence
( ( c1 = 0 implies c2 is Element of {0,1,2} ) & ( c2 = 0 implies c1 is Element of {0,1,2} ) & ( c1 = 1 & c2 = 1 implies 2 is Element of {0,1,2} ) & ( c1 = 1 & c2 = 2 implies 0 is Element of {0,1,2} ) & ( c1 = 2 & c2 = 1 implies 0 is Element of {0,1,2} ) & ( c1 = 2 & c2 = 2 implies 1 is Element of {0,1,2} ) ) by Lemma25, Lemma26, Lemma27;
consistency
for b1 being Element of {0,1,2} holds
( ( c1 = 0 & c2 = 0 implies ( b1 = c2 iff b1 = c1 ) ) & ( c1 = 0 & c1 = 1 & c2 = 1 implies ( b1 = c2 iff b1 = 2 ) ) & ( c1 = 0 & c1 = 1 & c2 = 2 implies ( b1 = c2 iff b1 = 0 ) ) & ( c1 = 0 & c1 = 2 & c2 = 1 implies ( b1 = c2 iff b1 = 0 ) ) & ( c1 = 0 & c1 = 2 & c2 = 2 implies ( b1 = c2 iff b1 = 1 ) ) & ( c2 = 0 & c1 = 1 & c2 = 1 implies ( b1 = c1 iff b1 = 2 ) ) & ( c2 = 0 & c1 = 1 & c2 = 2 implies ( b1 = c1 iff b1 = 0 ) ) & ( c2 = 0 & c1 = 2 & c2 = 1 implies ( b1 = c1 iff b1 = 0 ) ) & ( c2 = 0 & c1 = 2 & c2 = 2 implies ( b1 = c1 iff b1 = 1 ) ) & ( c1 = 1 & c2 = 1 & c1 = 1 & c2 = 2 implies ( b1 = 2 iff b1 = 0 ) ) & ( c1 = 1 & c2 = 1 & c1 = 2 & c2 = 1 implies ( b1 = 2 iff b1 = 0 ) ) & ( c1 = 1 & c2 = 1 & c1 = 2 & c2 = 2 implies ( b1 = 2 iff b1 = 1 ) ) & ( c1 = 1 & c2 = 2 & c1 = 2 & c2 = 1 implies ( b1 = 0 iff b1 = 0 ) ) & ( c1 = 1 & c2 = 2 & c1 = 2 & c2 = 2 implies ( b1 = 0 iff b1 = 1 ) ) & ( c1 = 2 & c2 = 1 & c1 = 2 & c2 = 2 implies ( b1 = 0 iff b1 = 1 ) ) ) ;
func c1 * c2 -> Element of {0,1,2} equals :Def17: :: MOD_2:def 17
0 if a2 = 0
0 if a1 = 0
a1 if a2 = 1
a2 if a1 = 1
1 if ( a1 = 2 & a2 = 2 )
;
coherence
( ( c2 = 0 implies 0 is Element of {0,1,2} ) & ( c1 = 0 implies 0 is Element of {0,1,2} ) & ( c2 = 1 implies c1 is Element of {0,1,2} ) & ( c1 = 1 implies c2 is Element of {0,1,2} ) & ( c1 = 2 & c2 = 2 implies 1 is Element of {0,1,2} ) ) by Lemma26;
consistency
for b1 being Element of {0,1,2} holds
( ( c2 = 0 & c1 = 0 implies ( b1 = 0 iff b1 = 0 ) ) & ( c2 = 0 & c2 = 1 implies ( b1 = 0 iff b1 = c1 ) ) & ( c2 = 0 & c1 = 1 implies ( b1 = 0 iff b1 = c2 ) ) & ( c2 = 0 & c1 = 2 & c2 = 2 implies ( b1 = 0 iff b1 = 1 ) ) & ( c1 = 0 & c2 = 1 implies ( b1 = 0 iff b1 = c1 ) ) & ( c1 = 0 & c1 = 1 implies ( b1 = 0 iff b1 = c2 ) ) & ( c1 = 0 & c1 = 2 & c2 = 2 implies ( b1 = 0 iff b1 = 1 ) ) & ( c2 = 1 & c1 = 1 implies ( b1 = c1 iff b1 = c2 ) ) & ( c2 = 1 & c1 = 2 & c2 = 2 implies ( b1 = c1 iff b1 = 1 ) ) & ( c1 = 1 & c1 = 2 & c2 = 2 implies ( b1 = c2 iff b1 = 1 ) ) ) ;
end;

:: deftheorem Def15 defines - MOD_2:def 15 :
for b1 being Element of {0,1,2} holds
( ( b1 = 0 implies - b1 = 0 ) & ( b1 = 1 implies - b1 = 2 ) & ( b1 = 2 implies - b1 = 1 ) );

:: deftheorem Def16 defines + MOD_2:def 16 :
for b1, b2 being Element of {0,1,2} holds
( ( b1 = 0 implies b1 + b2 = b2 ) & ( b2 = 0 implies b1 + b2 = b1 ) & ( b1 = 1 & b2 = 1 implies b1 + b2 = 2 ) & ( b1 = 1 & b2 = 2 implies b1 + b2 = 0 ) & ( b1 = 2 & b2 = 1 implies b1 + b2 = 0 ) & ( b1 = 2 & b2 = 2 implies b1 + b2 = 1 ) );

:: deftheorem Def17 defines * MOD_2:def 17 :
for b1, b2 being Element of {0,1,2} holds
( ( b2 = 0 implies b1 * b2 = 0 ) & ( b1 = 0 implies b1 * b2 = 0 ) & ( b2 = 1 implies b1 * b2 = b1 ) & ( b1 = 1 implies b1 * b2 = b2 ) & ( b1 = 2 & b2 = 2 implies b1 * b2 = 1 ) );

definition
func add3 -> BinOp of {0,1,2} means :Def18: :: MOD_2:def 18
for b1, b2 being Element of {0,1,2} holds a1 . b1,b2 = b1 + b2;
existence
ex b1 being BinOp of {0,1,2} st
for b2, b3 being Element of {0,1,2} holds b1 . b2,b3 = b2 + b3
proof end;
uniqueness
for b1, b2 being BinOp of {0,1,2} st ( for b3, b4 being Element of {0,1,2} holds b1 . b3,b4 = b3 + b4 ) & ( for b3, b4 being Element of {0,1,2} holds b2 . b3,b4 = b3 + b4 ) holds
b1 = b2
proof end;
func mult3 -> BinOp of {0,1,2} means :Def19: :: MOD_2:def 19
for b1, b2 being Element of {0,1,2} holds a1 . b1,b2 = b1 * b2;
existence
ex b1 being BinOp of {0,1,2} st
for b2, b3 being Element of {0,1,2} holds b1 . b2,b3 = b2 * b3
proof end;
uniqueness
for b1, b2 being BinOp of {0,1,2} st ( for b3, b4 being Element of {0,1,2} holds b1 . b3,b4 = b3 * b4 ) & ( for b3, b4 being Element of {0,1,2} holds b2 . b3,b4 = b3 * b4 ) holds
b1 = b2
proof end;
func compl3 -> UnOp of {0,1,2} means :Def20: :: MOD_2:def 20
for b1 being Element of {0,1,2} holds a1 . b1 = - b1;
existence
ex b1 being UnOp of {0,1,2} st
for b2 being Element of {0,1,2} holds b1 . b2 = - b2
proof end;
uniqueness
for b1, b2 being UnOp of {0,1,2} st ( for b3 being Element of {0,1,2} holds b1 . b3 = - b3 ) & ( for b3 being Element of {0,1,2} holds b2 . b3 = - b3 ) holds
b1 = b2
proof end;
func unit3 -> Element of {0,1,2} equals :: MOD_2:def 21
1;
coherence
1 is Element of {0,1,2} by ENUMSET1:def 1;
func zero3 -> Element of {0,1,2} equals :: MOD_2:def 22
0;
coherence
0 is Element of {0,1,2} by ENUMSET1:def 1;
end;

:: deftheorem Def18 defines add3 MOD_2:def 18 :
for b1 being BinOp of {0,1,2} holds
( b1 = add3 iff for b2, b3 being Element of {0,1,2} holds b1 . b2,b3 = b2 + b3 );

:: deftheorem Def19 defines mult3 MOD_2:def 19 :
for b1 being BinOp of {0,1,2} holds
( b1 = mult3 iff for b2, b3 being Element of {0,1,2} holds b1 . b2,b3 = b2 * b3 );

:: deftheorem Def20 defines compl3 MOD_2:def 20 :
for b1 being UnOp of {0,1,2} holds
( b1 = compl3 iff for b2 being Element of {0,1,2} holds b1 . b2 = - b2 );

:: deftheorem Def21 defines unit3 MOD_2:def 21 :
unit3 = 1;

:: deftheorem Def22 defines zero3 MOD_2:def 22 :
zero3 = 0;

definition
func Z3 -> strict doubleLoopStr equals :Def23: :: MOD_2:def 23
 doubleLoopStr(# {0,1,2},add3 ,mult3 ,unit3 ,zero3 #);
coherence
doubleLoopStr(# {0,1,2},add3 ,mult3 ,unit3 ,zero3 #) is strict doubleLoopStr ;
end;

:: deftheorem Def23 defines Z3 MOD_2:def 23 :
Z3 = doubleLoopStr(# {0,1,2},add3 ,mult3 ,unit3 ,zero3 #);

registration
cluster Z3 -> non empty strict ;
coherence
not Z3 is empty
proof end;
end;

E35: now
let c1, c2 be Element of Z3 ;
assume E36: c2 = 1 ;
reconsider c3 = c2, c4 = c1 as Element of {0,1,2} ;
thus c1 * c2 = mult3 . c1,c2
.= c4 * c3 by Def19
.= c1 by E36, Def17 ;
thus c2 * c1 = mult3 . c2,c1
.= c3 * c4 by Def19
.= c1 by E36, Def17 ;
end;

registration
cluster Z3 -> non empty unital strict ;
coherence
Z3 is unital
proof end;
end;

Lemma36: 1. Z3 = 1
proof end;

theorem Th31: :: MOD_2:31
canceled;

theorem Th32: :: MOD_2:32
( 0. Z3 = 0 & 1. Z3 = 1 & 0. Z3 is Element of {0,1,2} & 1. Z3 is Element of {0,1,2} & the add of Z3 = add3 & the mult of Z3 = mult3 ) by Lemma36;

Lemma38: for b1, b2 being Scalar of Z3
for b3, b4 being Element of {0,1,2} st b3 = b1 & b4 = b2 holds
( b1 + b2 = b3 + b4 & b1 * b2 = b3 * b4 )
proof end;

Lemma39: for b1, b2, b3 being Scalar of Z3
for b4, b5, b6 being Element of {0,1,2} st b4 = b1 & b5 = b2 & b6 = b3 holds
( (b1 + b2) + b3 = (b4 + b5) + b6 & b1 + (b2 + b3) = b4 + (b5 + b6) & (b1 * b2) * b3 = (b4 * b5) * b6 & b1 * (b2 * b3) = b4 * (b5 * b6) )
proof end;

Lemma40: for b1, b2, b3, b4 being Element of {0,1,2} st b4 = 0 holds
( b1 + (- b1) = b4 & b1 + b4 = b1 & (b1 + b2) + b3 = b1 + (b2 + b3) )
proof end;

registration
cluster Z3 -> non empty add-associative right_zeroed right_complementable unital strict ;
coherence
( Z3 is add-associative & Z3 is right_zeroed & Z3 is right_complementable )
proof end;
end;

theorem Th33: :: MOD_2:33
for b1, b2 being Scalar of Z3
for b3, b4 being Element of {0,1,2} st b3 = b1 & b4 = b2 holds
( b1 + b2 = b3 + b4 & b1 * b2 = b3 * b4 & - b1 = - b3 )
proof end;

theorem Th34: :: MOD_2:34
for b1, b2, b3 being Scalar of Z3
for b4, b5, b6 being Element of {0,1,2} st b4 = b1 & b5 = b2 & b6 = b3 holds
( (b1 + b2) + b3 = (b4 + b5) + b6 & b1 + (b2 + b3) = b4 + (b5 + b6) & (b1 * b2) * b3 = (b4 * b5) * b6 & b1 * (b2 * b3) = b4 * (b5 * b6) )
proof end;

theorem Th35: :: MOD_2:35
for b1, b2, b3, b4, b5 being Element of {0,1,2} st b4 = 0 & b5 = 1 holds
( b1 + b2 = b2 + b1 & (b1 + b2) + b3 = b1 + (b2 + b3) & b1 + b4 = b1 & b1 + (- b1) = b4 & b1 * b2 = b2 * b1 & (b1 * b2) * b3 = b1 * (b2 * b3) & b5 * b1 = b1 & ( b1 <> b4 implies ex b6 being Element of {0,1,2} st b1 * b6 = b5 ) & b4 <> b5 & b1 * (b2 + b3) = (b1 * b2) + (b1 * b3) )
proof end;

theorem Th36: :: MOD_2:36
for b1 being non empty doubleLoopStr st ( for b2, b3, b4 being Scalar of b1 holds
( b2 + b3 = b3 + b2 & (b2 + b3) + b4 = b2 + (b3 + b4) & b2 + (0. b1) = b2 & b2 + (- b2) = 0. b1 & b2 * b3 = b3 * b2 & (b2 * b3) * b4 = b2 * (b3 * b4) & (1. b1) * b2 = b2 & ( b2 <> 0. b1 implies ex b5 being Scalar of b1 st b2 * b5 = 1. b1 ) & 0. b1 <> 1. b1 & b2 * (b3 + b4) = (b2 * b3) + (b2 * b4) ) ) holds
b1 is Field
proof end;

theorem Th37: :: MOD_2:37
Z3 is Fanoian Field
proof end;

registration
cluster Z3 -> non empty Abelian add-associative right_zeroed right_complementable unital associative commutative strict distributive left_unital Field-like Fanoian ;
coherence
( Z3 is Fanoian & Z3 is add-associative & Z3 is right_zeroed & Z3 is right_complementable & Z3 is Abelian & Z3 is commutative & Z3 is associative & Z3 is left_unital & Z3 is distributive & Z3 is Field-like ) by Th37;
end;

Lemma46: for b1 being Universe holds the carrier of Z3 in b1
proof end;

theorem Th38: :: MOD_2:38
for b1, b2 being non empty set
for b3 being Universe
for b4 being Function of b1,b2 st b1 in b3 & b2 in b3 holds
b4 in b3
proof end;

Lemma48: for b1 being non empty set
for b2 being Universe holds
( ( for b3 being BinOp of b1 st b1 in b2 holds
b3 in b2 ) & ( for b3 being UnOp of b1 st b1 in b2 holds
b3 in b2 ) )
proof end;

theorem Th39: :: MOD_2:39
canceled;

theorem Th40: :: MOD_2:40
for b1 being Universe holds
( the carrier of Z3 in b1 & the add of Z3 is Element of b1 & comp Z3 is Element of b1 & the Zero of Z3 is Element of b1 & the mult of Z3 is Element of b1 & the unity of Z3 is Element of b1 )
proof end;