:: Rings and Modules - Part II
:: by Michal Muzalewski
::
:: Received October 18, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

Lm1:  for R being Ring holds VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is strict LeftMod of R
proofend;

definition
let R be Ring;
func TrivialLMod R ->  strict LeftMod of R equals :: MOD_2:def 1
 VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #);
coherence
 VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is strict LeftMod of R by Lm1;
end;

:: deftheorem  defines TrivialLMod MOD_2:def_1_:_
 for R being Ring holds TrivialLMod R = VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #);

theorem :: MOD_2:1
for R being Ring
for x being Vector of (TrivialLMod R) holds x = 0. (TrivialLMod R) by GRCAT_1:4;

definition
let R be non empty multMagma ;
let G, H be non empty VectSpStr over R;
let f be Function of G,H;
attrf is homogeneous  means :Def2: :: MOD_2:def 2
 for a being Scalar of R
for x being Vector of G holds f . (a * x) = a * (f . x);
end;

:: deftheorem Def2 defines homogeneous MOD_2:def_2_:_
 for R being non empty multMagma
for G, H being non empty VectSpStr over R
for f being Function of G,H holds
( f is homogeneous iff for a being Scalar of R
for x being Vector of G holds f . (a * x) = a * (f . x) );

theorem Th2: :: MOD_2:2
for R being Ring
for G, H, S being non empty VectSpStr over R
for f being Function of G,H
for g being Function of H,S st f is homogeneous & g is homogeneous holds
g * f is homogeneous
proofend;

registration
let R be Ring;
let G, H be LeftMod of R;
cluster ZeroMap (G,H) ->  homogeneous ;
coherence
 ZeroMap (G,H) is homogeneous
proofend;
end;

