The Mizar article:

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

MML identifier: RMOD_3
[ 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;
 definitions TARSKI, RMOD_2, XBOOLE_0;
 theorems BINOP_1, FUNCT_1, FUNCT_2, LATTICES, MCART_1, RLSUB_2, TARSKI,
      VECTSP_1, ZFMISC_1, RMOD_2, RLVECT_1, RELAT_1, XBOOLE_0, XBOOLE_1;
 schemes BINOP_1, FUNCT_1, XBOOLE_0;

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 :Def1:
    the carrier of it = {v + u : v in W1 & u in W2};
  existence
   proof set VS = {v + u : v in W1 & u in W2};
         VS c= the carrier of V
        proof let x be set;
          assume x in VS;
           then ex v1,v2 st x = v1 + v2 & v1 in W1 & v2 in W2;
         hence thesis;
        end;
      then reconsider VS as Subset of V;
         0.V in W1 & 0.V in W2 & 0.V = 0.V + 0.V by RMOD_2:25,VECTSP_1:7;
       then A1: 0.V in VS;
      reconsider V1 = the carrier of W1,
                 V2 = the carrier of W2 as Subset of V
                     by RMOD_2:def 2;
       A2: VS = {v + u : v in V1 & u in V2}
        proof
         thus VS c= {v + u : v in V1 & u in V2}
          proof let x be set;
            assume x in VS;
             then consider v,u such that A3: x = v + u and A4: v in W1 & u in
 W2;
                v in V1 & u in V2 by A4,RLVECT_1:def 1;
           hence thesis by A3;
          end;
         let x be set;
          assume x in {v + u : v in V1 & u in V2};
           then consider v,u such that A5: x = v + u and A6: v in V1 & u in V2;
              v in W1 & u in W2 by A6,RLVECT_1:def 1;
         hence thesis by A5;
        end;
         V1 is lineary-closed & V2 is lineary-closed by RMOD_2:41;
       then VS is lineary-closed by A2,RMOD_2:9;
    hence thesis by A1,RMOD_2:42;
   end;
  uniqueness by RMOD_2:37;
 end;

 definition let R; let V; let W1,W2;
  func W1 /\ W2 -> strict Submodule of V means :Def2:
    the carrier of it = (the carrier of W1) /\ (the carrier of W2);
  existence
   proof set VV = the carrier of V;
         set VW1 = the carrier of W1;
         set VW2 = the carrier of W2;
        VW1 c= VV & VW2 c= VV by RMOD_2:def 2;
      then VW1 /\ VW2 c= VV /\ VV by XBOOLE_1:27;
     then reconsider V1 = VW1, V2 = VW2, V3 = VW1 /\ VW2
          as Subset of V by RMOD_2:def 2;
        0.V in W1 & 0.V in W2 by RMOD_2:25;
      then 0.V in VW1 & 0.V in VW2 by RLVECT_1:def 1;
      then A1: VW1 /\ VW2 <> {} by XBOOLE_0:def 3;
        V1 is lineary-closed & V2 is lineary-closed by RMOD_2:41;
      then V3 is lineary-closed by RMOD_2:10;
    hence thesis by A1,RMOD_2:42;
   end;
  uniqueness by RMOD_2:37;
 end;

canceled 4;

theorem Th5:
 x in W1 + W2 iff
  (ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2)
   proof
    thus x in W1 + W2 implies (ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2)
     proof assume x in W1 + W2;
        then x in the carrier of W1 + W2 by RLVECT_1:def 1;
        then x in {v + u : v in W1 & u in W2} by Def1;
       then consider v1,v2 such that A1: x = v1 + v2 & v1 in W1 & v2 in W2;
      take v1,v2;
      thus thesis by A1;
     end;
     given v1,v2 such that A2: v1 in W1 & v2 in W2 & x = v1 + v2;
        x in {v + u : v in W1 & u in W2} by A2;
      then x in the carrier of W1 + W2 by Def1;
    hence thesis by RLVECT_1:def 1;
   end;

theorem
   v in W1 or v in W2 implies v in W1 + W2
  proof assume A1: v in W1 or v in W2;
      now per cases by A1;
     suppose A2: v in W1;
         v = v + 0.V & 0.V in W2 by RMOD_2:25,VECTSP_1:7;
      hence thesis by A2,Th5;
     suppose A3: v in W2;
         v = 0.V + v & 0.V in W1 by RMOD_2:25,VECTSP_1:7;
      hence thesis by A3,Th5;
    end;
   hence thesis;
  end;

theorem Th7:
 x in W1 /\ W2 iff x in W1 & x in W2
  proof
      x in W1 /\ W2 iff x in the carrier of W1 /\ W2 by RLVECT_1:def 1;
    then x in W1 /\ W2 iff
     x in (the carrier of W1) /\
         (the carrier of W2) by Def2;
    then x in W1 /\ W2 iff x in the carrier of W1 &
         x in the carrier of W2 by XBOOLE_0:def 3;
   hence thesis by RLVECT_1:def 1;
  end;

 Lm1: W1 + W2 = W2 + W1
  proof
        set A = {v + u : v in W1 & u in W2};
        set B = {v + u : v in W2 & u in W1};
    A1: the carrier of W1 + W2 = A &
       the carrier of W2 + W1 = B by Def1;
    A2: A c= B
     proof let x be set;
       assume x in A;
        then consider v,u such that A3: x = v + u and A4: v in W1 & u in W2;
      thus thesis by A3,A4;
     end;
      B c= A
     proof let x be set;
       assume x in B;
        then consider v,u such that A5: x = v + u and A6: v in W2 & u in W1;
      thus thesis by A5,A6;
     end;
   then A = B by A2,XBOOLE_0:def 10;
   hence thesis by A1,RMOD_2:37;
  end;

 Lm2: the carrier of W1 c=
         the carrier of W1 + W2
  proof let x be set;
     set A = {v + u : v in W1 & u in W2};
    assume x in the carrier of W1;
     then reconsider v = x as Element of W1;
     reconsider v as Vector of V by RMOD_2:18;
        v in W1 & 0.V in W2 & v = v + 0.V by RLVECT_1:def 1,RMOD_2:25,VECTSP_1:
7
;
      then x in A;
   hence thesis by Def1;
  end;

 Lm3:
  for W2 being strict Submodule of V
  holds the carrier of W1 c= the carrier of W2
  implies W1 + W2 = W2
  proof let W2 be strict Submodule of V;
     assume A1: the carrier of W1 c=
                   the carrier of W2;
      the carrier of W1 + W2 = the carrier of W2
     proof
      thus the carrier of W1 + W2 c=
           the carrier of W2
       proof
        let x be set;
         assume x in the carrier of W1 + W2;
           then x in {v + u : v in W1 & u in W2} by Def1;
          then consider v,u such that A2: x = v + u and A3: v in W1 and A4: u
in W2;
             W1 is Submodule of W2 by A1,RMOD_2:35;
           then v in W2 by A3,RMOD_2:16;
           then v + u in W2 by A4,RMOD_2:28;
        hence thesis by A2,RLVECT_1:def 1;
       end;
        W1 + W2 = W2 + W1 by Lm1;
      hence thesis by Lm2;
     end;
   hence thesis by RMOD_2:37;
  end;

theorem
  for W being strict Submodule of V holds W + W = W by Lm3;

theorem
   W1 + W2 = W2 + W1 by Lm1;

theorem Th10:
 W1 + (W2 + W3) = (W1 + W2) + W3
  proof set A = {v + u : v in W1 & u in W2};
        set B = {v + u : v in W2 & u in W3};
        set C = {v + u : v in W1 + W2 & u in W3};
        set D = {v + u : v in W1 & u in W2 + W3};
    A1: the carrier of W1 + (W2 + W3) = D &
       the carrier of (W1 + W2) + W3 = C by Def1;
    A2: D c= C
     proof let x be set;
       assume x in D;
        then consider v,u such that A3: x = v + u and
                                    A4: v in W1 and A5: u in W2 + W3;
           u in the carrier of W2 + W3 by A5,RLVECT_1:def 1;
         then u in B by Def1;
        then consider u1,u2 such that A6: u = u1 + u2 and
                                      A7: u1 in W2 and A8: u2 in W3;
         A9: v + u = (v + u1) + u2 by A6,RLVECT_1:def 6;
           v + u1 in A by A4,A7;
         then v + u1 in the carrier of W1 + W2 by Def1;
         then v + u1 in W1 + W2 by RLVECT_1:def 1;
      hence thesis by A3,A8,A9;
     end;
      C c= D
     proof let x be set;
       assume x in C;
        then consider v,u such that A10: x = v + u and
                                    A11: v in W1 + W2 and A12: u in W3;
           v in the carrier of W1 + W2 by A11,RLVECT_1:def 1;
         then v in A by Def1;
        then consider u1,u2 such that A13: v = u1 + u2 and
                                      A14: u1 in W1 and A15: u2 in W2;
         A16: v + u =u1 + (u2 + u) by A13,RLVECT_1:def 6;
           u2 + u in B by A12,A15;
         then u2 + u in the carrier of W2 + W3 by Def1;
         then u2 + u in W2 + W3 by RLVECT_1:def 1;
      hence thesis by A10,A14,A16;
     end;
    then D = C by A2,XBOOLE_0:def 10;
   hence thesis by A1,RMOD_2:37;
  end;

theorem Th11:
 W1 is Submodule of W1 + W2 & W2 is Submodule of W1 + W2
  proof the carrier of W1 c=
        the carrier of W1 + W2 by Lm2;
   hence W1 is Submodule of W1 + W2 by RMOD_2:35;
      the carrier of W2 c= the carrier of W2 + W1 by Lm2;
    then the carrier of W2 c=
         the carrier of W1 + W2 by Lm1;
   hence thesis by RMOD_2:35;
  end;

theorem Th12:
 for W2 being strict Submodule of V
 holds W1 is Submodule of W2 iff W1 + W2 = W2
  proof let W2 be strict Submodule of V;
   thus W1 is Submodule of W2 implies W1 + W2 = W2
    proof assume W1 is Submodule of W2;
      then the carrier of W1 c=
           the carrier of W2 by RMOD_2:def 2;
     hence thesis by Lm3;
    end;
   thus thesis by Th11;
  end;

theorem Th13:
 for W being strict Submodule of V
 holds (0).V + W = W & W + (0).V = W
  proof let W be strict Submodule of V;
      (0).V is Submodule of W by RMOD_2:50;
    then the carrier of (0).V c=
         the carrier of W by RMOD_2:def 2;
   hence (0).V + W = W by Lm3;
   hence thesis by Lm1;
  end;

Lm4:
 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
 proof
  let W,W',W1 be Submodule of V such that
A1: the carrier of W = the carrier of W';
  A2: now
   set W1W = {v1 + v2 : v1 in W1 & v2 in W};
   set W1W' = {v1 + v2 : v1 in W1 & v2 in W'};
   let v;
   thus v in W1 + W implies v in W1 + W'
    proof assume v in W1 + W;
     then v in the carrier of W1 + W by RLVECT_1:def 1;
     then v in W1W by Def1;
     then consider v1,v2 such that
