:: MOD_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

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

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

:: deftheorem MOD_2:def 1 :
canceled;

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

theorem :: MOD_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for x being Vector of (TrivialLMod R) holds x = 0. (TrivialLMod R) by Lm1, ALGSTR_1:def 4, GRCAT_1:8;

definition
let R be non empty doubleLoopStr ;
let G, H be non empty VectSpStr of R;
let f be Function of G,H;
canceled;
canceled;
attr f is linear means :Def5: :: MOD_2:def 5
( ( for x, y being Vector of G holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of R
for x being Vector of G holds f . (a * x) = a * (f . x) ) );
end;

:: deftheorem MOD_2:def 3 :
canceled;

:: deftheorem MOD_2:def 4 :
canceled;

:: deftheorem Def5 defines linear MOD_2:def 5 :
for R being non empty doubleLoopStr
for G, H being non empty VectSpStr of R
for f being Function of G,H holds
( f is linear iff ( ( for x, y being Vector of G holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of R
for x being Vector of G holds f . (a * x) = a * (f . x) ) ) );

theorem :: MOD_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MOD_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: MOD_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for G, H being non empty VectSpStr of R
for f being Function of G,H st f is linear holds
f is additive
proof end;

theorem :: MOD_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th6: :: MOD_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for G, H, S being non empty VectSpStr of R
for f being Function of G,H
for g being Function of H,S st f is linear & g is linear holds
g * f is linear
proof end;

theorem :: MOD_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th8: :: MOD_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for G, H being LeftMod of R holds ZeroMap G,H is linear
proof end;

definition
let R be Ring;
attr c2 is strict;
struct LModMorphismStr of R -> ;
aggr LModMorphismStr(# Dom, Cod, Fun #) -> LModMorphismStr of 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 of R;
func dom f -> LeftMod of R equals :: MOD_2:def 6
the Dom of f;
correctness
coherence
the Dom of f is LeftMod of R
;
;
func cod f -> LeftMod of R equals :: MOD_2:def 7
the Cod of f;
correctness
coherence
the Cod of f is LeftMod of R
;
;
end;

:: deftheorem defines dom MOD_2:def 6 :
for R being Ring
for f being LModMorphismStr of R holds dom f = the Dom of f;

:: deftheorem defines cod MOD_2:def 7 :
for R being Ring
for f being LModMorphismStr of R holds cod f = the Cod of f;

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

:: deftheorem defines fun MOD_2:def 8 :
for R being Ring
for f being LModMorphismStr of R holds fun f = the Fun of f;

theorem :: MOD_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for G1, G2 being LeftMod of R
for f being LModMorphismStr of 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 of R equals :: MOD_2:def 9
LModMorphismStr(# G,H,(ZeroMap G,H) #);
correctness
coherence
LModMorphismStr(# G,H,(ZeroMap G,H) #) is strict LModMorphismStr of R
;
;
end;

:: deftheorem defines ZERO MOD_2:def 9 :
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 of R;
attr IT is LModMorphism-like means :Def10: :: MOD_2:def 10
fun IT is linear;
end;

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

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

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

theorem Th10: :: MOD_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for F being LModMorphism of R holds the Fun of F is linear
proof end;

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

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

:: deftheorem Def11 defines Morphism MOD_2:def 11 :
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 Morphism of G,H;
existence
ex b1 being Morphism of G,H st b1 is strict
proof end;
end;

theorem Th11: :: MOD_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for G, H being LeftMod of R
for f being LModMorphismStr of R st dom f = G & cod f = H & fun f is linear holds
f is Morphism of G,H
proof end;

theorem Th12: :: MOD_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for G, H being LeftMod of R
for f being Function of G,H st f is linear holds
LModMorphismStr(# G,H,f #) is strict Morphism of G,H
proof end;

theorem Th13: :: MOD_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for G being LeftMod of R holds id G is linear
proof end;

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

:: deftheorem defines ID MOD_2:def 12 :
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
proof end;
end;

theorem Th14: :: MOD_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 linear )
proof end;

theorem Th15: :: MOD_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 #)
proof end;

theorem Th16: :: MOD_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for F being LModMorphism of R ex G, H being LeftMod of R st F is Morphism of G,H
proof end;

theorem :: MOD_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 linear )
proof end;

theorem Th18: :: MOD_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let R be Ring;
let G, F be LModMorphism of R;
assume A1: dom G = cod F ;
func G * F -> strict LModMorphism of R means :Def13: :: MOD_2:def 13
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) #)
proof end;
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
proof end;
end;

:: deftheorem Def13 defines * MOD_2:def 13 :
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 :: MOD_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th20: :: MOD_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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;
func G *' F -> strict Morphism of G1,G3 equals :: MOD_2:def 14
G * F;
coherence
G * F is strict Morphism of G1,G3
by Th20;
end;

:: deftheorem defines *' MOD_2:def 14 :
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 Th21: :: MOD_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) #) )
proof end;

