Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Submodules and Cosets of Submodules in Right Module over Associative Ring

by
Michal Muzalewski, and
Wojciech Skaba

MML identifier: RMOD_2
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCSDOM, VECTSP_1, VECTSP_2, RLSUB_1, BOOLE, RLVECT_1, ARYTM_1,
LMOD_4, RELAT_1, FUNCT_1, BINOP_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
STRUCT_0, DOMAIN_1, RLVECT_1, BINOP_1, VECTSP_1, FUNCSDOM, VECTSP_2;
constructors DOMAIN_1, BINOP_1, VECTSP_2, PARTFUN1, MEMBERED, XBOOLE_0;
clusters FUNCT_1, VECTSP_2, STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1,
XBOOLE_0;
requirements SUBSET, BOOLE;

begin

reserve x,y,y1,y2 for set;
reserve R for Ring;
reserve a for Scalar of R;
reserve V,X,Y for RightMod of R;
reserve u,u1,u2,v,v1,v2 for Vector of V;
reserve V1,V2,V3 for Subset of V;

definition let R, V, V1;
attr V1 is lineary-closed means
:: RMOD_2:def 1
(for v,u st v in V1 & u in V1 holds v + u in V1) &
(for a,v st v in V1 holds v * a in V1);
end;

canceled 3;

theorem :: RMOD_2:4
V1 <> {} & V1 is lineary-closed implies 0.V in V1;

theorem :: RMOD_2:5
V1 is lineary-closed implies (for v st v in V1 holds - v in V1);

theorem :: RMOD_2:6
V1 is lineary-closed implies
(for v,u st v in V1 & u in V1 holds v - u in V1);

theorem :: RMOD_2:7
{0.V} is lineary-closed;

theorem :: RMOD_2:8
the carrier of V = V1 implies V1 is lineary-closed;

theorem :: RMOD_2:9
V1 is lineary-closed & V2 is lineary-closed &
V3 = {v + u : v in V1 & u in V2} implies V3 is lineary-closed;

theorem :: RMOD_2:10
V1 is lineary-closed & V2 is lineary-closed implies
V1 /\ V2 is lineary-closed;

definition let R; let V;
mode Submodule of V -> RightMod of R means
:: RMOD_2:def 2
the carrier of it c= the carrier of V &
the Zero of it = the Zero 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:];
end;

reserve W,W1,W2 for Submodule of V;
reserve w,w1,w2 for Vector of W;

canceled 5;

theorem :: RMOD_2:16
x in W1 & W1 is Submodule of W2 implies x in W2;

theorem :: RMOD_2:17
x in W implies x in V;

theorem :: RMOD_2:18
w is Vector of V;

theorem :: RMOD_2:19
0.W = 0.V;

theorem :: RMOD_2:20
0.W1 = 0.W2;

theorem :: RMOD_2:21
w1 = v & w2 = u implies w1 + w2 = v + u;

theorem :: RMOD_2:22
w = v implies w * a = v * a;

theorem :: RMOD_2:23
w = v implies - v = - w;

theorem :: RMOD_2:24
w1 = v & w2 = u implies w1 - w2 = v - u;

theorem :: RMOD_2:25
0.V in W;

theorem :: RMOD_2:26
0.W1 in W2;

theorem :: RMOD_2:27
0.W in V;

theorem :: RMOD_2:28
u in W & v in W implies u + v in W;

theorem :: RMOD_2:29
v in W implies v * a in W;

theorem :: RMOD_2:30
v in W implies - v in W;

theorem :: RMOD_2:31
u in W & v in W implies u - v in W;

theorem :: RMOD_2:32
V is Submodule of V;

theorem :: RMOD_2:33
for X,V being strict RightMod of R
holds V is Submodule of X & X is Submodule of V implies V = X;

definition let R,V;
cluster strict Submodule of V;
end;

theorem :: RMOD_2:34
V is Submodule of X & X is Submodule of Y implies V is Submodule of Y;

theorem :: RMOD_2:35
the carrier of W1 c= the carrier of W2 implies
W1 is Submodule of W2;

theorem :: RMOD_2:36
(for v st v in W1 holds v in W2) implies W1 is Submodule of W2;

theorem :: RMOD_2:37
for W1,W2 being strict Submodule of V
holds the carrier of W1 = the carrier of W2 implies
W1 = W2;

theorem :: RMOD_2:38
for W1,W2 being strict Submodule of V
holds (for v being Vector of V holds v in W1 iff v in W2) implies W1 = W2;

theorem :: RMOD_2:39
for V being strict RightMod of R, W being strict Submodule of V
holds the carrier of W = the carrier of V
implies W = V;

