The abstract of the Mizar article:

Submodules

by

Michal Muzalewski

Received June 19, 1992

MML identifier: LMOD_6

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCSDOM, VECTSP_1, VECTSP_2, RLVECT_2, RLSUB_2, RMOD_3, FUNCT_1,
      RLSUB_1, RELAT_1, RLVECT_1, REALSET1, QC_LANG1, SUBSET_1, RLVECT_3,
      BOOLE, PARTFUN1, ARYTM_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, BINOP_1, REALSET1,
      RLVECT_1, STRUCT_0, VECTSP_1, FUNCSDOM, VECTSP_2, VECTSP_4, VECTSP_5,
      VECTSP_6, MOD_3, PRE_TOPC;
 constructors BINOP_1, DOMAIN_1, REALSET1, VECTSP_5, VECTSP_6, MOD_3, PRE_TOPC,
      VECTSP_2, MEMBERED, XBOOLE_0;
 clusters VECTSP_1, VECTSP_2, VECTSP_4, STRUCT_0, RELSET_1, MEMBERED, ZFMISC_1,
      XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

 reserve x for set,
         K for Ring,
         r for Scalar of K,
         V, M, M1, M2, N for LeftMod of K,
         a for Vector of V,
         m, m1, m2 for Vector of M,
         n, n1, n2 for Vector of N,
         A for Subset of V,
         l for Linear_Combination of A,
         W, W1, W2, W3 for Subspace of V;

 definition let K, V;
  redefine func Subspaces(V);
  synonym Submodules(V);
 end;

theorem :: LMOD_6:1
  M1 = the VectSpStr of M2 implies (x in M1 iff x in M2);

theorem :: LMOD_6:2
  for v being Vector of the VectSpStr of V st a=v holds r*a = r*v;

theorem :: LMOD_6:3
 the VectSpStr of V is strict Subspace of V;

theorem :: LMOD_6:4
 V is Subspace of (Omega).V;

begin

definition let K;
redefine canceled;

attr K is trivial means
:: LMOD_6:def 2

 0.K = 1_ K;
end;

theorem :: LMOD_6:5
 K is trivial implies (for r holds r = 0.K) & (for a holds a = 0.V);

theorem :: LMOD_6:6
   K is trivial implies V is trivial;

theorem :: LMOD_6:7
   V is trivial iff the VectSpStr of V = (0).V;

begin             ::
                  ::   1. Submodules and subsets
                  ::

definition let K,V; let W be strict Subspace of V;
 func @W -> Element of Submodules(V) equals
:: LMOD_6:def 3
W;
end;

canceled;

theorem :: LMOD_6:9
 for A being Subset of W holds A is Subset of V;

definition let K,V,W; let A be Subset of W;
 canceled;

 func @A -> Subset of V equals
:: LMOD_6:def 5
   A;
end;

definition let K,V,W; let A be non empty Subset of W;
 cluster @A -> non empty;
end;

theorem :: LMOD_6:10
 x in [#]V iff x in V;

theorem :: LMOD_6:11
   x in @[#]W iff x in W;

theorem :: LMOD_6:12
 A c= [#]Lin(A);

theorem :: LMOD_6:13
 A<>{} & A is lineary-closed implies Sum(l) in A;

canceled;

theorem :: LMOD_6:15
   0.V in A & A is lineary-closed implies A = [#]Lin(A);


begin             ::
                  ::   2. Cyclic submodule
                  ::

definition let K,V,a;
 redefine func {a} -> Subset of V;
end;

definition let K,V,a;
  func <:a:> -> strict Subspace of V equals
:: LMOD_6:def 6
Lin({a});
end;

begin              ::
                   ::  3. Inclusion of left R-modules
                   ::

definition let K,M,N;
  pred M c= N means
:: LMOD_6:def 7
 M is Subspace of N;
  reflexivity;
end;

theorem :: LMOD_6:16
M c= N implies
  (x in M implies x in N) & (x is Vector of M implies x is Vector of N);

theorem :: LMOD_6:17
  M c= N implies
   0.M = 0.N
 & (m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2)
 & (m = n implies r * m = r * n)
 & (m = n implies - n = - m)
 & (m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2)
 & 0.N in M
 & 0.M in N
 & (n1 in M & n2 in M implies n1 + n2 in M)
 & (n in M implies r * n in M)
 & (n in M implies - n in M)
 & (n1 in M & n2 in M implies n1 - n2 in M);

theorem :: LMOD_6:18
   M1 c= N & M2 c= N implies
    0.M1 = 0.M2
  & 0.M1 in M2
  & (the carrier of M1 c= the carrier of M2
   implies M1 c= M2)
  & ((for n st n in M1 holds n in M2) implies M1 c= M2)
  & (the carrier of M1 = the carrier of M2
    & M1 is strict & M2 is strict implies M1 = M2)
  & (0).M1 c= M2;

canceled 2;

theorem :: LMOD_6:21
  for V,M being strict LeftMod of K
  holds V c= M & M c= V implies V = M;

theorem :: LMOD_6:22
   V c= M & M c= N implies V c= N;

theorem :: LMOD_6:23
   M c= N implies (0).M c= N;

theorem :: LMOD_6:24
   M c= N implies (0).N c= M;

theorem :: LMOD_6:25
   M c= N implies M c= (Omega).N;

theorem :: LMOD_6:26
   W1 c= W1 + W2 & W2 c= W1 + W2;

theorem :: LMOD_6:27
   W1 /\ W2 c= W1 & W1 /\ W2 c= W2;

theorem :: LMOD_6:28
   W1 c= W2 implies W1 /\ W3 c= W2 /\ W3;

theorem :: LMOD_6:29
   W1 c= W3 implies W1 /\ W2 c= W3;

theorem :: LMOD_6:30
   W1 c= W2 & W1 c= W3 implies W1 c= W2 /\ W3;

theorem :: LMOD_6:31
   W1 /\ W2 c= W1 + W2;

theorem :: LMOD_6:32
   (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3);

theorem :: LMOD_6:33
   W1 c= W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3);

theorem :: LMOD_6:34
   W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3);

theorem :: LMOD_6:35
   W1 c= W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3);

theorem :: LMOD_6:36
   W1 c= W2 implies W1 c= W2 + W3;

theorem :: LMOD_6:37
   W1 c= W3 & W2 c= W3 implies W1 + W2 c= W3;

theorem :: LMOD_6:38
   for A,B being Subset of V st A c= B holds Lin(A) c= Lin(B);

theorem :: LMOD_6:39
   for A,B being Subset of V holds Lin(A /\ B) c= Lin(A) /\ Lin(B);

theorem :: LMOD_6:40
 M1 c= M2 implies [#]M1 c= [#]M2;

theorem :: LMOD_6:41
 W1 c= W2 iff for a st a in W1 holds a in W2;

theorem :: LMOD_6:42
 W1 c= W2 iff [#]W1 c= [#]W2;

theorem :: LMOD_6:43
   W1 c= W2 iff @[#]W1 c= @[#]W2;

theorem :: LMOD_6:44
   (0).W c= V & (0).V c= W & (0).W1 c= W2;