A3:    v = v1 + v2 and
A4:    v1 in W1 and
A5:    v2 in W;
       v2 in the carrier of W' by A1,A5,RLVECT_1:def 1;
     then v2 in W' by RLVECT_1:def 1;
     then v in W1W' by A3,A4;
     then v in the carrier of W1 + W' by Def1;
     hence thesis by RLVECT_1:def 1;
    end;
   assume v in W1 + W';
   then v in the carrier of W1 + W' by RLVECT_1:def 1;
   then v in W1W' by Def1;
   then consider v1,v2 such that
A6:  v = v1 + v2 and
A7:  v1 in W1 and
A8:  v2 in W';
     v2 in the carrier of W by A1,A8,RLVECT_1:def 1;
   then v2 in W by RLVECT_1:def 1;
   then v in W1W by A6,A7;
   then v in the carrier of W1 + W by Def1;
   hence v in W1 + W by RLVECT_1:def 1;
  end;
  hence
   W1 + W = W1 + W' by RMOD_2:38;
    W1 + W = W + W1 & W1 + W' = W' + W1 by Lm1;
  hence thesis by A2,RMOD_2:38;
 end;

Lm5: for W being Submodule of V holds W is Submodule of (Omega).V
 proof let W be Submodule of V;
A1:  the RightModStr of V = (Omega).V by RMOD_2:def 4;
  hence the carrier of W c= the carrier of (Omega).V
    by RMOD_2:def 2;
  thus thesis by A1,RMOD_2:def 2;
 end;

theorem Th14:
 for V being strict RightMod of R
 holds (0).V + (Omega).V = V & (Omega).V + (0).V = V
  proof let V be strict RightMod of R;
    consider W' being strict Submodule of V such that
A1:
     the carrier of W' = the carrier of (Omega).V;
A2:  the carrier of W' = the carrier of V
       by A1,RMOD_2:def 4;
   thus (0).V + (Omega).V = (0).V + W' by A1,Lm4
                     .= W' by Th13
                     .= V by A2,RMOD_2:39;
   hence thesis by Lm1;
  end;

theorem Th15:
 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
  proof let V be RightMod of R, W be Submodule of V;
    consider W' being strict Submodule of V such that
A1: the carrier of W' = the carrier of (Omega).V;
A2:  the RightModStr of V = (Omega).V by RMOD_2:def 4;
then A3: the carrier of W c=
         the carrier of W' by A1,RMOD_2:def 2;
A4:   W' is Submodule of (Omega).V by Lm5;
      W + (Omega).V = W + W' by A1,Lm4
                  .= W' by A3,Lm3
                  .= the RightModStr of V by A1,A2,A4,RMOD_2:39;
   hence thesis by Lm1;
  end;

theorem
   for V being strict RightMod of R holds (Omega).V + (Omega).V = V by Th15;

theorem
   for W being strict Submodule of V
 holds W /\ W = W
  proof let W be strict Submodule of V;
     the carrier of W =
    (the carrier of W) /\ the carrier of W;
   hence thesis by Def2;
  end;

theorem Th18:
 W1 /\ W2 = W2 /\ W1
  proof
     the carrier of W1 /\ W2 =(the carrier of W2) /\ (the carrier of W1) by
Def2
;
   hence thesis by Def2;
  end;

theorem Th19:
 W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
  proof
        set V1 = the carrier of W1;
        set V2 = the carrier of W2;
        set V3 = the carrier of W3;
      (the carrier of W1 /\ (W2 /\ W3)) = V1 /\ (the carrier of W2 /\ W3) by
Def2
        .= V1 /\ (V2 /\ V3) by Def2
        .= (V1 /\ V2) /\ V3 by XBOOLE_1:16
        .= (the carrier of W1 /\ W2) /\ V3 by Def2;
   hence thesis by Def2;
  end;

Lm6: the carrier of W1 /\ W2 c= the carrier of W1
 proof
     the carrier of W1 /\ W2 =
   (the carrier of W1) /\ (the carrier of W2) by Def2;
  hence thesis by XBOOLE_1:17;
 end;

theorem Th20:
 W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2
  proof the carrier of W1 /\ W2 c=
        the carrier of W1 by Lm6;
   hence W1 /\ W2 is Submodule of W1 by RMOD_2:35;
      the carrier of W2 /\ W1 c= the carrier of W2 by Lm6;
    then the carrier of W1 /\ W2 c=
         the carrier of W2 by Th18;
   hence thesis by RMOD_2:35;
  end;

