:: Submodules and Cosets of Submodules in Right Module over Associative Ring
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users


begin

definition
let R be Ring;
let V be RightMod of R;
let V1 be Subset of V;
attr V1 is linearly-closed means :Def1: :: RMOD_2:def 1
( ( for v, u being Vector of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for a being Scalar of R
for v being Vector of V st v in V1 holds
v * a in V1 ) );
end;

:: deftheorem Def1 defines linearly-closed RMOD_2:def 1 :
for R being Ring
for V being RightMod of R
for V1 being Subset of V holds
( V1 is linearly-closed iff ( ( for v, u being Vector of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for a being Scalar of R
for v being Vector of V st v in V1 holds
v * a in V1 ) ) );

theorem :: RMOD_2:1
canceled;

theorem :: RMOD_2:2
canceled;

theorem :: RMOD_2:3
canceled;

theorem Th4: :: RMOD_2:4
for R being Ring
for V being RightMod of R
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
0. V in V1
proof end;

theorem Th5: :: RMOD_2:5
for R being Ring
for V being RightMod of R
for V1 being Subset of V st V1 is linearly-closed holds
for v being Vector of V st v in V1 holds
- v in V1
proof end;

theorem :: RMOD_2:6
for R being Ring
for V being RightMod of R
for V1 being Subset of V st V1 is linearly-closed holds
for v, u being Vector of V st v in V1 & u in V1 holds
v - u in V1
proof end;

theorem Th7: :: RMOD_2:7
for R being Ring
for V being RightMod of R holds {(0. V)} is linearly-closed
proof end;

theorem :: RMOD_2:8
for R being Ring
for V being RightMod of R
for V1 being Subset of V st the carrier of V = V1 holds
V1 is linearly-closed
proof end;

theorem :: RMOD_2:9
for R being Ring
for V being RightMod of R
for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) } holds
V3 is linearly-closed
proof end;

theorem :: RMOD_2:10
for R being Ring
for V being RightMod of R
for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds
V1 /\ V2 is linearly-closed
proof end;

definition
let R be Ring;
let V be RightMod of R;
mode Submodule of V -> RightMod of R means :Def2: :: RMOD_2:def 2
( the carrier of it c= the carrier of V & 0. it = 0. V & the addF of it = the addF of V | [: the carrier of it, the carrier of it:] & the rmult of it = the rmult of V | [: the carrier of it, the carrier of R:] );
existence
ex b1 being RightMod of R st
( the carrier of b1 c= the carrier of V & 0. b1 = 0. V & the addF of b1 = the addF of V | [: the carrier of b1, the carrier of b1:] & the rmult of b1 = the rmult of V | [: the carrier of b1, the carrier of R:] )
proof end;
end;

:: deftheorem Def2 defines Submodule RMOD_2:def 2 :
for R being Ring
for V, b3 being RightMod of R holds
( b3 is Submodule of V iff ( the carrier of b3 c= the carrier of V & 0. b3 = 0. V & the addF of b3 = the addF of V | [: the carrier of b3, the carrier of b3:] & the rmult of b3 = the rmult of V | [: the carrier of b3, the carrier of R:] ) );

theorem :: RMOD_2:11
canceled;

theorem :: RMOD_2:12
canceled;

theorem :: RMOD_2:13
canceled;

theorem :: RMOD_2:14
canceled;

theorem :: RMOD_2:15
canceled;

theorem :: RMOD_2:16
for x being set
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V st x in W1 & W1 is Submodule of W2 holds
x in W2
proof end;

theorem Th17: :: RMOD_2:17
for x being set
for R being Ring
for V being RightMod of R
for W being Submodule of V st x in W holds
x in V
proof end;

theorem Th18: :: RMOD_2:18
for R being Ring
for V being RightMod of R
for W being Submodule of V
for w being Vector of W holds w is Vector of V
proof end;

theorem :: RMOD_2:19
for R being Ring
for V being RightMod of R
for W being Submodule of V holds 0. W = 0. V by Def2;

theorem :: RMOD_2:20
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds 0. W1 = 0. W2
proof end;

theorem Th21: :: RMOD_2:21
for R being Ring
for V being RightMod of R
for v, u being Vector of V
for W being Submodule of V
for w1, w2 being Vector of W st w1 = v & w2 = u holds
w1 + w2 = v + u
proof end;

theorem Th22: :: RMOD_2:22
for R being Ring
for a being Scalar of R
for V being RightMod of R
for v being Vector of V
for W being Submodule of V
for w being Vector of W st w = v holds
w * a = v * a
proof end;

