The abstract of the Mizar article:

Operations on Submodules in Right Module over Associative Ring

by

Michal Muzalewski, and

Wojciech Skaba

Received October 22, 1990

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;