theorem Th21:
 (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
  proof
   thus for W1 being strict Submodule of V
     holds W1 is Submodule of W2 implies W1 /\ W2 = W1
    proof let W1 be strict Submodule of V;
      assume W1 is Submodule of W2;
       then A1: the carrier of W1 c=
               the carrier of W2 by RMOD_2:def 2;
         the carrier of W1 /\ W2 =
        (the carrier of W1) /\ (the carrier of W2) by Def2;
       then the carrier of W1 /\ W2 =
            the carrier of W1 by A1,XBOOLE_1:28;
     hence thesis by RMOD_2:37;
    end;
   thus thesis by Th20;
  end;

theorem
   W1 is Submodule of W2 implies W1 /\ W3 is Submodule of W2 /\ W3
  proof assume A1: W1 is Submodule of W2;
   set A1 = the carrier of W1;
   set A2 = the carrier of W2;
   set A3 = the carrier of W3;
   set A4 = the carrier of W1 /\ W3;
      A1 c= A2 by A1,RMOD_2:def 2;
    then A1 /\ A3 c= A2 /\ A3 by XBOOLE_1:26;
    then A4 c= A2 /\ A3 by Def2;
    then A4 c= (the carrier of W2 /\ W3) by Def2;
   hence thesis by RMOD_2:35;
  end;

theorem
   W1 is Submodule of W3 implies W1 /\ W2 is Submodule of W3
  proof assume A1: W1 is Submodule of W3;
     W1 /\ W2 is Submodule of W1 by Th20;
   hence thesis by A1,RMOD_2:34;
  end;

theorem
   W1 is Submodule of W2 & W1 is Submodule of W3 implies
  W1 is Submodule of W2 /\ W3
   proof assume A1: W1 is Submodule of W2 & W1 is Submodule of W3;
       now let v;
      assume v in W1;
       then v in W2 & v in W3 by A1,RMOD_2:16;
     hence v in W2 /\ W3 by Th7;
    end;
   hence thesis by RMOD_2:36;
 end;

theorem Th25:
 (0).V /\ W = (0).V & W /\ (0).V = (0).V
  proof
    A1: the carrier of (0).V /\ W
           = (the carrier of (0).V) /\
             (the carrier of W) by Def2
          .= {0.V} /\ (the carrier of W) by RMOD_2:def 3;
      0.V in W by RMOD_2:25;
    then 0.V in the carrier of W by RLVECT_1:def 1;
    then {0.V} c= the carrier of W by ZFMISC_1:37;
    then {0.V} /\ (the carrier of W) = {0.V} &
         the carrier of (0).V = {0.V} by RMOD_2:def 3,XBOOLE_1:28;
   hence (0).V /\ W = (0).V by A1,RMOD_2:37;
   hence thesis by Th18;
  end;

canceled;

theorem Th27:
 for W being strict Submodule of V
 holds (Omega).V /\ W = W & W /\ (Omega).V = W
  proof let W be strict Submodule of V;
A1: the carrier of the RightModStr of V = the carrier of V;
    A2: the carrier of (Omega).V /\ W =
     (the carrier of (Omega).V) /\ (the carrier of W) by Def2
  .= (the carrier of V) /\ (the carrier of W) by A1,RMOD_2:def 4;
      the carrier of W c= the carrier of V by RMOD_2:def 2;
    then the carrier of (Omega).V /\ W =
         the carrier of W by A2,XBOOLE_1:28;
   hence (Omega).V /\ W = W by RMOD_2:37;
   hence thesis by Th18;
  end;

Lm7:
 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
 proof
  let W,W',W1 be Submodule of V such that
A1: the carrier of W = the carrier of W';
  A2: now
   thus the carrier of W1 /\ W
     = (the carrier of W1) /\ (the carrier of W')
        by A1,Def2
    .= the carrier of W1 /\ W' by Def2;
  end;
  hence
   W1 /\ W = W1 /\ W' by RMOD_2:37;
    W1 /\ W = W /\ W1 & W1 /\ W' = W' /\ W1 by Th18;
  hence thesis by A2,RMOD_2:37;
 end;

theorem
   for V being strict RightMod of R holds (Omega).V /\ (Omega).V = V
  proof let V be strict RightMod of R;
    consider W' being strict Submodule of V such that
A1: the carrier of W' = the carrier of (Omega).V;
A2: V = (Omega).V by RMOD_2:def 4;
   thus (Omega).V /\ (Omega).V = (Omega).V /\ W' by A1,Lm7
                     .= W' by Th27
                     .= V by A1,A2,RMOD_2:39;
  end;

Lm8: the carrier of W1 /\ W2 c= the carrier of W1 + W2
 proof the carrier of W1 /\ W2 c=
       the carrier of W1 &
       the carrier of W1 c=
       the carrier of W1 + W2 by Lm2,Lm6;
  hence thesis by XBOOLE_1:1;
 end;

theorem
   W1 /\ W2 is Submodule of W1 + W2
  proof the carrier of W1 /\ W2 c=
        the carrier of W1 + W2 by Lm8;
   hence thesis by RMOD_2:35;
  end;

Lm9: the carrier of (W1 /\ W2) + W2 =
     the carrier of W2
 proof
  thus the carrier of (W1 /\ W2) + W2 c=
   the carrier of W2
    proof let x be set;
      assume x in the carrier of (W1 /\ W2) + W2;
        then x in {u + v : u in W1 /\ W2 & v in W2} by Def1;
       then consider u,v such that A1: x = u + v and
                                   A2: u in W1 /\ W2 and A3: v in W2;
          u in W2 by A2,Th7;
        then u + v in W2 by A3,RMOD_2:28;
     hence thesis by A1,RLVECT_1:def 1;
    end;
  let x be set;
   assume A4: x in the carrier of W2;
      the carrier of W2 c=
    the carrier of W2 + (W1 /\ W2) by Lm2;
    then the carrier of W2 c=
         the carrier of (W1 /\ W2) + W2 by Lm1;
  hence thesis by A4;
 end;

theorem Th30:
 for W2 being strict Submodule of V holds (W1 /\ W2) + W2 = W2
  proof let W2 be strict Submodule of V;
     the carrier of (W1 /\ W2) + W2 =
        the carrier of W2 by Lm9;
   hence thesis by RMOD_2:37;
  end;

Lm10: the carrier of W1 /\ (W1 + W2) = the carrier of W1
 proof
  thus the carrier of W1 /\ (W1 + W2) c=
       the carrier of W1
   proof let x be set;
     assume A1: x in the carrier of W1 /\ (W1 + W2);
        the carrier of W1 /\ (W1 + W2) =
         (the carrier of W1) /\
         (the carrier of W1 + W2) by Def2;
    hence thesis by A1,XBOOLE_0:def 3;
   end;
  let x be set;
   assume A2: x in the carrier of W1;
       the carrier of W1 c= the carrier of V by RMOD_2:def 2;
    then reconsider x1 = x as Element of V by A2;
       x1 + 0.V = x1 & 0.V in W2 & x in
 W1 by A2,RLVECT_1:def 1,RMOD_2:25,VECTSP_1:7;
     then x in {u + v : u in W1 & v in W2};
     then x in the carrier of W1 + W2 by Def1;
     then x in (the carrier of W1) /\
              (the carrier of W1 + W2) by A2,XBOOLE_0:def 3;
  hence thesis by Def2;
 end;

theorem Th31:
 for W1 being strict Submodule of V holds W1 /\ (W1 + W2) = W1
  proof let W1 be strict Submodule of V;
     the carrier of W1 /\ (W1 + W2) =
        the carrier of W1 by Lm10;
   hence thesis by RMOD_2:37;
  end;

Lm11: the carrier of (W1 /\ W2) + (W2 /\ W3) c=
     the carrier of W2 /\ (W1 + W3)
 proof
  let x be set;
   assume x in the carrier of (W1 /\ W2) + (W2 /\ W3);
     then x in {u + v : u in W1 /\ W2 & v in W2 /\ W3} by Def1;
    then consider u,v such that A1: x = u + v and
                                A2: u in W1 /\ W2 & v in W2 /\ W3;
       u in W1 & u in W2 & v in W2 & v in W3 by A2,Th7;
     then x in W1 + W3 & x in W2 by A1,Th5,RMOD_2:28;
     then x in W2 /\ (W1 + W3) by Th7;
  hence thesis by RLVECT_1:def 1;
 end;

theorem
   (W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3)
  proof
      the carrier of (W1 /\ W2) + (W2 /\ W3) c=
    the carrier of W2 /\ (W1 + W3) by Lm11;
   hence thesis by RMOD_2:35;
  end;

Lm12: W1 is Submodule of W2 implies
      the carrier of W2 /\ (W1 + W3) =
      the carrier of (W1 /\ W2) + (W2 /\ W3)
 proof assume A1: W1 is Submodule of W2;
  thus the carrier of W2 /\ (W1 + W3) c=
       the carrier of (W1 /\ W2) + (W2 /\ W3)
   proof let x be set;
     assume x in the carrier of W2 /\ (W1 + W3);
      then A2: x in (the carrier of W2) /\
                  (the carrier of W1 + W3) by Def2;
      then x in the carrier of W1 + W3 by XBOOLE_0:def 3;
      then x in {u + v : u in W1 & v in W3} by Def1;
     then consider u1,v1 such that A3: x = u1 + v1 and
                                   A4: u1 in W1 and A5: v1 in W3;
      A6: u1 in W2 by A1,A4,RMOD_2:16;
      then A7: u1 in W1 /\ W2 by A4,Th7;
        x in the carrier of W2 by A2,XBOOLE_0:def 3;
      then u1 + v1 in W2 by A3,RLVECT_1:def 1;
      then (v1 + u1) - u1 in W2 by A6,RMOD_2:31;
      then v1 + (u1 - u1) in W2 by RLVECT_1:42;
      then v1 + 0.V in W2 by VECTSP_1:66;
      then v1 in W2 by VECTSP_1:7;
      then v1 in W2 /\ W3 by A5,Th7;
      then x in (W1 /\ W2) + (W2 /\ W3) by A3,A7,Th5;
    hence thesis by RLVECT_1:def 1;
   end;
 thus thesis by Lm11;
end;

theorem Th33:
 W1 is Submodule of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
  proof
   assume W1 is Submodule of W2;
    then the carrier of W2 /\ (W1 + W3) =
         the carrier of (W1 /\ W2) + (W2 /\ W3) by Lm12;
   hence thesis by RMOD_2:37;
  end;

Lm13: the carrier of W2 + (W1 /\ W3) c=
        the carrier of (W1 + W2) /\ (W2 + W3)
   proof let x be set;
     assume x in the carrier of W2 + (W1 /\ W3);
       then x in {u + v : u in W2 & v in W1 /\ W3} by Def1;
      then consider u,v such that A1: x = u + v and
                                  A2: u in W2 and A3: v in W1 /\ W3;
         v in W1 & v in W3 & x = v + u by A1,A3,Th7;
       then x in {v1 + v2 : v1 in W1 & v2 in W2} &
            x in {u1 + u2 : u1 in W2 & u2 in W3} by A2;
       then x in the carrier of W1 + W2 &
            x in the carrier of W2 + W3 by Def1;
       then x in (the carrier of W1 + W2) /\
                (the carrier of W2 + W3) by XBOOLE_0:def 3;
    hence thesis by Def2;
   end;

theorem
   W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3)
  proof the carrier of W2 + (W1 /\ W3) c=
        the carrier of (W1 + W2) /\ (W2 + W3) by Lm13;
   hence thesis by RMOD_2:35;
  end;

Lm14: W1 is Submodule of W2 implies
        the carrier of W2 + (W1 /\ W3) =
         the carrier of (W1 + W2) /\ (W2 + W3)
 proof assume A1: W1 is Submodule of W2;
   reconsider V2 = the carrier of W2 as Subset of V
         by RMOD_2:def 2;
  thus the carrier of W2 + (W1 /\ W3) c=
       the carrier of (W1 + W2) /\ (W2 + W3) by Lm13;
  let x be set;
   assume x in the carrier of (W1 + W2) /\ (W2 + W3);
     then x in (the carrier of W1 + W2) /\
              (the carrier of W2 + W3) by Def2;
     then x in the carrier of W1 + W2 by XBOOLE_0:def 3;
     then x in {u1 + u2 : u1 in W1 & u2 in W2} by Def1;
    then consider u1,u2 such that A2: x = u1 + u2 and
                                  A3: u1 in W1 and A4: u2 in W2;
     A5: u1 in the carrier of W1 by A3,RLVECT_1:def 1;
     A6: u2 in the carrier of W2 by A4,RLVECT_1:def 1;
       the carrier of W1 c= the carrier of W2 by A1,RMOD_2:def 2;
     then u1 in the carrier of W2 & V2 is lineary-closed by A5,RMOD_2:41;
     then u1 + u2 in V2 by A6,RMOD_2:def 1;
     then A7: u1 + u2 in W2 by RLVECT_1:def 1;
     A8: 0.V in W1 /\ W3 by RMOD_2:25;
       (u1 + u2) + 0.V = u1 + u2 by VECTSP_1:7;
     then x in {u + v : u in W2 & v in W1 /\ W3} by A2,A7,A8;
  hence thesis by Def1;
 end;

theorem
   W1 is Submodule of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
  proof
   assume W1 is Submodule of W2;
    then the carrier of W2 + (W1 /\ W3) =
         the carrier of (W1 + W2) /\ (W2 + W3) by Lm14;
   hence thesis by RMOD_2:37;
  end;

theorem Th36:
 for W1 being strict Submodule of V
 holds W1 is Submodule of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3
  proof let W1 be strict Submodule of V;
   assume A1: W1 is Submodule of W3;
   thus (W1 + W2) /\ W3 = W3 /\ (W1 + W2) by Th18
                      .= (W1 /\ W3) + (W3 /\ W2) by A1,Th33
                      .= W1 + (W3 /\ W2) by A1,Th21
                      .= W1 + (W2 /\ W3) by Th18;
  end;

theorem
   for W1,W2 being strict Submodule of V
 holds W1 + W2 = W2 iff W1 /\ W2 = W1
  proof let W1,W2 be strict Submodule of V;
       (W1 + W2 = W2 iff W1 is Submodule of W2) &
    (W1 /\ W2 = W1 iff W1 is Submodule of W2) by Th12,Th21;
   hence thesis;
  end;

theorem
   for W2,W3 being strict Submodule of V
 holds W1 is Submodule of W2 implies W1 + W3 is Submodule of W2 + W3
  proof let W2,W3 be strict Submodule of V;
   assume A1: W1 is Submodule of W2;
      (W1 + W3) + (W2 + W3) = (W1 + W3) + (W3 + W2) by Lm1
                         .= ((W1 + W3) + W3) + W2 by Th10
                         .= (W1 + (W3 + W3)) + W2 by Th10
                         .= (W1 + W3) + W2 by Lm3
                         .= W1 + (W3 + W2) by Th10
                         .= W1 + (W2 + W3) by Lm1
                         .= (W1 + W2) + W3 by Th10
                         .= W2 + W3 by A1,Th12;
   hence thesis by Th12;
  end;

theorem
   W1 is Submodule of W2 implies W1 is Submodule of W2 + W3
 proof assume A1: W1 is Submodule of W2;
     W2 is Submodule of W2 + W3 by Th11;
  hence thesis by A1,RMOD_2:34;
 end;

theorem
   W1 is Submodule of W3 & W2 is Submodule of W3 implies
       W1 + W2 is Submodule of W3
 proof assume A1: W1 is Submodule of W3 & W2 is Submodule of W3;
     now let v;
     assume v in W1 + W2;
      then consider v1,v2 such that A2: v1 in W1 & v2 in W2 and A3: v = v1 + v2
                                                                       by Th5;
         v1 in W3 & v2 in W3 by A1,A2,RMOD_2:16;
    hence v in W3 by A3,RMOD_2:28;
   end;
  hence thesis by RMOD_2:36;
 end;

theorem
   (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
   proof
     set VW1 = the carrier of W1;
     set VW2 = the carrier of W2;
    thus (ex W st the carrier of W =
       (the carrier of W1) \/ (the carrier of W2))
        implies W1 is Submodule of W2 or W2 is Submodule of W1
     proof given W such that
            A1: the carrier of W =
                (the carrier of W1) \/
                (the carrier of W2);
        set VW = the carrier of W;
       assume not W1 is Submodule of W2 & not W2 is Submodule of W1;
         then A2: not VW1 c= VW2 & not VW2 c= VW1 by RMOD_2:35;
        then consider x being set such that A3: x in VW1 and A4: not x in VW2
                                                     by TARSKI:def 3;
        consider y being set such that A5: y in VW2 and A6: not y in VW1 by A2,
TARSKI:def 3;
        reconsider x as Element of VW1 by A3;
        reconsider x as Vector of V by RMOD_2:18;
        reconsider y as Element of VW2 by A5;
        reconsider y as Vector of V by RMOD_2:18;
        reconsider A1 = VW as Subset of V by RMOD_2:def 2;
           x in VW & y in VW & A1 is lineary-closed by A1,RMOD_2:41,XBOOLE_0:
def 2;
         then A7: x + y in VW by RMOD_2:def 1;
         A8: now assume A9: x + y in VW1;
           reconsider A2 = VW1 as Subset of V by RMOD_2:def 2;
              A2 is lineary-closed by RMOD_2:41;
            then (y + x) - x in VW1 by A9,RMOD_2:6;
            then y + (x - x) in VW1 by RLVECT_1:42;
            then y + 0.V in VW1 by VECTSP_1:66;
          hence contradiction by A6,VECTSP_1:7;
         end;
           now assume A10: x + y in VW2;
           reconsider A2 = VW2 as Subset of V by RMOD_2:def 2;
              A2 is lineary-closed by RMOD_2:41;
            then (x + y) - y in VW2 by A10,RMOD_2:6;
            then x + (y - y) in VW2 by RLVECT_1:42;
            then x + 0.V in VW2 by VECTSP_1:66;
          hence contradiction by A4,VECTSP_1:7;
         end;
      hence thesis by A1,A7,A8,XBOOLE_0:def 2;
     end;
     assume A11: W1 is Submodule of W2 or W2 is Submodule of W1;
      A12: now assume W1 is Submodule of W2;
        then VW1 c= VW2 by RMOD_2:def 2;
        then VW1 \/ VW2 = VW2 by XBOOLE_1:12;
       hence thesis;
      end;
        now assume W2 is Submodule of W1;
        then VW2 c= VW1 by RMOD_2:def 2;
        then VW1 \/ VW2 = VW1 by XBOOLE_1:12;
       hence thesis;
      end;
    hence thesis by A11,A12;
   end;

 definition let R; let V;
  func Submodules(V) -> set means
   :Def3:  for x holds x in it iff
    ex W being strict Submodule of V st W = x;
  existence
   proof
     defpred P[set] means
         ex W being strict Submodule of V st $1 = the carrier of W;
     consider B being set such that
      A1: for x holds x in B iff x in bool the carrier of V & P[x]
       from Separation;
      defpred Q[set,set] means
        (ex W being strict Submodule of V st $2 = W &
             $1 = the carrier of W);
       A2: for x,y1,y2 st Q[x,y1] & Q[x,y2]
       holds y1 = y2 by RMOD_2:37;
     consider f being Function such that
      A3: for x,y holds [x,y] in f iff x in B & Q[x,y]
           from GraphFunc(A2);
        for x holds x in B iff ex y st [x,y] in f
       proof let x;
        thus x in B implies ex y st [x,y] in f
         proof assume A4: x in B;
           then consider W being strict Submodule of V such that
            A5: x = the carrier of W by A1;
          take W;
          thus thesis by A3,A4,A5;
         end;
         given y such that A6: [x,y] in f;
        thus thesis by A3,A6;
       end;
      then A7: B = dom f by RELAT_1:def 4;
        for y holds y in rng f iff
        ex W being strict Submodule of V st y = W
       proof let y;
        thus y in rng f implies
         ex W being strict Submodule of V st
           y = W
         proof assume y in rng f;
           then consider x such that A8: x in dom f & y = f.x by FUNCT_1:def 5;
              [x,y] in f by A8,FUNCT_1:def 4;
            then ex W being strict Submodule of V st y = W &
             x = the carrier of W by A3;
          hence thesis;
         end;
         given W being strict Submodule of V such that
A9:        y = W;
          reconsider W = y as Submodule of V by A9;
          reconsider x = the carrier of W as set;
             the carrier of W c=
           the carrier of V by RMOD_2:def 2;
           then A10: x in dom f by A1,A7,A9;
           then [x,y] in f by A3,A7,A9;
           then y = f.x by A10,FUNCT_1:def 4;
        hence thesis by A10,FUNCT_1:def 5;
       end;
    hence thesis;
   end;
  uniqueness
    proof
      defpred P[set] means ex W being strict Submodule of V
         st W = $1;
      for X1,X2 being set st
         (for x being set holds x in X1 iff P[x]) &
         (for x being set holds x in X2 iff P[x]) holds X1 = X2
             from SetEq;
      hence thesis;
    end;
 end;

 definition let R; let V;
  cluster Submodules(V) -> non empty;
  coherence
  proof
    consider W being strict Submodule of V;
      W in Submodules(V) by Def3;
    hence thesis;
  end;
 end;



canceled 2;

theorem
   for V being strict RightMod of R
 holds V in Submodules(V)
  proof let V be strict RightMod of R;
    consider W' being strict Submodule of V such that
A1:
     the carrier of (Omega).V = the carrier of W';
A2:  the carrier of V = the carrier of W'
       by A1,RMOD_2:def 4;
      W' in Submodules(V) by Def3;
   hence thesis by A2,RMOD_2:39;
  end;

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

Lm15:
 for V being RightMod of R, W1,W2 being Submodule of V holds
 W1 + W2 = the RightModStr 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
  proof let V be RightMod of R, W1,W2 be Submodule of V;
A1:  the RightModStr of V = (Omega).V by RMOD_2:def 4;
   thus W1 + W2 = the RightModStr of V implies
    for v being Vector of V
     ex v1,v2 being Vector of V st v1 in W1 & v2 in W2 & v = v1 + v2
    proof assume A2: W1 + W2 = the RightModStr of V;
     let v be Vector of V;
        v in (Omega).V by A1,RLVECT_1:3;
     hence thesis by A1,A2,Th5;
    end;
    assume A3: for v being Vector of V
      ex v1,v2 being Vector of V st v1 in W1 & v2 in W2 & v = v1 + v2;
       now
      thus W1 + W2 is Submodule of (Omega).V by Lm5;
      let u be Vector of V;
          ex v1,v2 being Vector of V st v1 in W1 & v2 in W2 & u = v1 + v2 by A3
;
      hence u in W1 + W2 by Th5;
     end;
   hence thesis by A1,RMOD_2:40;
  end;

Lm16: v = v1 + v2 iff v1 = v - v2
 proof
  thus v = v1 + v2 implies v1 = v - v2
   proof assume A1: v = v1 + v2;
    thus v1 = 0.V + v1 by VECTSP_1:7
           .= v + (- (v2 + v1)) + v1 by A1,VECTSP_1:66
           .= v + ((- v2) + (- v1)) + v1 by RLVECT_1:45
           .= (v + (- v2)) + (- v1) + v1 by RLVECT_1:def 6
           .= (v + (- v2)) + ((- v1) + v1) by RLVECT_1:def 6
           .= v + (- v2) + 0.V by RLVECT_1:16
           .= v + (- v2) by VECTSP_1:7
           .= v - v2 by RLVECT_1:def 11;
   end;
   assume A2: v1 = v - v2;
  thus v = v + 0.V by VECTSP_1:7
        .= v + (v1 + (- v1)) by RLVECT_1:16
        .= (v + v1) + (- (v - v2)) by A2,RLVECT_1:def 6
        .= (v + v1) + ((- v) + v2) by RLVECT_1:47
        .= (v + v1) + (- v) + v2 by RLVECT_1:def 6
        .= v + (- v) + v1 + v2 by RLVECT_1:def 6
        .= 0.V + v1 + v2 by RLVECT_1:16
        .= v1 + v2 by VECTSP_1:7;
 end;

canceled;

theorem
Th46: V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2,W1
 proof assume V is_the_direct_sum_of W1,W2;
   then the RightModStr of V = W1 + W2 & W1 /\ W2 = (0).V by Def4;
   then the RightModStr of V = W2 + W1 & W2 /\ W1 = (0).V by Lm1,Th18;
  hence thesis by Def4;
 end;

theorem
   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
   proof let V be strict RightMod of R;
       (0).V + (Omega).V = V & (0).V = (0).V /\ (Omega).V by Th14,Th25;
    hence V is_the_direct_sum_of (0).V,(Omega).V by Def4;
    hence thesis by Th46;
   end;

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

theorem Th48:
 C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2
   proof assume A1: C1 /\ C2 <> {};
     consider v being Element of C1 /\ C2;
     reconsider v as Element of V by A1,TARSKI:def 3;
     set C = C1 /\ C2;
        v in C1 by A1,XBOOLE_0:def 3;
      then A2: C1 = v + W1 by RMOD_2:90;
        v in C2 by A1,XBOOLE_0:def 3;
      then A3: C2 = v + W2 by RMOD_2:90;
        C is Coset of W1 /\ W2
       proof
        take v;
        thus C c= v + W1 /\ W2
         proof let x;
          assume A4: x in C;
            then x in C1 by XBOOLE_0:def 3;
           then consider u1 such that A5: u1 in W1 and A6: x = v + u1
                                                             by A2,RMOD_2:57;
              x in C2 by A4,XBOOLE_0:def 3;
           then consider u2 such that A7: u2 in W2 and A8: x = v + u2
                                                            by A3,RMOD_2:57;
              u1 = u2 by A6,A8,RLVECT_1:21;
            then u1 in W1 /\ W2 by A5,A7,Th7;
            then x in {v + u : u in W1 /\ W2} by A6;
          hence thesis by RMOD_2:def 5;
         end;
        let x;
         assume x in v + (W1 /\ W2);
          then consider u such that A9: u in W1 /\ W2 and A10: x = v + u
                                                           by RMOD_2:57;
             u in W1 & u in W2 by A9,Th7;
           then x in {v + u1 : u1 in W1} & x in {v + u2 : u2 in W2} by A10;
           then x in C1 & x in C2 by A2,A3,RMOD_2:def 5;
        hence thesis by XBOOLE_0:def 3;
       end;
    hence thesis;
   end;

theorem Th49:
 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}
   proof let V be RightMod of R, W1,W2 be Submodule of V;
      set VW1 = the carrier of W1;
      set VW2 = the carrier of W2;
      A1: VW1 is Coset of W1 & VW2 is Coset of W2 by RMOD_2:86;
    thus V is_the_direct_sum_of W1,W2 implies
     for C1 being Coset of W1, C2 being Coset of W2
      ex v being Vector of V st C1 /\ C2 = {v}
     proof assume A2: V is_the_direct_sum_of W1,W2;
      let C1 be Coset of W1, C2 be Coset of W2;
A3:    the RightModStr of V = (Omega).V by RMOD_2:def 4;
       consider v1 being Vector of V such that A4: C1 = v1 + W1 by RMOD_2:def 6
;
       consider v2 being Vector of V such that A5: C2 = v2 + W2 by RMOD_2:def 6
;
        A6: the RightModStr of V = W1 + W2 by A2,Def4;
          v1 in (Omega).V by A3,RLVECT_1:3;
       then consider v11,v12 being Vector of V such that A7: v11 in W1 and
        A8: v12 in W2 and A9: v1 = v11 + v12 by A3,A6,Th5;
          v2 in (Omega).V by A3,RLVECT_1:3;
       then consider v21,v22 being Vector of V such that A10: v21 in W1 and
        A11: v22 in W2 and A12: v2 = v21 + v22 by A3,A6,Th5;
      take v = v12 + v21;
         {v} = C1 /\ C2
        proof
         thus A13: {v} c= C1 /\ C2
          proof let x;
            assume x in {v};
             then A14: x = v by TARSKI:def 1;
               v12 = v1 - v11 by A9,Lm16;
             then v12 in C1 by A4,A7,RMOD_2:75;
             then C1 = v12 + W1 by RMOD_2:90;
             then A15: x in C1 by A10,A14,RMOD_2:57;
               v21 = v2 - v22 by A12,Lm16;
             then v21 in C2 by A5,A11,RMOD_2:75;
             then C2 = v21 + W2 & v = v21 + v12 by RMOD_2:90;
             then x in C2 by A8,A14,RMOD_2:57;
           hence thesis by A15,XBOOLE_0:def 3;
          end;
         let x;
          assume A16: x in C1 /\ C2;
           then C1 meets C2 by XBOOLE_0:4;
           then reconsider C = C1 /\ C2 as Coset of W1 /\ W2 by Th48;
              W1 /\ W2 = (0).V by A2,Def4;
           then A17: ex u being Vector of V st C = {u} by RMOD_2:85;
              v in {v} by TARSKI:def 1;
            hence thesis by A13,A16,A17,TARSKI:def 1;
         thus thesis;
        end;
       hence C1 /\ C2 = {v};
      end;
     assume A18: for C1 being Coset of W1, C2 being Coset of W2
      ex v being Vector of V st C1 /\ C2 = {v};
A19:   W1 + W2 is Submodule of (Omega).V & the RightModStr of V = (Omega).V
        by Lm5,RMOD_2:def 4;
         the carrier of V = the carrier of W1 + W2
        proof
         thus the carrier of V c=
              the carrier of W1 + W2
          proof let x;
            assume x in the carrier of V;
             then reconsider u = x as Vector of V;
             consider C1 being Coset of W1 such that
             A20: u in C1 by RMOD_2:81;
             consider v being Vector of V such that A21: C1 /\
              VW2 = {v} by A1,A18;
              A22: v in {v} by TARSKI:def 1;
              then v in VW2 by A21,XBOOLE_0:def 3;
              then A23: v in W2 by RLVECT_1:def 1;
                v in C1 by A21,A22,XBOOLE_0:def 3;
             then consider v1 being Vector of V such that A24: v1 in W1 and
              A25: u - v1 = v by A20,RMOD_2:92;
                u = v1 + v by A25,Lm16;
              then x in W1 + W2 by A23,A24,Th5;
           hence thesis by RLVECT_1:def 1;
          end;
         thus thesis by RMOD_2:def 2;
        end;
    hence the RightModStr of V = W1 + W2 by A19,RMOD_2:39;
      consider v being Vector of V such that A26: VW1 /\ VW2 = {v} by A1,A18;
         0.V in W1 & 0.V in W2 by RMOD_2:25;
       then 0.V in VW1 & 0.V in VW2 by RLVECT_1:def 1;
       then A27: 0.V in {v} by A26,XBOOLE_0:def 3;
         the carrier of (0).V = {0.V} by RMOD_2:def 3
                           .= VW1 /\ VW2 by A26,A27,TARSKI:def 1
                           .= the carrier of W1 /\ W2 by Def2;
    hence thesis by RMOD_2:37;
   end;

theorem
   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 by Lm15;

theorem Th51:
 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
     proof let V be RightMod of R, W1,W2 be Submodule of V,
               v,v1,v2,u1,u2 be Vector of V;
      assume A1: V is_the_direct_sum_of W1,W2;
       assume that A2: v = v1 + v2 & v = u1 + u2 and A3: v1 in W1 & u1 in
 W1 and
                   A4: v2 in W2 & u2 in W2;
        reconsider C2 = v1 + W2 as Coset of W2 by RMOD_2:def 6;
        reconsider C1 = the carrier of W1 as Coset of W1 by RMOD_2:86;
         A5: u1 = (v1 + v2) - u2 by A2,Lm16
              .= v1 + (v2 - u2) by RLVECT_1:42;
           v2 - u2 in W2 by A4,RMOD_2:31;
         then v1 in C1 & v1 in C2 & u1 in C1 & u1 in C2 by A3,A5,RLVECT_1:def 1
,RMOD_2:57,59;
         then A6: v1 in C1 /\ C2 & u1 in C1 /\ C2 by XBOOLE_0:def 3;
        consider u being Vector of V such that A7: C1 /\ C2 = {u} by A1,Th49;
A8:         v1 = u & u1 = u by A6,A7,TARSKI:def 1;
      hence v1 = u1;
      thus v2 = u2 by A2,A8,RLVECT_1:21;
     end;

theorem
   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
  proof assume A1: V = W1 + W2;
    given v such that A2: 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;
      A3: the carrier of (0).V = {0.V} by RMOD_2:def 3;
    assume not thesis;
      then W1 /\ W2 <> (0).V by A1,Def4;
      then the carrier of W1 /\ W2 <>
           the carrier of (0).V &
           (0).V is Submodule of W1 /\ W2 by RMOD_2:37,50;
      then the carrier of W1 /\ W2 <> {0.V} & {0.V} c=
           the carrier of W1 /\ W2 by A3,RMOD_2:def 2;
           then {0.V} c< the carrier of W1 /\ W2 by XBOOLE_0:def 8;
     then consider x such that A4: x in the carrier of W1 /\ W2 and
                               A5: not x in {0.V} by RLSUB_2:77;
A6:      x in W1 /\ W2 by A4,RLVECT_1:def 1;
      then A7: x in W1 & x in W2 by Th7;
      A8: x <> 0.V by A5,TARSKI:def 1;
        x in V by A6,RMOD_2:17;
     then reconsider u = x as Vector of V by RLVECT_1:def 1;
     consider v1,v2 such that A9: v1 in W1 & v2 in W2 and A10: v = v1 + v2
                                                                by A1,Lm15;
      A11: v = v1 + v2 + 0.V by A10,VECTSP_1:7
          .= (v1 + v2) + (u - u) by VECTSP_1:66
          .= ((v1 + v2) + u) - u by RLVECT_1:42
          .= ((v1 + u) + v2) - u by RLVECT_1:def 6
          .= (v1 + u) + (v2 - u) by RLVECT_1:42;
        v1 + u in W1 & v2 - u in W2 by A7,A9,RMOD_2:28,31;
      then v2 - u = v2 by A2,A9,A10,A11;
      then v2 + (- u) = v2 by RLVECT_1:def 11
                     .= v2 + 0.V by VECTSP_1:7;
      then - u = 0.V by RLVECT_1:21;
      then u = - 0.V by RLVECT_1:30;
   hence thesis by A8,RLVECT_1:25;
  end;



definition let R; let V be RightMod of R;
 let v be Vector of V; let W1,W2 be Submodule of V;
 assume A1: V is_the_direct_sum_of W1,W2;
 func v |-- (W1,W2) -> Element of [:the carrier of V,
                                   the carrier of V:] means
  :Def5: v = it`1 + it`2 & it`1 in W1 & it`2 in W2;
 existence
  proof
    W1 + W2 = the RightModStr of V by A1,Def4;
    then consider v1,v2 being Vector of V such that
    A2: v1 in W1 & v2 in W2 & v = v1 + v2 by Lm15;
   take [v1,v2];
      [v1,v2]`1 = v1 & [v1,v2]`2 = v2 by MCART_1:7;
   hence thesis by A2;
  end;
 uniqueness
  proof let t1,t2 be Element of [:the carrier of V,
              the carrier of V:];
    assume v = t1`1 + t1`2 & t1`1 in W1 & t1`2 in W2 &
           v = t2`1 + t2`2 & t2`1 in W1 & t2`2 in W2;
     then t1`1 = t2`1 & t1`2 = t2`2 & t1 = [t1`1,t1`2] & t2 = [t2`1,t2`2]
                                                by A1,Th51,MCART_1:23;
   hence thesis;
  end;
end;

canceled 4;

theorem
   V is_the_direct_sum_of W1,W2 implies
  (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2
   proof assume A1: V is_the_direct_sum_of W1,W2;
     then A2: v = (v |-- (W1,W2))`1 + (v |-- (W1,W2))`2 & (v |-- (W1,W2))`1 in
 W1 &
             (v |-- (W1,W2))`2 in W2 by Def5;
     A3: V is_the_direct_sum_of W2,W1 by A1,Th46;
     then A4: v = (v |-- (W2,W1))`2 + (v |-- (W2,W1))`1 by Def5;
       (v |-- (W2,W1))`1 in W2 & (v |-- (W2,W1))`2 in W1 by A3,Def5;
    hence thesis by A1,A2,A4,Th51;
   end;

theorem
   V is_the_direct_sum_of W1,W2 implies
  (v |-- (W1,W2))`2 = (v |-- (W2,W1))`1
   proof assume A1: V is_the_direct_sum_of W1,W2;
     then A2: v = (v |-- (W1,W2))`1 + (v |-- (W1,W2))`2 & (v |-- (W1,W2))`1 in
 W1 &
             (v |-- (W1,W2))`2 in W2 by Def5;
     A3: V is_the_direct_sum_of W2,W1 by A1,Th46;
     then A4: v = (v |-- (W2,W1))`2 + (v |-- (W2,W1))`1 by Def5;
       (v |-- (W2,W1))`1 in W2 & (v |-- (W2,W1))`2 in W1 by A3,Def5;
    hence thesis by A1,A2,A4,Th51;
   end;

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

 definition let R; let V;
  func SubJoin(V) -> BinOp of Submodules(V) means
   :Def6: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 + W2;
  existence
   proof
     defpred P[Element of Submodules(V),Element of Submodules(V),
             Element of Submodules(V)] means
         for W1,W2 st $1 = W1 & $2 = W2 holds $3 = W1 + W2;
     A1: for A1,A2 ex B st P[A1,A2,B]
      proof let A1,A2;
         consider W1 being strict Submodule of V such that
A2:       W1 = A1 by Def3;
         consider W2 being strict Submodule of V such that
A3:       W2 = A2 by Def3;
        reconsider C = W1 + W2 as Element of Submodules(V) by Def3;
       take C;
       thus thesis by A2,A3;
      end;
    ex o being BinOp of Submodules(V) st
       for a,b being Element of Submodules(V) holds P[a,b,o.(a,b)]
               from BinOpEx(A1);
     hence thesis;
   end;
  uniqueness
   proof let o1,o2 be BinOp of Submodules(V);
     assume A4: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds o1.(A1,A2) = W1 + W2
;
     assume A5: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds o2.(A1,A2) = W1 + W2
;
        now let x,y be set;
        assume A6: x in Submodules(V) & y in Submodules(V);
         then reconsider A = x, B = y as Element of Submodules(V);
         consider W1 being strict Submodule of V such that
A7:       W1 = x by A6,Def3;
         consider W2 being strict Submodule of V such that
A8:       W2 = y by A6,Def3;
            o1.(A,B) = W1 + W2 & o2.(A,B) = W1 + W2 by A4,A5,A7,A8;
          then o1.(x,y) = o2.(x,y) & o1.[x,y] = o1.(x,y) & o2.[x,y] = o2.(x,y)
                                                       by BINOP_1:def 1;
       hence o1.[x,y] = o2.[x,y];
      end;
    hence thesis by FUNCT_2:118;
   end;
 end;

 definition let R; let V;
  func SubMeet(V) -> BinOp of Submodules(V) means
   :Def7: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 /\ W2;
  existence
   proof
     defpred P[Element of Submodules(V),Element of Submodules(V),
             Element of Submodules(V)] means
         for W1,W2 st $1 = W1 & $2 = W2 holds $3 = W1 /\ W2;
     A1: for A1,A2 ex B st P[A1,A2,B]
      proof let A1,A2;
         consider W1 being strict Submodule of V such that
A2:       W1 = A1 by Def3;
         consider W2 being strict Submodule of V such that
A3:       W2 = A2 by Def3;
        reconsider C = W1 /\ W2 as Element of Submodules(V) by Def3;
       take C;
       thus thesis by A2,A3;
      end;
    ex o being BinOp of Submodules(V) st
       for a,b being Element of Submodules(V) holds P[a,b,o.(a,b)]
               from BinOpEx(A1);
     hence thesis;
   end;
  uniqueness
   proof let o1,o2 be BinOp of Submodules(V);
     assume A4: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds o1.(A1,A2) = W1 /\
W2;
     assume A5: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds o2.(A1,A2) = W1 /\
W2;
        now let x,y be set;
        assume A6: x in Submodules(V) & y in Submodules(V);
         then reconsider A = x, B = y as Element of Submodules(V);
         consider W1 being strict Submodule of V such that
A7:       W1 = x by A6,Def3;
         consider W2 being strict Submodule of V such that
A8:       W2 = y by A6,Def3;
            o1.(A,B) = W1 /\ W2 & o2.(A,B) = W1 /\ W2 by A4,A5,A7,A8;
          then o1.(x,y) = o2.(x,y) & o1.[x,y] = o1.(x,y) & o2.[x,y] = o2.(x,y)
                                                  by BINOP_1:def 1;
       hence o1.[x,y] = o2.[x,y];
      end;
    hence thesis by FUNCT_2:118;
   end;
 end;



canceled 4;

theorem Th63:
 LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is Lattice
  proof set S = LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #);
    A1: for A,B being Element of S
         holds A "\/" B = B "\/" A
     proof let A,B be Element of S;
         consider W1 being strict Submodule of V such that
A2:       W1 = A by Def3;
         consider W2 being strict Submodule of V such that
A3:       W2 = B by Def3;
      thus A "\/" B = SubJoin(V).(A,B) by LATTICES:def 1
                 .= W1 + W2 by A2,A3,Def6
                 .= W2 + W1 by Lm1
                 .= SubJoin(V).(B,A) by A2,A3,Def6
                 .= B "\/" A by LATTICES:def 1;
     end;
    A4: for A,B,C being Element of S
         holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
     proof let A,B,C be Element of S;
         consider W1 being strict Submodule of V such that
A5:       W1 = A by Def3;
         consider W2 being strict Submodule of V such that
A6:       W2 = B by Def3;
         consider W3 being strict Submodule of V such that
A7:       W3 = C by Def3;
       reconsider AB = W1 + W2, BC = W2 + W3 as
              Element of S by Def3;
      thus A "\/" (B "\/" C) = SubJoin(V).(A,B "\/" C) by LATTICES:def 1
                        .= SubJoin(V).(A,SubJoin(V).(B,C)) by LATTICES:def 1
                        .= SubJoin(V).(A,BC) by A6,A7,Def6
                        .= W1 + (W2 + W3) by A5,Def6
                        .= (W1 + W2) + W3 by Th10
                        .= SubJoin(V).(AB,C) by A7,Def6
                        .= SubJoin(V).(SubJoin(V).(A,B),C) by A5,A6,Def6
                        .= SubJoin(V).(A "\/" B,C) by LATTICES:def 1
                        .= (A "\/" B) "\/" C by LATTICES:def 1;
     end;
    A8: for A,B being Element of S
         holds (A "/\" B) "\/" B = B
     proof let A,B be Element of S;
         consider W1 being strict Submodule of V such that
A9:       W1 = A by Def3;
         consider W2 being strict Submodule of V such that
A10:       W2 = B by Def3;
       reconsider AB = W1 /\ W2 as Element of S by Def3;
      thus (A "/\" B) "\/" B = SubJoin(V).(A "/\" B,B) by LATTICES:def 1
                        .= SubJoin(V).(SubMeet(V).(A,B),B) by LATTICES:def 2
                        .= SubJoin(V).(AB,B) by A9,A10,Def7
                        .= (W1 /\ W2) + W2 by A10,Def6
                        .= B by A10,Th30;
     end;
    A11: for A,B being Element of S
         holds A "/\" B = B "/\" A
     proof let A,B be Element of S;
         consider W1 being strict Submodule of V such that
A12:       W1 = A by Def3;
         consider W2 being strict Submodule of V such that
A13:       W2 = B by Def3;
      thus A "/\" B = SubMeet(V).(A,B) by LATTICES:def 2
                 .= W1 /\ W2 by A12,A13,Def7
                 .= W2 /\ W1 by Th18
                 .= SubMeet(V).(B,A) by A12,A13,Def7
                 .= B "/\" A by LATTICES:def 2;
     end;
    A14: for A,B,C being Element of S
         holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
     proof let A,B,C be Element of S;
         consider W1 being strict Submodule of V such that
A15:       W1 = A by Def3;
         consider W2 being strict Submodule of V such that
A16:       W2 = B by Def3;
         consider W3 being strict Submodule of V such that
A17:       W3 = C by Def3;
       reconsider AB = W1 /\ W2, BC = W2 /\ W3 as
              Element of S by Def3;
      thus A "/\" (B "/\" C) = SubMeet(V).(A,B "/\" C) by LATTICES:def 2
                        .= SubMeet(V).(A,SubMeet(V).(B,C)) by LATTICES:def 2
                        .= SubMeet(V).(A,BC) by A16,A17,Def7
                        .= W1 /\ (W2 /\ W3) by A15,Def7
                        .= (W1 /\ W2) /\ W3 by Th19
                        .= SubMeet(V).(AB,C) by A17,Def7
                        .= SubMeet(V).(SubMeet(V).(A,B),C) by A15,A16,Def7
                        .= SubMeet(V).(A "/\" B,C) by LATTICES:def 2
                        .= (A "/\" B) "/\" C by LATTICES:def 2;
     end;
      for A,B being Element of S
         holds A "/\" (A "\/" B) = A
     proof let A,B be Element of S;
         consider W1 being strict Submodule of V such that
A18:       W1 = A by Def3;
         consider W2 being strict Submodule of V such that
A19:       W2 = B by Def3;
       reconsider AB = W1 + W2 as Element of S by Def3;
      thus A "/\" (A "\/" B) = SubMeet(V).(A,A "\/" B) by LATTICES:def 2
                        .= SubMeet(V).(A,SubJoin(V).(A,B)) by LATTICES:def 1
                        .= SubMeet(V).(A,AB) by A18,A19,Def6
                        .= W1 /\ (W1 + W2) by A18,Def7
                        .= A by A18,Th31;
     end;
   then S is join-commutative join-associative meet-absorbing
        meet-commutative meet-associative join-absorbing
   by A1,A4,A8,A11,A14,LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
   hence thesis by LATTICES:def 10;
end;

theorem Th64:
 LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is 0_Lattice
  proof set S = LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #);
      ex C being Element of S st
     for A being Element of S holds C "/\" A = C & A "/\" C = C
      proof
       reconsider C = (0).V as Element of S by Def3;
       take C;
       let A be Element of S;
         consider W being strict Submodule of V such that
A1:       W = A by Def3;
       thus C "/\" A = SubMeet(V).(C,A) by LATTICES:def 2
                  .= (0).V /\ W by A1,Def7
                  .= C by Th25;
       thus A "/\" C = SubMeet(V).(A,C) by LATTICES:def 2
                  .= W /\ (0).V by A1,Def7
                  .= C by Th25;
      end;
   hence thesis by Th63,LATTICES:def 13;
  end;

theorem Th65:
 for V being RightMod of R
  holds LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is 1_Lattice
   proof let V be RightMod of R;
    set S = LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #);
      ex C being Element of S st
     for A being Element of S holds C "\/" A = C & A "\/" C = C
      proof
       consider W' being strict Submodule of V such that
A1:  the carrier of W' = the carrier of (Omega).V;
        reconsider C = W' as Element of S by Def3;
       take C;
       let A be Element of S;
          consider W being strict Submodule of V such that
A2:       W = A by Def3;
A3:    C is Submodule of (Omega).V & the RightModStr of V = (Omega).V
      by Lm5,RMOD_2:def 4;
       thus C "\/" A = SubJoin(V).(C,A) by LATTICES:def 1
                  .= W' + W by A2,Def6
                  .= (Omega).V + W by A1,Lm4
                  .= the RightModStr of V by Th15
                  .= C by A1,A3,RMOD_2:39;
       thus A "\/" C = SubJoin(V).(A,C) by LATTICES:def 1
                  .= W + W' by A2,Def6
                  .= W + (Omega).V by A1,Lm4
                  .= the RightModStr of V by Th15
                  .= C by A1,A3,RMOD_2:39;
      end;
   hence thesis by Th63,LATTICES:def 14;
  end;

theorem
   for V being RightMod of R
  holds LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is 01_Lattice
   proof let V be RightMod of R;
      LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #)
     is lower-bounded upper-bounded Lattice by Th64,Th65;
   hence thesis;
  end;

theorem
   LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is M_Lattice
  proof set S = LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #);
      for A,B,C being Element of S st A [= C
     holds A "\/" (B "/\" C) = (A "\/" B) "/\" C
      proof let A,B,C be Element of S;
        assume A1: A [= C;
         consider W1 being strict Submodule of V such that
A2:       W1 = A by Def3;
         consider W2 being strict Submodule of V such that
A3:       W2 = B by Def3;
         consider W3 being strict Submodule of V such that
A4:       W3 = C by Def3;
         reconsider BC = W2 /\ W3 as Element of S by Def3;
         reconsider AB = W1 + W2 as Element of S by Def3;
            W1 + W3 = SubJoin(V).(A,C) by A2,A4,Def6
                      .= A "\/" C by LATTICES:def 1
                      .= W3 by A1,A4,LATTICES:def 3;
          then A5: W1 is Submodule of W3 by Th12;
       thus A "\/" (B "/\" C) = SubJoin(V).(A,B "/\" C) by LATTICES:def 1
                         .= SubJoin(V).(A,SubMeet(V).(B,C)) by LATTICES:def 2
                         .= SubJoin(V).(A,BC) by A3,A4,Def7
                         .= W1 + (W2 /\ W3) by A2,Def6
                         .= (W1 + W2) /\ W3 by A5,Th36
                         .= SubMeet(V).(AB,C) by A4,Def7
                         .= SubMeet(V).(SubJoin(V).(A,B),C) by A2,A3,Def6
                         .= SubMeet(V).(A "\/" B,C) by LATTICES:def 1
                         .= (A "\/" B) "/\" C by LATTICES:def 2;
      end;
   hence thesis by Th63,LATTICES:def 12;
  end;

Back to top