theorem Th23: :: RMOD_2:23
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V
for w being Vector of W st w = v holds
- v = - w
proof end;

theorem Th24: :: RMOD_2:24
for R being Ring
for V being RightMod of R
for v, u being Vector of V
for W being Submodule of V
for w1, w2 being Vector of W st w1 = v & w2 = u holds
w1 - w2 = v - u
proof end;

Lm1: for R being Ring
for V being RightMod of R
for V1 being Subset of V
for W being Submodule of V st the carrier of W = V1 holds
V1 is linearly-closed
proof end;

theorem Th25: :: RMOD_2:25
for R being Ring
for V being RightMod of R
for W being Submodule of V holds 0. V in W
proof end;

theorem :: RMOD_2:26
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds 0. W1 in W2
proof end;

theorem :: RMOD_2:27
for R being Ring
for V being RightMod of R
for W being Submodule of V holds 0. W in V by Th17, RLVECT_1:3;

theorem Th28: :: RMOD_2:28
for R being Ring
for V being RightMod of R
for u, v being Vector of V
for W being Submodule of V st u in W & v in W holds
u + v in W
proof end;

theorem Th29: :: RMOD_2:29
for R being Ring
for a being Scalar of R
for V being RightMod of R
for v being Vector of V
for W being Submodule of V st v in W holds
v * a in W
proof end;

theorem Th30: :: RMOD_2:30
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V st v in W holds
- v in W
proof end;

theorem Th31: :: RMOD_2:31
for R being Ring
for V being RightMod of R
for u, v being Vector of V
for W being Submodule of V st u in W & v in W holds
u - v in W
proof end;

theorem Th32: :: RMOD_2:32
for R being Ring
for V being RightMod of R holds V is Submodule of V
proof end;

theorem Th33: :: RMOD_2:33
for R being Ring
for X, V being strict RightMod of R st V is Submodule of X & X is Submodule of V holds
V = X
proof end;

registration
let R be Ring;
let V be RightMod of R;
cluster non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like Submodule of V;
existence
ex b1 being Submodule of V st b1 is strict
proof end;
end;

theorem Th34: :: RMOD_2:34
for R being Ring
for V, X, Y being RightMod of R st V is Submodule of X & X is Submodule of Y holds
V is Submodule of Y
proof end;

theorem Th35: :: RMOD_2:35
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V st the carrier of W1 c= the carrier of W2 holds
W1 is Submodule of W2
proof end;

theorem :: RMOD_2:36
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V st ( for v being Vector of V st v in W1 holds
v in W2 ) holds
W1 is Submodule of W2
proof end;

theorem Th37: :: RMOD_2:37
for R being Ring
for V being RightMod of R
for W1, W2 being strict Submodule of V st the carrier of W1 = the carrier of W2 holds
W1 = W2
proof end;

theorem Th38: :: RMOD_2:38
for R being Ring
for V being RightMod of R
for W1, W2 being strict Submodule of V st ( for v being Vector of V holds
( v in W1 iff v in W2 ) ) holds
W1 = W2
proof end;

theorem :: RMOD_2:39
for R being Ring
for V being strict RightMod of R
for W being strict Submodule of V st the carrier of W = the carrier of V holds
W = V
proof end;

theorem :: RMOD_2:40
for R being Ring
for V being strict RightMod of R
for W being strict Submodule of V st ( for v being Vector of V holds v in W ) holds
W = V
proof end;

theorem :: RMOD_2:41
for R being Ring
for V being RightMod of R
for V1 being Subset of V
for W being Submodule of V st the carrier of W = V1 holds
V1 is linearly-closed by Lm1;

theorem Th42: :: RMOD_2:42
for R being Ring
for V being RightMod of R
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Submodule of V st V1 = the carrier of W
proof end;

definition
let R be Ring;
let V be RightMod of R;
func (0). V -> strict Submodule of V means :Def3: :: RMOD_2:def 3
 the carrier of it = {(0. V)};
correctness
existence
ex b1 being strict Submodule of V st the carrier of b1 = {(0. V)};
uniqueness
for b1, b2 being strict Submodule of V st the carrier of b1 = {(0. V)} & the carrier of b2 = {(0. V)} holds
b1 = b2;
by Th7, Th37, Th42;
end;

:: deftheorem Def3 defines (0). RMOD_2:def 3 :
for R being Ring
for V being RightMod of R
for b3 being strict Submodule of V holds
( b3 = (0). V iff the carrier of b3 = {(0. V)} );

