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

proof end;

definition

let R be Ring;

VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is strict LeftMod of R by Lm1;

end;
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)) #);

VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is strict LeftMod of R by Lm1;

:: deftheorem defines TrivialLMod MOD_2:def 1 :

for R being Ring holds TrivialLMod R = VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #);

for R being Ring holds TrivialLMod R = VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #);

theorem :: MOD_2:1

definition

let R be non empty multMagma ;

let G, H be non empty VectSpStr over R;

let f be Function of G,H;

end;
let G, H be non empty VectSpStr over R;

let f be Function of G,H;

attr f 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);

for a being Scalar of R

for x being Vector of G holds f . (a * x) = a * (f . x);

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

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

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

proof end;

registration
end;

definition

let R be Ring;

attr c_{2} is strict ;

struct LModMorphismStr over R -> ;

aggr LModMorphismStr(# Dom, Cod, Fun #) -> LModMorphismStr over R;

sel Dom c_{2} -> LeftMod of R;

sel Cod c_{2} -> LeftMod of R;

sel Fun c_{2} -> Function of the Dom of c_{2}, the Cod of c_{2};

end;
attr c

struct LModMorphismStr over R -> ;

aggr LModMorphismStr(# Dom, Cod, Fun #) -> LModMorphismStr over R;

sel Dom c

sel Cod c

sel Fun c

definition

let R be Ring;

let f be LModMorphismStr over R;

correctness

coherence

the Dom of f is LeftMod of R;

;

correctness

coherence

the Cod of f is LeftMod of R;

;

end;
let f be LModMorphismStr over R;

correctness

coherence

the Dom of f is LeftMod of R;

;

correctness

coherence

the Cod of f is LeftMod of R;

;

:: deftheorem defines dom MOD_2:def 3 :

for R being Ring

for f being LModMorphismStr over R holds dom f = the Dom of f;

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;

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;

coherence

the Fun of f is Function of (dom f),(cod f) ;

end;
let f be LModMorphismStr over R;

coherence

the Fun of f is Function of (dom f),(cod f) ;

:: deftheorem defines fun MOD_2:def 5 :

for R being Ring

for f being LModMorphismStr over R holds fun f = the Fun of f;

for R being Ring

for f being LModMorphismStr over R holds fun f = the Fun of f;

theorem :: MOD_2:3

definition

let R be Ring;

let G, H be LeftMod of R;

coherence

LModMorphismStr(# G,H,(ZeroMap (G,H)) #) is strict LModMorphismStr over R;

;

end;
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 LModMorphismStr(# G,H,(ZeroMap (G,H)) #);

coherence

LModMorphismStr(# G,H,(ZeroMap (G,H)) #) is strict LModMorphismStr over R;

;

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

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;

end;
let IT be LModMorphismStr over R;

attr IT is LModMorphism-like means :Def7: :: MOD_2:def 7

( fun IT is additive & fun IT is homogeneous );

( fun IT is additive & fun IT is homogeneous );

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

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;

existence

ex b_{1} being LModMorphismStr over R st

( b_{1} is strict & b_{1} is LModMorphism-like )

end;
existence

ex b

( b

proof 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 )

for F being LModMorphism of R holds

( the Fun of F is additive & the Fun of F is homogeneous )

proof end;

registration
end;

definition

let R be Ring;

let G, H be LeftMod of R;

existence

ex b_{1} being LModMorphism of R st

( dom b_{1} = G & cod b_{1} = H )

end;
let G, H be LeftMod of R;

existence

ex b

( dom b

proof end;

:: deftheorem Def8 defines Morphism MOD_2:def 8 :

for R being Ring

for G, H being LeftMod of R

for b_{4} being LModMorphism of R holds

( b_{4} is Morphism of G,H iff ( dom b_{4} = G & cod b_{4} = H ) );

for R being Ring

for G, H being LeftMod of R

for b

( b

registration

let R be Ring;

let G, H be LeftMod of R;

existence

ex b_{1} being Morphism of G,H st b_{1} is strict

end;
let G, H be LeftMod of R;

existence

ex b

proof 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

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

proof end;

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

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

proof end;

definition

let R be Ring;

let G be LeftMod of R;

coherence

LModMorphismStr(# G,G,(id G) #) is strict Morphism of G,G

end;
let G be LeftMod of R;

coherence

LModMorphismStr(# G,G,(id G) #) is strict Morphism of G,G

proof 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) #);

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

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

proof 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 )

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 )

proof end;

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 #)

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 #)

proof end;

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 )

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 )

proof end;

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 )

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 )

proof end;

definition

let R be Ring;

let G, F be LModMorphism of R;

assume A1: dom G = cod F ;

ex b_{1} 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

b_{1} = LModMorphismStr(# G1,G3,(g * f) #)

for b_{1}, b_{2} 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

b_{1} = 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

b_{2} = LModMorphismStr(# G1,G3,(g * f) #) ) holds

b_{1} = b_{2}

end;
let G, F be LModMorphism of R;

assume A1: dom G = cod F ;

func G * 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 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) #);

ex b

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof 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 b_{4} being strict LModMorphism of R holds

( b_{4} = 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

b_{4} = LModMorphismStr(# G1,G3,(g * f) #) );

for R being Ring

for G, F being LModMorphism of R st dom G = cod F holds

for b

( b

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

b

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

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

proof end;

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;

coherence

G * F is strict Morphism of G1,G3 by Th12;

end;
let G1, G2, G3 be LeftMod of R;

let G be Morphism of G2,G3;

let F be Morphism of G1,G2;

coherence

G * F is strict Morphism of G1,G3 by Th12;

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

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) #) )

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) #) )

proof end;

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) #) )

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) #) )

proof end;

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 )

for f, g being strict LModMorphism of R st dom g = cod f holds

( dom (g * f) = dom f & cod (g * f) = cod g )

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

proof end;

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

proof end;

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

proof end;

definition

let a be Element of {0,1,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 b_{1} being Element of {0,1,2} holds

( ( a = 0 & a = 1 implies ( b_{1} = 0 iff b_{1} = 2 ) ) & ( a = 0 & a = 2 implies ( b_{1} = 0 iff b_{1} = 1 ) ) & ( a = 1 & a = 2 implies ( b_{1} = 2 iff b_{1} = 1 ) ) )
;

let b be Element of {0,1,2};

( ( 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 b_{1} being Element of {0,1,2} holds

( ( a = 0 & b = 0 implies ( b_{1} = b iff b_{1} = a ) ) & ( a = 0 & a = 1 & b = 1 implies ( b_{1} = b iff b_{1} = 2 ) ) & ( a = 0 & a = 1 & b = 2 implies ( b_{1} = b iff b_{1} = 0 ) ) & ( a = 0 & a = 2 & b = 1 implies ( b_{1} = b iff b_{1} = 0 ) ) & ( a = 0 & a = 2 & b = 2 implies ( b_{1} = b iff b_{1} = 1 ) ) & ( b = 0 & a = 1 & b = 1 implies ( b_{1} = a iff b_{1} = 2 ) ) & ( b = 0 & a = 1 & b = 2 implies ( b_{1} = a iff b_{1} = 0 ) ) & ( b = 0 & a = 2 & b = 1 implies ( b_{1} = a iff b_{1} = 0 ) ) & ( b = 0 & a = 2 & b = 2 implies ( b_{1} = a iff b_{1} = 1 ) ) & ( a = 1 & b = 1 & a = 1 & b = 2 implies ( b_{1} = 2 iff b_{1} = 0 ) ) & ( a = 1 & b = 1 & a = 2 & b = 1 implies ( b_{1} = 2 iff b_{1} = 0 ) ) & ( a = 1 & b = 1 & a = 2 & b = 2 implies ( b_{1} = 2 iff b_{1} = 1 ) ) & ( a = 1 & b = 2 & a = 2 & b = 1 implies ( b_{1} = 0 iff b_{1} = 0 ) ) & ( a = 1 & b = 2 & a = 2 & b = 2 implies ( b_{1} = 0 iff b_{1} = 1 ) ) & ( a = 2 & b = 1 & a = 2 & b = 2 implies ( b_{1} = 0 iff b_{1} = 1 ) ) )
;

( ( 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 b_{1} being Element of {0,1,2} holds

( ( b = 0 & a = 0 implies ( b_{1} = 0 iff b_{1} = 0 ) ) & ( b = 0 & b = 1 implies ( b_{1} = 0 iff b_{1} = a ) ) & ( b = 0 & a = 1 implies ( b_{1} = 0 iff b_{1} = b ) ) & ( b = 0 & a = 2 & b = 2 implies ( b_{1} = 0 iff b_{1} = 1 ) ) & ( a = 0 & b = 1 implies ( b_{1} = 0 iff b_{1} = a ) ) & ( a = 0 & a = 1 implies ( b_{1} = 0 iff b_{1} = b ) ) & ( a = 0 & a = 2 & b = 2 implies ( b_{1} = 0 iff b_{1} = 1 ) ) & ( b = 1 & a = 1 implies ( b_{1} = a iff b_{1} = b ) ) & ( b = 1 & a = 2 & b = 2 implies ( b_{1} = a iff b_{1} = 1 ) ) & ( a = 1 & a = 2 & b = 2 implies ( b_{1} = b iff b_{1} = 1 ) ) )
;

end;
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 b

( ( a = 0 & a = 1 implies ( b

let b be Element of {0,1,2};

func a + 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 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 )

;

( ( 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 b

( ( a = 0 & b = 0 implies ( b

func a * 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 0 if b = 0

0 if a = 0

a if b = 1

b if a = 1

1 if ( a = 2 & b = 2 )

;

( ( 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 b

( ( b = 0 & a = 0 implies ( b

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

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

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

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

ex b_{1} being BinOp of {0,1,2} st

for a, b being Element of {0,1,2} holds b_{1} . (a,b) = a + b

for b_{1}, b_{2} being BinOp of {0,1,2} st ( for a, b being Element of {0,1,2} holds b_{1} . (a,b) = a + b ) & ( for a, b being Element of {0,1,2} holds b_{2} . (a,b) = a + b ) holds

b_{1} = b_{2}

ex b_{1} being BinOp of {0,1,2} st

for a, b being Element of {0,1,2} holds b_{1} . (a,b) = a * b

for b_{1}, b_{2} being BinOp of {0,1,2} st ( for a, b being Element of {0,1,2} holds b_{1} . (a,b) = a * b ) & ( for a, b being Element of {0,1,2} holds b_{2} . (a,b) = a * b ) holds

b_{1} = b_{2}

ex b_{1} being UnOp of {0,1,2} st

for a being Element of {0,1,2} holds b_{1} . a = - a

for b_{1}, b_{2} being UnOp of {0,1,2} st ( for a being Element of {0,1,2} holds b_{1} . a = - a ) & ( for a being Element of {0,1,2} holds b_{2} . a = - a ) holds

b_{1} = b_{2}

1 is Element of {0,1,2} by ENUMSET1:def 1;

coherence

0 is Element of {0,1,2} by ENUMSET1:def 1;

end;

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 for a, b being Element of {0,1,2} holds it . (a,b) = a + b;

ex b

for a, b being Element of {0,1,2} holds b

proof end;

uniqueness for b

b

proof end;

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 for a, b being Element of {0,1,2} holds it . (a,b) = a * b;

ex b

for a, b being Element of {0,1,2} holds b

proof end;

uniqueness for b

b

proof end;

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 for a being Element of {0,1,2} holds it . a = - a;

ex b

for a being Element of {0,1,2} holds b

proof end;

uniqueness for b

b

proof end;

coherence 1 is Element of {0,1,2} by ENUMSET1:def 1;

coherence

0 is Element of {0,1,2} by ENUMSET1:def 1;

:: deftheorem Def15 defines add3 MOD_2:def 15 :

for b_{1} being BinOp of {0,1,2} holds

( b_{1} = add3 iff for a, b being Element of {0,1,2} holds b_{1} . (a,b) = a + b );

for b

( b

:: deftheorem Def16 defines mult3 MOD_2:def 16 :

for b_{1} being BinOp of {0,1,2} holds

( b_{1} = mult3 iff for a, b being Element of {0,1,2} holds b_{1} . (a,b) = a * b );

for b

( b

:: deftheorem Def17 defines compl3 MOD_2:def 17 :

for b_{1} being UnOp of {0,1,2} holds

( b_{1} = compl3 iff for a being Element of {0,1,2} holds b_{1} . a = - a );

for b

( b

definition

doubleLoopStr(# {0,1,2},add3,mult3,unit3,zero3 #) is strict doubleLoopStr ;

end;

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

doubleLoopStr(# {0,1,2},add3,mult3,unit3,zero3 #) is strict doubleLoopStr ;

:: deftheorem Def20 defines Z_3 MOD_2:def 20 :

Z_3 = doubleLoopStr(# {0,1,2},add3,mult3,unit3,zero3 #);

Z_3 = doubleLoopStr(# {0,1,2},add3,mult3,unit3,zero3 #);

Lm5: now :: thesis: for h, e being Element of Z_3 st e = 1 holds

( h * e = h & e * h = h )

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

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

proof end;

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

proof end;

registration
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 )

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 )

proof end;

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

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

proof end;

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 & (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

( x + y = y + x & (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

proof end;

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 & (x + y) + z = x + (y + z) & x + (0. F) = x & x + (- x) = 0. F & x * y = y * x & (x * y) * z = x * (y * z) & (1. F) * x = x & x * (1. F) = x & ( x <> 0. F implies ex y being Scalar of F st x * y = 1. F ) & 0. F <> 1. F & x * (y + z) = (x * y) + (x * z) ) ) holds

F is Field

( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. F) = x & x + (- x) = 0. F & x * y = y * x & (x * y) * z = x * (y * z) & (1. F) * x = x & x * (1. F) = x & ( x <> 0. F implies ex y being Scalar of F st x * y = 1. F ) & 0. F <> 1. F & x * (y + z) = (x * y) + (x * z) ) ) holds

F is Field

proof end;

registration

( Z_3 is Fanoian & Z_3 is add-associative & Z_3 is right_zeroed & Z_3 is right_complementable & Z_3 is Abelian & Z_3 is commutative & Z_3 is associative & Z_3 is well-unital & Z_3 is distributive & Z_3 is almost_left_invertible ) by Th27;

end;

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 & Z_3 is add-associative & Z_3 is right_zeroed & Z_3 is right_complementable & Z_3 is Abelian & Z_3 is commutative & Z_3 is associative & Z_3 is well-unital & Z_3 is distributive & Z_3 is almost_left_invertible ) by Th27;

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

proof end;

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 & D9 in UN holds

f in UN

for UN being Universe

for f being Function of D,D9 st D in UN & D9 in UN holds

f in UN

proof end;

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 ) & ( for f being UnOp of D st D in UN holds

f in UN ) )

proof end;

theorem :: MOD_2:29

for UN being Universe holds

( the carrier of Z_3 in UN & the addF of Z_3 in UN & comp Z_3 in UN & 0. Z_3 in UN & the multF of Z_3 in UN & 1. Z_3 in UN )

( the carrier of Z_3 in UN & the addF of Z_3 in UN & comp Z_3 in UN & 0. Z_3 in UN & the multF of Z_3 in UN & 1. Z_3 in UN )

proof end;