definition
let R be Ring;
attrc2 is strict ;
struct LModMorphismStr over R -> ;
aggrLModMorphismStr(# Dom, Cod, Fun #) ->  LModMorphismStr over R;
sel Dom c2 ->  LeftMod of R;
sel Cod c2 ->  LeftMod of R;
sel Fun c2 ->  Function of the Dom of c2, the Cod of c2;
end;

definition
let R be Ring;
let f be LModMorphismStr over R;
func dom f ->  LeftMod of R equals :: MOD_2:def 3
 the Dom of f;
correctness
coherence
the Dom of f is LeftMod of R;
;
func cod f ->  LeftMod of R equals :: MOD_2:def 4
 the Cod of f;
correctness
coherence
the Cod of f is LeftMod of R;
;
end;

:: deftheorem  defines dom MOD_2:def_3_:_
 for R being Ring
for f being LModMorphismStr over R holds dom f = the Dom of f;

:: deftheorem  defines cod MOD_2:def_4_:_
 for R being Ring
for f being LModMorphismStr over R holds cod f = the Cod of f;

definition
let R be Ring;
let f be LModMorphismStr over R;
func fun f ->  Function of (dom f),(cod f) equals :: MOD_2:def 5
 the Fun of f;
coherence
 the Fun of f is Function of (dom f),(cod f) ;
end;

:: deftheorem  defines fun MOD_2:def_5_:_
 for R being Ring
for f being LModMorphismStr over R holds fun f = the Fun of f;

theorem :: MOD_2:3
for R being Ring
for G1, G2 being LeftMod of R
for f being LModMorphismStr over R
for f0 being Function of G1,G2 st f = LModMorphismStr(# G1,G2,f0 #) holds
( dom f = G1 & cod f = G2 & fun f = f0 ) ;

definition
let R be Ring;
let G, H be LeftMod of R;
func ZERO (G,H) ->  strict LModMorphismStr over R equals :: MOD_2:def 6
 LModMorphismStr(# G,H,(ZeroMap (G,H)) #);
correctness
coherence
LModMorphismStr(# G,H,(ZeroMap (G,H)) #) is strict LModMorphismStr over R;
;
end;

:: deftheorem  defines ZERO MOD_2:def_6_:_
 for R being Ring
for G, H being LeftMod of R holds ZERO (G,H) = LModMorphismStr(# G,H,(ZeroMap (G,H)) #);

definition
let R be Ring;
let IT be LModMorphismStr over R;
attrIT is LModMorphism-like  means :Def7: :: MOD_2:def 7
( fun IT is additive & fun IT is homogeneous );
end;

:: deftheorem Def7 defines LModMorphism-like MOD_2:def_7_:_
 for R being Ring
for IT being LModMorphismStr over R holds
( IT is LModMorphism-like iff ( fun IT is additive & fun IT is homogeneous ) );

registration
let R be Ring;
cluster strict LModMorphism-like for LModMorphismStr over R;
existence
 ex b1 being LModMorphismStr over R st
( b1 is strict & b1 is LModMorphism-like )
proofend;
end;

definition
let R be Ring;
mode LModMorphism of R is LModMorphism-like LModMorphismStr over R;
end;

theorem Th4: :: MOD_2:4
for R being Ring
for F being LModMorphism of R holds
( the Fun of F is additive & the Fun of F is homogeneous )
proofend;

registration
let R be Ring;
let G, H be LeftMod of R;
cluster ZERO (G,H) ->  strict LModMorphism-like ;
coherence
 ZERO (G,H) is LModMorphism-like
proofend;
end;

definition
let R be Ring;
let G, H be LeftMod of R;
mode Morphism of G,H ->  LModMorphism of R means :Def8: :: MOD_2:def 8
( dom it = G & cod it = H );
existence
 ex b1 being LModMorphism of R st
( dom b1 = G & cod b1 = H )
proofend;
end;

:: deftheorem Def8 defines Morphism MOD_2:def_8_:_
 for R being Ring
for G, H being LeftMod of R
for b4 being LModMorphism of R holds
( b4 is Morphism of G,H iff ( dom b4 = G & cod b4 = H ) );

registration
let R be Ring;
let G, H be LeftMod of R;
cluster strict LModMorphism-like for Morphism of G,H;
existence
 ex b1 being Morphism of G,H st b1 is strict
proofend;
end;

theorem Th5: :: MOD_2:5
for R being Ring
for G, H being LeftMod of R
for f being LModMorphismStr over R st dom f = G & cod f = H & fun f is additive & fun f is homogeneous holds
f is Morphism of G,H
proofend;

theorem Th6: :: MOD_2:6
for R being Ring
for G, H being LeftMod of R
for f being Function of G,H st f is additive & f is homogeneous holds
LModMorphismStr(# G,H,f #) is strict Morphism of G,H
proofend;

registration
let R be Ring;
let G be LeftMod of R;
cluster id G ->  homogeneous ;
coherence
 id G is homogeneous
proofend;
end;

definition
let R be Ring;
let G be LeftMod of R;
func ID G ->  strict Morphism of G,G equals :: MOD_2:def 9
 LModMorphismStr(# G,G,(id G) #);
coherence
 LModMorphismStr(# G,G,(id G) #) is strict Morphism of G,G
proofend;
end;

:: deftheorem  defines ID MOD_2:def_9_:_
 for R being Ring
for G being LeftMod of R holds ID G = LModMorphismStr(# G,G,(id G) #);

definition
let R be Ring;
let G, H be LeftMod of R;
:: original:ZERO
redefine func ZERO (G,H) ->  strict Morphism of G,H;
coherence
 ZERO (G,H) is strict Morphism of G,H
proofend;
end;

theorem Th7: :: MOD_2:7
for R being Ring
for G, H being LeftMod of R
for F being Morphism of G,H ex f being Function of G,H st
( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
proofend;

theorem Th8: :: MOD_2:8
for R being Ring
for G, H being LeftMod of R
for F being strict Morphism of G,H ex f being Function of G,H st F = LModMorphismStr(# G,H,f #)
proofend;

theorem Th9: :: MOD_2:9
for R being Ring
for F being LModMorphism of R ex G, H being LeftMod of R st F is Morphism of G,H
proofend;

theorem :: MOD_2:10
for R being Ring
for F being strict LModMorphism of R ex G, H being LeftMod of R ex f being Function of G,H st
( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
proofend;

theorem Th11: :: MOD_2:11
for R being Ring
for g, f being LModMorphism of R st dom g = cod f holds
ex G1, G2, G3 being LeftMod of R st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
proofend;

definition
let R be Ring;
let G, F be LModMorphism of R;
assume A1: dom G = cod F ;
funcG * F ->  strict LModMorphism of R means :Def10: :: MOD_2:def 10
 for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
it = LModMorphismStr(# G1,G3,(g * f) #);
existence
 ex b1 being strict LModMorphism of R st
for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
b1 = LModMorphismStr(# G1,G3,(g * f) #)
proofend;
uniqueness
 for b1, b2 being strict LModMorphism of R st ( for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
b1 = LModMorphismStr(# G1,G3,(g * f) #) ) & ( for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
b2 = LModMorphismStr(# G1,G3,(g * f) #) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines * MOD_2:def_10_:_
 for R being Ring
for G, F being LModMorphism of R st dom G = cod F holds
for b4 being strict LModMorphism of R holds
( b4 = G * F iff for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
b4 = LModMorphismStr(# G1,G3,(g * f) #) );

theorem Th12: :: MOD_2:12
for R being Ring
for G2, G3, G1 being LeftMod of R
for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G * F is strict Morphism of G1,G3
proofend;

definition
let R be Ring;
let G1, G2, G3 be LeftMod of R;
let G be Morphism of G2,G3;
let F be Morphism of G1,G2;
funcG *' F ->  strict Morphism of G1,G3 equals :: MOD_2:def 11
G * F;
coherence
 G * F is strict Morphism of G1,G3 by Th12;
end;

:: deftheorem  defines *' MOD_2:def_11_:_
 for R being Ring
for G1, G2, G3 being LeftMod of R
for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G *' F = G * F;

theorem Th13: :: MOD_2:13
for R being Ring
for G2, G3, G1 being LeftMod of R
for G being Morphism of G2,G3
for F being Morphism of G1,G2
for g being Function of G2,G3
for f being Function of G1,G2 st G = LModMorphismStr(# G2,G3,g #) & F = LModMorphismStr(# G1,G2,f #) holds
( G *' F = LModMorphismStr(# G1,G3,(g * f) #) & G * F = LModMorphismStr(# G1,G3,(g * f) #) )
proofend;

theorem Th14: :: MOD_2:14
for R being Ring
for f, g being strict LModMorphism of R st dom g = cod f holds
ex G1, G2, G3 being LeftMod of R ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = LModMorphismStr(# G1,G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# G1,G3,(g0 * f0) #) )
proofend;

theorem :: MOD_2:15
for R being Ring
for f, g being strict LModMorphism of R st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g )
proofend;

theorem Th16: :: MOD_2:16
for R being Ring
for G1, G2, G3, G4 being LeftMod of R
for f being strict Morphism of G1,G2
for g being strict Morphism of G2,G3
for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f
proofend;

theorem :: MOD_2:17
for R being Ring
for f, g, h being strict LModMorphism of R st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f
proofend;

theorem :: MOD_2:18
for R being Ring
for G being LeftMod of R holds
( dom (ID G) = G & cod (ID G) = G & ( for f being strict LModMorphism of R st cod f = G holds
(ID G) * f = f ) & ( for g being strict LModMorphism of R st dom g = G holds
g * (ID G) = g ) )
proofend;

theorem Th19: :: MOD_2:19
for UN being Universe
for u, v, w being Element of UN holds {u,v,w} is Element of UN
proofend;

theorem Th20: :: MOD_2:20
for UN being Universe
for u being Element of UN holds succ u is Element of UN
proofend;

theorem Th21: :: MOD_2:21
for UN being Universe holds
( 0 is Element of UN & 1 is Element of UN & 2 is Element of UN )
proofend;

Lm2:  ex c being Element of {0,1,2} st c = 0
proofend;

Lm3:  ex c being Element of {0,1,2} st c = 1
proofend;

Lm4:  ex c being Element of {0,1,2} st c = 2
proofend;

definition
let a be Element of {0,1,2};
func - a ->  Element of {0,1,2} equals :Def12: :: MOD_2:def 12
 0  if a = 0
2 if a = 1
1 if a = 2
;
coherence
 ( ( a = 0 implies 0 is Element of {0,1,2} ) & ( a = 1 implies 2 is Element of {0,1,2} ) & ( a = 2 implies 1 is Element of {0,1,2} ) ) by Lm3, Lm4;
consistency
 for b1 being Element of {0,1,2} holds
( ( a = 0 & a = 1 implies ( b1 = 0 iff b1 = 2 ) ) & ( a = 0 & a = 2 implies ( b1 = 0 iff b1 = 1 ) ) & ( a = 1 & a = 2 implies ( b1 = 2 iff b1 = 1 ) ) ) ;
let b be Element of {0,1,2};
funca + b ->  Element of {0,1,2} equals :Def13: :: MOD_2:def 13
b if a = 0
a if b = 0
2 if ( a = 1 & b = 1 )
0  if ( a = 1 & b = 2 )
0  if ( a = 2 & b = 1 )
1 if ( a = 2 & b = 2 )
;
coherence
 ( ( a = 0 implies b is Element of {0,1,2} ) & ( b = 0 implies a is Element of {0,1,2} ) & ( a = 1 & b = 1 implies 2 is Element of {0,1,2} ) & ( a = 1 & b = 2 implies 0 is Element of {0,1,2} ) & ( a = 2 & b = 1 implies 0 is Element of {0,1,2} ) & ( a = 2 & b = 2 implies 1 is Element of {0,1,2} ) ) by Lm2, Lm3, Lm4;
consistency
 for b1 being Element of {0,1,2} holds
( ( a = 0 & b = 0 implies ( b1 = b iff b1 = a ) ) & ( a = 0 & a = 1 & b = 1 implies ( b1 = b iff b1 = 2 ) ) & ( a = 0 & a = 1 & b = 2 implies ( b1 = b iff b1 = 0 ) ) & ( a = 0 & a = 2 & b = 1 implies ( b1 = b iff b1 = 0 ) ) & ( a = 0 & a = 2 & b = 2 implies ( b1 = b iff b1 = 1 ) ) & ( b = 0 & a = 1 & b = 1 implies ( b1 = a iff b1 = 2 ) ) & ( b = 0 & a = 1 & b = 2 implies ( b1 = a iff b1 = 0 ) ) & ( b = 0 & a = 2 & b = 1 implies ( b1 = a iff b1 = 0 ) ) & ( b = 0 & a = 2 & b = 2 implies ( b1 = a iff b1 = 1 ) ) & ( a = 1 & b = 1 & a = 1 & b = 2 implies ( b1 = 2 iff b1 = 0 ) ) & ( a = 1 & b = 1 & a = 2 & b = 1 implies ( b1 = 2 iff b1 = 0 ) ) & ( a = 1 & b = 1 & a = 2 & b = 2 implies ( b1 = 2 iff b1 = 1 ) ) & ( a = 1 & b = 2 & a = 2 & b = 1 implies ( b1 = 0 iff b1 = 0 ) ) & ( a = 1 & b = 2 & a = 2 & b = 2 implies ( b1 = 0 iff b1 = 1 ) ) & ( a = 2 & b = 1 & a = 2 & b = 2 implies ( b1 = 0 iff b1 = 1 ) ) ) ;
funca * b ->  Element of {0,1,2} equals :Def14: :: MOD_2:def 14
 0  if b = 0
0  if a = 0
a if b = 1
b if a = 1
1 if ( a = 2 & b = 2 )
;
coherence
 ( ( b = 0 implies 0 is Element of {0,1,2} ) & ( a = 0 implies 0 is Element of {0,1,2} ) & ( b = 1 implies a is Element of {0,1,2} ) & ( a = 1 implies b is Element of {0,1,2} ) & ( a = 2 & b = 2 implies 1 is Element of {0,1,2} ) ) by Lm3;
consistency
 for b1 being Element of {0,1,2} holds
( ( b = 0 & a = 0 implies ( b1 = 0 iff b1 = 0 ) ) & ( b = 0 & b = 1 implies ( b1 = 0 iff b1 = a ) ) & ( b = 0 & a = 1 implies ( b1 = 0 iff b1 = b ) ) & ( b = 0 & a = 2 & b = 2 implies ( b1 = 0 iff b1 = 1 ) ) & ( a = 0 & b = 1 implies ( b1 = 0 iff b1 = a ) ) & ( a = 0 & a = 1 implies ( b1 = 0 iff b1 = b ) ) & ( a = 0 & a = 2 & b = 2 implies ( b1 = 0 iff b1 = 1 ) ) & ( b = 1 & a = 1 implies ( b1 = a iff b1 = b ) ) & ( b = 1 & a = 2 & b = 2 implies ( b1 = a iff b1 = 1 ) ) & ( a = 1 & a = 2 & b = 2 implies ( b1 = b iff b1 = 1 ) ) ) ;
end;

:: deftheorem Def12 defines - MOD_2:def_12_:_
 for a being Element of {0,1,2} holds
( ( a = 0 implies - a = 0 ) & ( a = 1 implies - a = 2 ) & ( a = 2 implies - a = 1 ) );

:: deftheorem Def13 defines + MOD_2:def_13_:_
 for a, b being Element of {0,1,2} holds
( ( a = 0 implies a + b = b ) & ( b = 0 implies a + b = a ) & ( a = 1 & b = 1 implies a + b = 2 ) & ( a = 1 & b = 2 implies a + b = 0 ) & ( a = 2 & b = 1 implies a + b = 0 ) & ( a = 2 & b = 2 implies a + b = 1 ) );

:: deftheorem Def14 defines * MOD_2:def_14_:_
 for a, b being Element of {0,1,2} holds
( ( b = 0 implies a * b = 0 ) & ( a = 0 implies a * b = 0 ) & ( b = 1 implies a * b = a ) & ( a = 1 implies a * b = b ) & ( a = 2 & b = 2 implies a * b = 1 ) );

definition
func add3  ->  BinOp of {0,1,2} means :Def15: :: MOD_2:def 15
 for a, b being Element of {0,1,2} holds it . (a,b) = a + b;
existence
 ex b1 being BinOp of {0,1,2} st
for a, b being Element of {0,1,2} holds b1 . (a,b) = a + b
proofend;
uniqueness
 for b1, b2 being BinOp of {0,1,2} st ( for a, b being Element of {0,1,2} holds b1 . (a,b) = a + b ) & ( for a, b being Element of {0,1,2} holds b2 . (a,b) = a + b ) holds
b1 = b2
proofend;
func mult3  ->  BinOp of {0,1,2} means :Def16: :: MOD_2:def 16
 for a, b being Element of {0,1,2} holds it . (a,b) = a * b;
existence
 ex b1 being BinOp of {0,1,2} st
for a, b being Element of {0,1,2} holds b1 . (a,b) = a * b
proofend;
uniqueness
 for b1, b2 being BinOp of {0,1,2} st ( for a, b being Element of {0,1,2} holds b1 . (a,b) = a * b ) & ( for a, b being Element of {0,1,2} holds b2 . (a,b) = a * b ) holds
b1 = b2
proofend;
func compl3  ->  UnOp of {0,1,2} means :Def17: :: MOD_2:def 17
 for a being Element of {0,1,2} holds it . a = - a;
existence
 ex b1 being UnOp of {0,1,2} st
for a being Element of {0,1,2} holds b1 . a = - a
proofend;
uniqueness
 for b1, b2 being UnOp of {0,1,2} st ( for a being Element of {0,1,2} holds b1 . a = - a ) & ( for a being Element of {0,1,2} holds b2 . a = - a ) holds
b1 = b2
proofend;
func unit3  ->  Element of {0,1,2} equals :: MOD_2:def 18
1;
coherence
 1 is Element of {0,1,2} by ENUMSET1:def_1;
func zero3  ->  Element of {0,1,2} equals :: MOD_2:def 19
 0 ;
coherence
 0 is Element of {0,1,2} by ENUMSET1:def_1;
end;

:: deftheorem Def15 defines add3 MOD_2:def_15_:_
 for b1 being BinOp of {0,1,2} holds
( b1 = add3 iff for a, b being Element of {0,1,2} holds b1 . (a,b) = a + b );

:: deftheorem Def16 defines mult3 MOD_2:def_16_:_
 for b1 being BinOp of {0,1,2} holds
( b1 = mult3 iff for a, b being Element of {0,1,2} holds b1 . (a,b) = a * b );

:: deftheorem Def17 defines compl3 MOD_2:def_17_:_
 for b1 being UnOp of {0,1,2} holds
( b1 = compl3 iff for a being Element of {0,1,2} holds b1 . a = - a );

:: deftheorem  defines unit3 MOD_2:def_18_:_
 unit3 = 1;

:: deftheorem  defines zero3 MOD_2:def_19_:_
 zero3 = 0 ;

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

:: deftheorem Def20 defines Z_3 MOD_2:def_20_:_
 Z_3 = doubleLoopStr(# {0,1,2},add3,mult3,unit3,zero3 #);

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

Lm5: now__::_thesis:_for_h,_e_being_Element_of_Z_3_st_e_=_1_holds_
(_h_*_e_=_h_&_e_*_h_=_h_)
let h, e be Element of Z_3; ::_thesis: ( e = 1 implies ( h * e = h & e * h = h ) )
assume A1: e = 1 ; ::_thesis: ( h * e = h & e * h = h )
reconsider a = e, b = h as Element of {0,1,2} ;
thus h * e = b * a by Def16
.= h by A1, Def14 ; ::_thesis: e * h = h
thus e * h = a * b by Def16
.= h by A1, Def14 ; ::_thesis: verum
end;

registration
cluster Z_3  ->  strict well-unital ;
coherence
 Z_3 is well-unital
proofend;
end;

theorem Th22: :: MOD_2:22
( 0. Z_3 = 0 & 1. Z_3 = 1 & 0. Z_3 is Element of {0,1,2} & 1. Z_3 is Element of {0,1,2} & the addF of Z_3 = add3 & the multF of Z_3 = mult3 ) ;

Lm6:  for x, y, z being Scalar of Z_3
for X, Y, Z being Element of {0,1,2} st X = x & Y = y & Z = z holds
( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) )
proofend;

Lm7:  for x, y, z, a being Element of {0,1,2} st a = 0 holds
( x + (- x) = a & x + a = x & (x + y) + z = x + (y + z) )
proofend;

registration
cluster Z_3  ->  right_complementable strict add-associative right_zeroed ;
coherence
 ( Z_3 is add-associative & Z_3 is right_zeroed & Z_3 is right_complementable )
proofend;
end;

theorem Th23: :: MOD_2:23
for x, y being Scalar of Z_3
for X, Y being Element of {0,1,2} st X = x & Y = y holds
( x + y = X + Y & x * y = X * Y & - x = - X )
proofend;

theorem Th24: :: MOD_2:24
for x, y, z being Scalar of Z_3
for X, Y, Z being Element of {0,1,2} st X = x & Y = y & Z = z holds
( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) )
proofend;

theorem Th25: :: MOD_2:25
for x, y, z, a, b being Element of {0,1,2} st a = 0 & b = 1 holds
( x + y = y + x &amp; (x + y) + z = x + (y + z) &amp; x + a = x &amp; x + (- x) = a &amp; x * y = y * x &amp; (x * y) * z = x * (y * z) &amp; b * x = x &amp; ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) &amp; a <> b &amp; x * (y + z) = (x * y) + (x * z) )
proofend;

theorem Th26: :: MOD_2:26
for F being non empty doubleLoopStr st ( for x, y, z being Scalar of F holds
( x + y = y + x &amp; (x + y) + z = x + (y + z) &amp; x + (0. F) = x &amp; x + (- x) = 0. F &amp; x * y = y * x &amp; (x * y) * z = x * (y * z) &amp; (1. F) * x = x &amp; x * (1. F) = x &amp; ( x <> 0. F implies ex y being Scalar of F st x * y = 1. F ) &amp; 0. F <> 1. F &amp; x * (y + z) = (x * y) + (x * z) ) ) holds
F is Field
proofend;

theorem Th27: :: MOD_2:27
Z_3 is Fanoian Field
proofend;

registration
cluster Z_3  ->  right_complementable almost_left_invertible strict associative commutative well-unital distributive Fanoian Abelian add-associative right_zeroed ;
coherence
 ( Z_3 is Fanoian &amp; Z_3 is add-associative &amp; Z_3 is right_zeroed &amp; Z_3 is right_complementable &amp; Z_3 is Abelian &amp; Z_3 is commutative &amp; Z_3 is associative &amp; Z_3 is well-unital &amp; Z_3 is distributive &amp; Z_3 is almost_left_invertible ) by Th27;
end;

Lm8:  for UN being Universe holds the carrier of Z_3 in UN
proofend;

theorem Th28: :: MOD_2:28
for D, D9 being non empty set
for UN being Universe
for f being Function of D,D9 st D in UN &amp; D9 in UN holds
f in UN
proofend;

Lm9:  for D being non empty set
for UN being Universe holds
( ( for f being BinOp of D st D in UN holds
f in UN ) &amp; ( for f being UnOp of D st D in UN holds
f in UN ) )
proofend;

theorem :: MOD_2:29
for UN being Universe holds
( the carrier of Z_3 in UN &amp; the addF of Z_3 in UN &amp; comp Z_3 in UN &amp; 0. Z_3 in UN &amp; the multF of Z_3 in UN &amp; 1. Z_3 in UN )
proofend;