definition
let R be Ring;
let V be RightMod of R;
func (Omega). V -> strict Submodule of V equals :: RMOD_2:def 4
 RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #);
coherence
RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is strict Submodule of V
proof end;
end;

:: deftheorem defines (Omega). RMOD_2:def 4 :
for R being Ring
for V being RightMod of R holds (Omega). V = RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #);

theorem :: RMOD_2:43
canceled;

theorem :: RMOD_2:44
canceled;

theorem :: RMOD_2:45
canceled;

theorem :: RMOD_2:46
for x being set
for R being Ring
for V being RightMod of R holds
( x in (0). V iff x = 0. V )
proof end;

theorem Th47: :: RMOD_2:47
for R being Ring
for V being RightMod of R
for W being Submodule of V holds (0). W = (0). V
proof end;

theorem Th48: :: RMOD_2:48
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds (0). W1 = (0). W2
proof end;

theorem :: RMOD_2:49
for R being Ring
for V being RightMod of R
for W being Submodule of V holds (0). W is Submodule of V by Th34;

theorem :: RMOD_2:50
for R being Ring
for V being RightMod of R
for W being Submodule of V holds (0). V is Submodule of W
proof end;

theorem :: RMOD_2:51
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds (0). W1 is Submodule of W2
proof end;

theorem :: RMOD_2:52
canceled;

theorem :: RMOD_2:53
for R being Ring
for V being strict RightMod of R holds V is Submodule of (Omega). V ;

definition
let R be Ring;
let V be RightMod of R;
let v be Vector of V;
let W be Submodule of V;
func v + W -> Subset of V equals :: RMOD_2:def 5
 { (v + u) where u is Vector of V : u in W } ;
coherence
{ (v + u) where u is Vector of V : u in W } is Subset of V
proof end;
end;

:: deftheorem defines + RMOD_2:def 5 :
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V holds v + W = { (v + u) where u is Vector of V : u in W } ;

Lm2: for R being Ring
for V being RightMod of R
for W being Submodule of V holds (0. V) + W = the carrier of W
proof end;

definition
let R be Ring;
let V be RightMod of R;
let W be Submodule of V;
mode Coset of W -> Subset of V means :Def6: :: RMOD_2:def 6
 ex v being Vector of V st it = v + W;
existence
ex b1 being Subset of V ex v being Vector of V st b1 = v + W
proof end;
end;

:: deftheorem Def6 defines Coset RMOD_2:def 6 :
for R being Ring
for V being RightMod of R
for W being Submodule of V
for b4 being Subset of V holds
( b4 is Coset of W iff ex v being Vector of V st b4 = v + W );

theorem :: RMOD_2:54
canceled;

theorem :: RMOD_2:55
canceled;

theorem :: RMOD_2:56
canceled;

theorem Th57: :: RMOD_2:57
for x being set
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V holds
( x in v + W iff ex u being Vector of V st
( u in W & x = v + u ) )
proof end;

theorem Th58: :: RMOD_2:58
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V holds
( 0. V in v + W iff v in W )
proof end;

theorem Th59: :: RMOD_2:59
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V holds v in v + W
proof end;

theorem :: RMOD_2:60
for R being Ring
for V being RightMod of R
for W being Submodule of V holds (0. V) + W = the carrier of W by Lm2;

theorem Th61: :: RMOD_2:61
for R being Ring
for V being RightMod of R
for v being Vector of V holds v + ((0). V) = {v}
proof end;

Lm3: for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V holds
( v in W iff v + W = the carrier of W )
proof end;

theorem Th62: :: RMOD_2:62
for R being Ring
for V being RightMod of R
for v being Vector of V holds v + ((Omega). V) = the carrier of V
proof end;

theorem Th63: :: RMOD_2:63
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V holds
( 0. V in v + W iff v + W = the carrier of W )
proof end;

theorem :: RMOD_2:64
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V holds
( v in W iff v + W = the carrier of W ) by Lm3;

theorem :: RMOD_2:65
for R being Ring
for a being Scalar of R
for V being RightMod of R
for v being Vector of V
for W being Submodule of V st v in W holds
(v * a) + W = the carrier of W
proof end;

theorem Th66: :: RMOD_2:66
for R being Ring
for V being RightMod of R
for u, v being Vector of V
for W being Submodule of V holds
( u in W iff v + W = (v + u) + W )
proof end;

theorem :: RMOD_2:67
for R being Ring
for V being RightMod of R
for u, v being Vector of V
for W being Submodule of V holds
( u in W iff v + W = (v - u) + W )
proof end;