theorem Th22: :: MOD_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) #) )
proof end;

theorem :: MOD_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th24: :: MOD_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: MOD_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: MOD_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

registration
let x, y, z be set ;
cluster {x,y,z} -> non empty ;
coherence
not {x,y,z} is empty
by ENUMSET1:def 1;
end;

theorem :: MOD_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th28: :: MOD_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for u, v, w being Element of UN holds {u,v,w} is Element of UN
proof end;

theorem Th29: :: MOD_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for u being Element of UN holds succ u is Element of UN
proof end;

theorem Th30: :: MOD_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe holds
( 0 is Element of UN & 1 is Element of UN & 2 is Element of UN )
proof end;

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

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

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

definition
let a be Element of {0,1,2};
func - a -> Element of {0,1,2} equals :Def15: :: MOD_2:def 15
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 Lm4, Lm5;
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};
func a + b -> Element of {0,1,2} equals :Def16: :: MOD_2:def 16
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 Lm3, Lm4, Lm5;
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 ) ) )
;
func a * b -> Element of {0,1,2} equals :Def17: :: MOD_2:def 17
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 Lm4;
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 Def15 defines - MOD_2:def 15 :
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 Def16 defines + MOD_2:def 16 :
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 Def17 defines * MOD_2:def 17 :
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 :Def18: :: MOD_2:def 18
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
proof end;
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
proof end;
func mult3 -> BinOp of {0,1,2} means :Def19: :: MOD_2:def 19
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
proof end;
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
proof end;
func compl3 -> UnOp of {0,1,2} means :Def20: :: MOD_2:def 20
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
proof end;
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
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 a, b being Element of {0,1,2} holds b1 . a,b = a + b );

:: deftheorem Def19 defines mult3 MOD_2:def 19 :
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 Def20 defines compl3 MOD_2:def 20 :
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 21 :
unit3 = 1;

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

Lm6: now
let h, e be Element of Z3 ; :: 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 = mult3 . h,e
.= b * a by Def19
.= h by A1, Def17 ; :: thesis: e * h = h
thus e * h = mult3 . e,h
.= a * b by Def19
.= h by A1, Def17 ; :: thesis: verum
end;

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

Lm7: 1. Z3 = 1
proof end;

theorem :: MOD_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th32: :: MOD_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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 Lm7;

Lm8: for x, y being Scalar of Z3
for X, Y being Element of {0,1,2} st X = x & Y = y holds
( x + y = X + Y & x * y = X * Y )
proof end;

Lm9: for x, y, z being Scalar of Z3
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;

Lm10: 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
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Scalar of Z3
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 Th34: :: MOD_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being Scalar of Z3
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 Th35: :: MOD_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th36: :: MOD_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 <> 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;

theorem Th37: :: MOD_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

Lm11: for UN being Universe holds the carrier of Z3 in UN
proof end;

theorem Th38: :: MOD_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, D' being non empty set
for UN being Universe
for f being Function of D,D' st D in UN & D' in UN holds
f in UN
proof end;

Lm12: 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:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MOD_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe holds
( the carrier of Z3 in UN & the add of Z3 is Element of UN & comp Z3 is Element of UN & the Zero of Z3 is Element of UN & the mult of Z3 is Element of UN & the unity of Z3 is Element of UN )
proof end;