begin
Lm1:
for R being Ring holds VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is strict LeftMod of R
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 :
Def10:
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) #)
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
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 Th13:
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) #) )
theorem Th14:
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) #) )
Lm2:
ex c being Element of {0,1,2} st c = 0
Lm3:
ex c being Element of {0,1,2} st c = 1
Lm4:
ex c being Element of {0,1,2} st c = 2
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 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 :
Def13:
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 ) ) )
;
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 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
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
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
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
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
existence
ex b1 being UnOp of {0,1,2} st
for a being Element of {0,1,2} holds b1 . a = - a
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
coherence
1 is Element of {0,1,2}
by ENUMSET1:def 1;
coherence
0 is Element of {0,1,2}
by ENUMSET1:def 1;
end;
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) )
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) )
theorem Th24:
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) )
theorem Th25:
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) )
Lm8:
for UN being Universe holds the carrier of Z_3 in UN
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 ) )