theorem Th68: :: RMOD_2:68
for R being Ring
for V being RightMod of R
for v, u being Vector of V
for W being Submodule of V holds
( v in u + W iff u + W = v + W )
proof end;

theorem Th69: :: RMOD_2:69
for R being Ring
for V being RightMod of R
for u, v1, v2 being Vector of V
for W being Submodule of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W
proof end;

theorem Th70: :: RMOD_2:70
for R being Ring
for a being Scalar of R
for V being RightMod of R
for v being Vector of V
for W being Submodule of V st v in W holds
v * a in v + W
proof end;

theorem :: RMOD_2:71
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V st v in W holds
- v in v + W
proof end;

theorem Th72: :: RMOD_2:72
for R being Ring
for V being RightMod of R
for u, v being Vector of V
for W being Submodule of V holds
( u + v in v + W iff u in W )
proof end;

theorem :: RMOD_2:73
for R being Ring
for V being RightMod of R
for v, u being Vector of V
for W being Submodule of V holds
( v - u in v + W iff u in W )
proof end;

theorem :: RMOD_2:74
canceled;

theorem :: RMOD_2:75
for R being Ring
for V being RightMod of R
for u, v being Vector of V
for W being Submodule of V holds
( u in v + W iff ex v1 being Vector of V st
( v1 in W & u = v - v1 ) )
proof end;

theorem Th76: :: RMOD_2:76
for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V
for W being Submodule of V holds
( ex v being Vector of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
proof end;

theorem Th77: :: RMOD_2:77
for R being Ring
for V being RightMod of R
for v, u being Vector of V
for W being Submodule of V st v + W = u + W holds
ex v1 being Vector of V st
( v1 in W & v + v1 = u )
proof end;

theorem Th78: :: RMOD_2:78
for R being Ring
for V being RightMod of R
for v, u being Vector of V
for W being Submodule of V st v + W = u + W holds
ex v1 being Vector of V st
( v1 in W & v - v1 = u )
proof end;

theorem Th79: :: RMOD_2:79
for R being Ring
for V being RightMod of R
for v being Vector of V
for W1, W2 being strict Submodule of V holds
( v + W1 = v + W2 iff W1 = W2 )
proof end;

theorem Th80: :: RMOD_2:80
for R being Ring
for V being RightMod of R
for v, u being Vector of V
for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds
W1 = W2
proof end;

theorem :: RMOD_2:81
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V ex C being Coset of W st v in C
proof end;

theorem :: RMOD_2:82
for R being Ring
for V being RightMod of R
for W being Submodule of V
for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W )
proof end;

theorem :: RMOD_2:83
for R being Ring
for V being RightMod of R
for W1, W2 being strict Submodule of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 = C2 holds
W1 = W2
proof end;

theorem :: RMOD_2:84
for R being Ring
for V being RightMod of R
for v being Vector of V holds {v} is Coset of (0). V
proof end;

theorem :: RMOD_2:85
for R being Ring
for V being RightMod of R
for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being Vector of V st V1 = {v}
proof end;

theorem :: RMOD_2:86
for R being Ring
for V being RightMod of R
for W being Submodule of V holds the carrier of W is Coset of W
proof end;

theorem :: RMOD_2:87
for R being Ring
for V being RightMod of R holds the carrier of V is Coset of (Omega). V
proof end;

theorem :: RMOD_2:88
for R being Ring
for V being RightMod of R
for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V
proof end;

theorem :: RMOD_2:89
for R being Ring
for V being RightMod of R
for W being Submodule of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
proof end;

theorem Th90: :: RMOD_2:90
for R being Ring
for V being RightMod of R
for u being Vector of V
for W being Submodule of V
for C being Coset of W holds
( u in C iff C = u + W )
proof end;

theorem :: RMOD_2:91
for R being Ring
for V being RightMod of R
for u, v being Vector of V
for W being Submodule of V
for C being Coset of W st u in C & v in C holds
ex v1 being Vector of V st
( v1 in W & u + v1 = v )
proof end;

theorem :: RMOD_2:92
for R being Ring
for V being RightMod of R
for u, v being Vector of V
for W being Submodule of V
for C being Coset of W st u in C & v in C holds
ex v1 being Vector of V st
( v1 in W & u - v1 = v )
proof end;

theorem :: RMOD_2:93
for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V
for W being Submodule of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
proof end;

theorem :: RMOD_2:94
for R being Ring
for V being RightMod of R
for u being Vector of V
for W being Submodule of V
for B, C being Coset of W st u in B & u in C holds
B = C
proof end;