:: Operations on Submodules in Right Module over Associative Ring
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines + RMOD_3:def 1 :
:: deftheorem Def2 defines /\ RMOD_3:def 2 :
theorem :: RMOD_3:1
canceled;
theorem :: RMOD_3:2
canceled;
theorem :: RMOD_3:3
canceled;
theorem :: RMOD_3:4
canceled;
theorem Th5: :: RMOD_3:5
theorem :: RMOD_3:6
theorem Th7: :: RMOD_3:7
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 :: RMOD_3:8
theorem :: RMOD_3:9
theorem Th10: :: RMOD_3:10
theorem Th11: :: RMOD_3:11
theorem Th12: :: RMOD_3:12
theorem Th13: :: RMOD_3:13
Lm4:
for R being Ring
for V being RightMod of R
for W, W', W1 being Submodule of V st the carrier of W = the carrier of W' holds
( W1 + W = W1 + W' & W + W1 = W' + 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 :: RMOD_3:14
theorem Th15: :: RMOD_3:15
theorem :: RMOD_3:16
theorem :: RMOD_3:17
theorem Th18: :: RMOD_3:18
theorem Th19: :: RMOD_3:19
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: :: RMOD_3:20
theorem Th21: :: RMOD_3:21
theorem :: RMOD_3:22
theorem :: RMOD_3:23
theorem :: RMOD_3:24
theorem Th25: :: RMOD_3:25
theorem :: RMOD_3:26
canceled;
theorem Th27: :: RMOD_3:27
theorem :: RMOD_3:28
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 :: RMOD_3:29
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 :: RMOD_3:30
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 :: RMOD_3:31
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 :: RMOD_3:32
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 :: RMOD_3:33
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 :: RMOD_3:34
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 :: RMOD_3:35
theorem Th36: :: RMOD_3:36
theorem :: RMOD_3:37
theorem :: RMOD_3:38
theorem :: RMOD_3:39
theorem :: RMOD_3:40
theorem :: RMOD_3:41
:: deftheorem Def3 defines Submodules RMOD_3:def 3 :
theorem :: RMOD_3:42
canceled;
theorem :: RMOD_3:43
canceled;
theorem :: RMOD_3:44
:: deftheorem Def4 defines is_the_direct_sum_of RMOD_3:def 4 :
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 U2 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 :: RMOD_3:45
canceled;
theorem Th46: :: RMOD_3:46
theorem :: RMOD_3:47
theorem Th48: :: RMOD_3:48
theorem Th49: :: RMOD_3:49
theorem :: RMOD_3:50
theorem Th51: :: RMOD_3:51
theorem :: RMOD_3:52
:: deftheorem Def5 defines |-- RMOD_3:def 5 :
theorem :: RMOD_3:53
canceled;
theorem :: RMOD_3:54
canceled;
theorem :: RMOD_3:55
canceled;
theorem :: RMOD_3:56
canceled;
theorem :: RMOD_3:57
theorem :: RMOD_3:58
definition
let R be
Ring;
let V be
RightMod of
R;
func SubJoin V -> BinOp of
Submodules V means :
Def6:
:: RMOD_3:def 6
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 :
definition
let R be
Ring;
let V be
RightMod of
R;
func SubMeet V -> BinOp of
Submodules V means :
Def7:
:: RMOD_3:def 7
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 :
theorem :: RMOD_3:59
canceled;
theorem :: RMOD_3:60
canceled;
theorem :: RMOD_3:61
canceled;
theorem :: RMOD_3:62
canceled;
theorem Th63: :: RMOD_3:63
theorem Th64: :: RMOD_3:64
theorem Th65: :: RMOD_3:65
theorem :: RMOD_3:66
theorem :: RMOD_3:67