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

Operations on Submodules in Right Module over Associative Ring

by
Michal Muzalewski, and
Wojciech Skaba

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

```environ

vocabulary FUNCSDOM, VECTSP_2, LMOD_4, VECTSP_1, RLVECT_1, RLSUB_1, BOOLE,
ARYTM_1, FUNCT_1, RELAT_1, RLSUB_2, MCART_1, BINOP_1, LATTICES, RMOD_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, RELAT_1, FUNCT_1,
STRUCT_0, LATTICES, RLVECT_1, DOMAIN_1, FUNCSDOM, VECTSP_2, RMOD_2;
constructors BINOP_1, LATTICES, DOMAIN_1, RMOD_2, MEMBERED, XBOOLE_0;
clusters LATTICES, VECTSP_2, RMOD_2, STRUCT_0, RLSUB_2, RELSET_1, SUBSET_1,
MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

reserve R for Ring,
V for RightMod of R,
W,W1,W2,W3 for Submodule of V,
u,u1,u2,v,v1,v2 for Vector of V,
x,y,y1,y2 for set;

definition let R; let V; let W1,W2;
func W1 + W2 -> strict Submodule of V means
:: RMOD_3:def 1
the carrier of it = {v + u : v in W1 & u in W2};
end;

definition let R; let V; let W1,W2;
func W1 /\ W2 -> strict Submodule of V means
:: RMOD_3:def 2
the carrier of it = (the carrier of W1) /\ (the carrier of W2);
end;

canceled 4;

theorem :: RMOD_3:5
x in W1 + W2 iff
(ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2);

theorem :: RMOD_3:6
v in W1 or v in W2 implies v in W1 + W2;

theorem :: RMOD_3:7
x in W1 /\ W2 iff x in W1 & x in W2;

theorem :: RMOD_3:8
for W being strict Submodule of V holds W + W = W;

theorem :: RMOD_3:9
W1 + W2 = W2 + W1;

theorem :: RMOD_3:10
W1 + (W2 + W3) = (W1 + W2) + W3;

theorem :: RMOD_3:11
W1 is Submodule of W1 + W2 & W2 is Submodule of W1 + W2;

theorem :: RMOD_3:12
for W2 being strict Submodule of V
holds W1 is Submodule of W2 iff W1 + W2 = W2;

theorem :: RMOD_3:13
for W being strict Submodule of V
holds (0).V + W = W & W + (0).V = W;

theorem :: RMOD_3:14
for V being strict RightMod of R
holds (0).V + (Omega).V = V & (Omega).V + (0).V = V;

theorem :: RMOD_3:15
for V being RightMod of R, W being Submodule of V
holds (Omega).V + W = the RightModStr of V & W + (Omega).
V = the RightModStr of V;

theorem :: RMOD_3:16
for V being strict RightMod of R holds (Omega).V + (Omega).V = V;

theorem :: RMOD_3:17
for W being strict Submodule of V
holds W /\ W = W;

theorem :: RMOD_3:18
W1 /\ W2 = W2 /\ W1;

theorem :: RMOD_3:19
W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3;

theorem :: RMOD_3:20
W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2;

theorem :: RMOD_3:21
(for W1 being strict Submodule of V
holds W1 is Submodule of W2 implies W1 /\ W2 = W1) &
for W1 st W1 /\ W2 = W1 holds W1 is Submodule of W2;

theorem :: RMOD_3:22
W1 is Submodule of W2 implies W1 /\ W3 is Submodule of W2 /\ W3;

theorem :: RMOD_3:23
W1 is Submodule of W3 implies W1 /\ W2 is Submodule of W3;

theorem :: RMOD_3:24
W1 is Submodule of W2 & W1 is Submodule of W3 implies
W1 is Submodule of W2 /\ W3;

theorem :: RMOD_3:25
(0).V /\ W = (0).V & W /\ (0).V = (0).V;

canceled;

theorem :: RMOD_3:27
for W being strict Submodule of V
holds (Omega).V /\ W = W & W /\ (Omega).V = W;

theorem :: RMOD_3:28
for V being strict RightMod of R holds (Omega).V /\ (Omega).V = V;

theorem :: RMOD_3:29
W1 /\ W2 is Submodule of W1 + W2;

theorem :: RMOD_3:30
for W2 being strict Submodule of V holds (W1 /\ W2) + W2 = W2;

theorem :: RMOD_3:31
for W1 being strict Submodule of V holds W1 /\ (W1 + W2) = W1;

theorem :: RMOD_3:32
(W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3);

theorem :: RMOD_3:33
W1 is Submodule of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3);

theorem :: RMOD_3:34
W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3);

theorem :: RMOD_3:35
W1 is Submodule of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3);

theorem :: RMOD_3:36
for W1 being strict Submodule of V
holds W1 is Submodule of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3;

theorem :: RMOD_3:37
for W1,W2 being strict Submodule of V
holds W1 + W2 = W2 iff W1 /\ W2 = W1;

theorem :: RMOD_3:38
for W2,W3 being strict Submodule of V
holds W1 is Submodule of W2 implies W1 + W3 is Submodule of W2 + W3;

theorem :: RMOD_3:39
W1 is Submodule of W2 implies W1 is Submodule of W2 + W3;

theorem :: RMOD_3:40
W1 is Submodule of W3 & W2 is Submodule of W3 implies
W1 + W2 is Submodule of W3;

theorem :: RMOD_3:41
(ex W st the carrier of W =
(the carrier of W1) \/ (the carrier of W2)) iff
W1 is Submodule of W2 or W2 is Submodule of W1;

definition let R; let V;
func Submodules(V) -> set means
:: RMOD_3:def 3
for x holds x in it iff
ex W being strict Submodule of V st W = x;
end;

definition let R; let V;
cluster Submodules(V) -> non empty;
end;

canceled 2;

theorem :: RMOD_3:44
for V being strict RightMod of R
holds V in Submodules(V);

definition let R; let V; let W1,W2;
pred V is_the_direct_sum_of W1,W2 means
:: RMOD_3:def 4
the RightModStr of V = W1 + W2 & W1 /\ W2 = (0).V;
end;

canceled;

theorem :: RMOD_3:46
V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2,W1;

theorem :: RMOD_3:47
for V being strict RightMod of R
holds V is_the_direct_sum_of (0).V,(Omega).V &
V is_the_direct_sum_of (Omega).V,(0).V;

reserve C1 for Coset of W1;
reserve C2 for Coset of W2;

theorem :: RMOD_3:48
C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2;

theorem :: RMOD_3:49
for V being RightMod of R, W1,W2 being Submodule of V
holds
V is_the_direct_sum_of W1,W2 iff
for C1 being Coset of W1, C2 being Coset of W2
ex v being Vector of V st C1 /\ C2 = {v};

theorem :: RMOD_3:50
for V being strict RightMod of R, W1,W2 being Submodule of V
holds W1 + W2 = 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;

theorem :: RMOD_3:51
for V being RightMod of R, W1,W2 being Submodule of V,
v,v1,v2,u1,u2 being Vector of V holds V is_the_direct_sum_of W1,W2 &
v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 implies
v1 = u1 & v2 = u2;

theorem :: RMOD_3:52
V = W1 + W2 &
(ex v st for v1,v2,u1,u2 st
v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
v1 = u1 & v2 = u2) implies V is_the_direct_sum_of W1,W2;

definition let R; let V be RightMod of R;
let v be Vector of V; let W1,W2 be Submodule of V;
assume  V is_the_direct_sum_of W1,W2;
func v |-- (W1,W2) -> Element of [:the carrier of V,
the carrier of V:] means
:: RMOD_3:def 5
v = it`1 + it`2 & it`1 in W1 & it`2 in W2;
end;

canceled 4;

theorem :: RMOD_3:57
V is_the_direct_sum_of W1,W2 implies
(v |-- (W1,W2))`1 = (v |-- (W2,W1))`2;

theorem :: RMOD_3:58
V is_the_direct_sum_of W1,W2 implies
(v |-- (W1,W2))`2 = (v |-- (W2,W1))`1;

reserve A1,A2,B for Element of Submodules(V);

definition let R; let V;
func SubJoin(V) -> BinOp of Submodules(V) means
:: RMOD_3:def 6
for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 + W2;
end;

definition let R; let V;
func SubMeet(V) -> BinOp of Submodules(V) means
:: RMOD_3:def 7
for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 /\ W2;
end;

canceled 4;

theorem :: RMOD_3:63
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is Lattice;

theorem :: RMOD_3:64
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is 0_Lattice;

theorem :: RMOD_3:65
for V being RightMod of R
holds LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is 1_Lattice;

theorem :: RMOD_3:66
for V being RightMod of R
holds LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is 01_Lattice;

theorem :: RMOD_3:67
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is M_Lattice;
```