theorem :: RMOD_2:40
for V being strict RightMod of R, W being strict Submodule of V
holds (for v being Vector of V holds v in W) implies W = V;

theorem :: RMOD_2:41
the carrier of W = V1 implies V1 is lineary-closed;

theorem :: RMOD_2:42
V1 <> {} & V1 is lineary-closed implies
(ex W being strict Submodule of V st V1 = the carrier of W);

definition let R; let V;
func (0).V -> strict Submodule of V means
:: RMOD_2:def 3
the carrier of it = {0.V};
end;

definition let R; let V;
func (Omega).V -> strict Submodule of V equals
:: RMOD_2:def 4
the RightModStr of V;
end;

canceled 3;

theorem :: RMOD_2:46
x in (0).V iff x = 0.V;

theorem :: RMOD_2:47
(0).W = (0).V;

theorem :: RMOD_2:48
(0).W1 = (0).W2;

theorem :: RMOD_2:49
(0).W is Submodule of V;

theorem :: RMOD_2:50
(0).V is Submodule of W;

theorem :: RMOD_2:51
(0).W1 is Submodule of W2;

canceled;

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

definition let R; let V; let v,W;
func v + W -> Subset of V equals
:: RMOD_2:def 5
{v + u : u in W};
end;

definition let R; let V; let W;
mode Coset of W -> Subset of V means
:: RMOD_2:def 6
ex v st it = v + W;
end;

reserve B,C for Coset of W;

canceled 3;

theorem :: RMOD_2:57
x in v + W iff ex u st u in W & x = v + u;

theorem :: RMOD_2:58
0.V in v + W iff v in W;

theorem :: RMOD_2:59
v in v + W;

theorem :: RMOD_2:60
0.V + W = the carrier of W;

theorem :: RMOD_2:61
v + (0).V = {v};

theorem :: RMOD_2:62
v + (Omega).V = the carrier of V;

theorem :: RMOD_2:63
0.V in v + W iff v + W = the carrier of W;

theorem :: RMOD_2:64
v in W iff v + W = the carrier of W;

theorem :: RMOD_2:65
v in W implies (v * a) + W = the carrier of W;

theorem :: RMOD_2:66
u in W iff v + W = (v + u) + W;

theorem :: RMOD_2:67
u in W iff v + W = (v - u) + W;

theorem :: RMOD_2:68
v in u + W iff u + W = v + W;

theorem :: RMOD_2:69
u in v1 + W & u in v2 + W implies v1 + W = v2 + W;

theorem :: RMOD_2:70
v in W implies v * a in v + W;

theorem :: RMOD_2:71
v in W implies - v in v + W;

theorem :: RMOD_2:72
u + v in v + W iff u in W;

theorem :: RMOD_2:73
v - u in v + W iff u in W;

canceled;

theorem :: RMOD_2:75
u in v + W iff
(ex v1 st v1 in W & u = v - v1);

theorem :: RMOD_2:76
(ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W;

theorem :: RMOD_2:77
v + W = u + W implies
(ex v1 st v1 in W & v + v1 = u);

theorem :: RMOD_2:78
v + W = u + W implies
(ex v1 st v1 in W & v - v1 = u);

theorem :: RMOD_2:79
for W1,W2 being strict Submodule of V
holds v + W1 = v + W2 iff W1 = W2;

theorem :: RMOD_2:80
for W1,W2 being strict Submodule of V
holds v + W1 = u + W2 implies W1 = W2;

theorem :: RMOD_2:81
ex C st v in C;

theorem :: RMOD_2:82
C is lineary-closed iff C = the carrier of W;

theorem :: RMOD_2:83
for W1,W2 being strict Submodule of V
for C1 being Coset of W1, C2 being Coset of W2
holds C1 = C2 implies W1 = W2;

theorem :: RMOD_2:84
{v} is Coset of (0).V;

theorem :: RMOD_2:85
V1 is Coset of (0).V implies (ex v st V1 = {v});

theorem :: RMOD_2:86
the carrier of W is Coset of W;

theorem :: RMOD_2:87
the carrier of V is Coset of (Omega).V;

theorem :: RMOD_2:88
V1 is Coset of (Omega).V implies V1 = the carrier of V;

theorem :: RMOD_2:89
0.V in C iff C = the carrier of W;

theorem :: RMOD_2:90
u in C iff C = u + W;

theorem :: RMOD_2:91
u in C & v in C implies (ex v1 st v1 in W & u + v1 = v);

theorem :: RMOD_2:92
u in C & v in C implies (ex v1 st v1 in W & u - v1 = v);

theorem :: RMOD_2:93
(ex C st v1 in C & v2 in C) iff v1 - v2 in W;

theorem :: RMOD_2:94
u in B & u in C implies B = C;
```