The abstract of the Mizar article:

Submodules and Cosets of Submodules in Right Module over Associative Ring

by

Michal Muzalewski, and

Wojciech Skaba

Received October 22, 1990

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 add of it = (the add 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;