begin
:: deftheorem Def1 defines + RMOD_3:def 1 :
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V
for b5 being strict Submodule of V holds
( b5 = W1 + W2 iff the carrier of b5 = { (v + u) where v, u is Vector of V : ( v in W1 & u in W2 ) } );
:: deftheorem Def2 defines /\ RMOD_3:def 2 :
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V
for b5 being strict Submodule of V holds
( b5 = W1 /\ W2 iff the carrier of b5 = the carrier of W1 /\ the carrier of W2 );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem
theorem Th7:
Lm1:
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds W1 + W2 = W2 + W1
Lm2:
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of W1 c= the carrier of (W1 + W2)
Lm3:
for R being Ring
for V being RightMod of R
for W1 being Submodule of V
for W2 being strict Submodule of V st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
theorem
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
Lm4:
for R being Ring
for V being RightMod of R
for W, W9, W1 being Submodule of V st the carrier of W = the carrier of W9 holds
( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
Lm5:
for R being Ring
for V being RightMod of R
for W being Submodule of V holds W is Submodule of (Omega). V
theorem
theorem Th15:
theorem
theorem
theorem Th18:
theorem Th19:
Lm6:
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of W1
theorem Th20:
theorem Th21:
theorem
theorem
theorem
theorem Th25:
theorem
canceled;
theorem Th27:
theorem
Lm7:
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
theorem
Lm8:
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
theorem
Lm9:
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
theorem
Lm10:
for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
theorem
Lm11:
for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
theorem
Lm12:
for R being Ring
for V being RightMod of R
for W2, W1, W3 being Submodule of V holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
theorem
Lm13:
for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))
theorem
theorem Th36:
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def3 defines Submodules RMOD_3:def 3 :
for R being Ring
for V being RightMod of R
for b3 being set holds
( b3 = Submodules V iff for x being set holds
( x in b3 iff ex W being strict Submodule of V st W = x ) );
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem Def4 defines is_the_direct_sum_of RMOD_3:def 4 :
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds
( V is_the_direct_sum_of W1,W2 iff ( RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W1 + W2 & W1 /\ W2 = (0). V ) );
Lm14:
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds
( W1 + W2 = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) iff for v being Vector of V ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) )
Lm15:
for R being Ring
for V being RightMod of R
for v, v1, v2 being Vector of V holds
( v = v1 + v2 iff v1 = v - v2 )
theorem
canceled;
theorem Th46:
theorem
theorem Th48:
theorem Th49:
theorem
theorem Th51:
theorem
:: deftheorem Def5 defines |-- RMOD_3:def 5 :
for R being Ring
for V being RightMod of R
for v being Vector of V
for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds
for b6 being Element of [: the carrier of V, the carrier of V:] holds
( b6 = v |-- (W1,W2) iff ( v = (b6 `1) + (b6 `2) & b6 `1 in W1 & b6 `2 in W2 ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
definition
let R be
Ring;
let V be
RightMod of
R;
func SubJoin V -> BinOp of
(Submodules V) means :
Def6:
for
A1,
A2 being
Element of
Submodules V for
W1,
W2 being
Submodule of
V st
A1 = W1 &
A2 = W2 holds
it . (
A1,
A2)
= W1 + W2;
existence
ex b1 being BinOp of (Submodules V) st
for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2
uniqueness
for b1, b2 being BinOp of (Submodules V) st ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 + W2 ) holds
b1 = b2
end;
:: deftheorem Def6 defines SubJoin RMOD_3:def 6 :
for R being Ring
for V being RightMod of R
for b3 being BinOp of (Submodules V) holds
( b3 = SubJoin V iff for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b3 . (A1,A2) = W1 + W2 );
definition
let R be
Ring;
let V be
RightMod of
R;
func SubMeet V -> BinOp of
(Submodules V) means :
Def7:
for
A1,
A2 being
Element of
Submodules V for
W1,
W2 being
Submodule of
V st
A1 = W1 &
A2 = W2 holds
it . (
A1,
A2)
= W1 /\ W2;
existence
ex b1 being BinOp of (Submodules V) st
for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2
uniqueness
for b1, b2 being BinOp of (Submodules V) st ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 /\ W2 ) holds
b1 = b2
end;
:: deftheorem Def7 defines SubMeet RMOD_3:def 7 :
for R being Ring
for V being RightMod of R
for b3 being BinOp of (Submodules V) holds
( b3 = SubMeet V iff for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b3 . (A1,A2) = W1 /\ W2 );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th63:
theorem Th64:
theorem Th65:
theorem
theorem