:: $\mathbb Z$-modules
::  by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received September 5, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, ALGSTR_0, STRUCT_0, SUBSET_1, BINOP_1, FUNCT_1,
      ZFMISC_1, XBOOLE_0, RELAT_1, ARYTM_3, PARTFUN1, SUPINF_2, FUNCT_5,
      MCART_1, ARYTM_1, CARD_1, FINSEQ_1, CARD_3, TARSKI, XXREAL_0, RLVECT_1,
      REALSET1, RLSUB_1, ZMODUL01, INT_1, FINSEQ_4, LATTICES, EQREL_1, PBOOLE,
      RLSUB_2, RMOD_2, RMOD_3, BINOM, NAT_1, INT_3, VECTSP_1, MESFUNC1,
      BINOP_2, MOD_2, VECTSP_2, FUNCSDOM;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      PARTFUN1, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3, FUNCT_5, NUMBERS,
      XCMPLX_0, XXREAL_0, INT_1, NAT_1, REALSET1, FINSEQ_1, BINOP_2, XREAL_0,
      FINSEQ_4, STRUCT_0, ALGSTR_0, LATTICES, RLVECT_1, VECTSP_1, BINOM,
      GROUP_1, VECTSP_2, INT_3, VECTSP_4, VECTSP_5, MOD_2;
 constructors BINOP_1, NAT_1, FUNCT_3, FUNCT_5, REALSET1, RELSET_1, GROUP_1,
      LATTICES, RLSUB_1, ALGSTR_1, BINOM, FINSEQ_4, VECTSP_1, INT_3, VECTSP_2,
      VECTSP_4, BINOP_2, MOD_2, VECTSP_5, MEMBERED;
 registrations ORDINAL1, XREAL_0, NAT_1, STRUCT_0, ALGSTR_0, FINSEQ_1, CARD_1,
      SUBSET_1, INT_1, LATTICES, RELAT_1, ALGSTR_1, INT_3, VECTSP_1, VECTSP_5,
      MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: 1. Definition of Z-module

definition
::$CD 6
  mode Z_Module is LeftMod of INT.Ring;
end;

registration
  cluster TrivialLMod INT.Ring -> trivial non empty strict;
end;

registration
  cluster strict for Z_Module;
end;

definition
  let R be Ring;
  let V be LeftMod of R;
  mode VECTOR of V is Element of V;
end;

 reserve R for Ring;
 reserve x, y, y1 for set;
 reserve a, b for Element of R;
 reserve V for LeftMod of R;
 reserve v, w for Vector of V;

definition
  let R be Ring;
  let IT be LeftMod of R;
  attr IT is Mult-cancelable means
:: ZMODUL01:def 7
  for a being Element of R
  for v being Vector of IT st a * v = 0.IT holds
    a = 0.R or v = 0.IT;
end;

theorem :: ZMODUL01:1
  for V being Z_Module
  for a being Element of INT.Ring,
      v being Vector of V holds
    a = 0.INT.Ring or v = 0.V implies a * v = 0.V;

theorem :: ZMODUL01:2
  - v = (- 1.R) * v;

theorem :: ZMODUL01:3
  for V being Z_Module,
      v being Vector of V holds
  V is Mult-cancelable & v = - v implies v = 0.V;

theorem :: ZMODUL01:4
  for V being Z_Module,
      v being Vector of V holds
  V is Mult-cancelable & v + v = 0.V implies v = 0.V;

theorem :: ZMODUL01:5
  for V being Z_Module,
      a being Element of INT.Ring,
      v being Vector of V holds
  a * (- v) = (- a) * v;

theorem :: ZMODUL01:6
  for V being Z_Module,
      a being Element of INT.Ring,
      v being Vector of V holds
  a * (- v) = - (a * v);

theorem :: ZMODUL01:7
  for V being Z_Module,
      a being Element of INT.Ring,
      v being Vector of V holds
  (- a) * (- v) = a * v;

theorem :: ZMODUL01:8
  for V being Z_Module,
      a being Element of INT.Ring,
      v,w being Vector of V holds
  a * (v - w) = a * v - a * w;

theorem :: ZMODUL01:9
  for V being Z_Module,
      a,b being Element of INT.Ring,
      v being Vector of V holds
  (a - b) * v = a * v - b * v;

theorem :: ZMODUL01:10
  for V being Z_Module,
      a being Element of INT.Ring,
      v,w being Vector of V holds
  V is Mult-cancelable & a <> 0.INT.Ring & a * v = a * w implies v = w;

theorem :: ZMODUL01:11
  for V being Z_Module,
      a,b being Element of INT.Ring,
      v being Vector of V holds
  V is Mult-cancelable & v <> 0.V & a * v = b * v implies a = b;

 reserve u,v,w for Vector of V;
 reserve F,G,H,I for FinSequence of V;
 reserve j,k,n for Nat;
 reserve f,f9,g for sequence of V;

theorem :: ZMODUL01:12
  len F = len G & (for k,v st k in dom F & v = G.k holds F.k = a * v)
  implies Sum(F) = a * Sum(G);

theorem :: ZMODUL01:13
  for V being Z_Module, a being Element of INT.Ring holds
    a * Sum(<*>(the carrier of V)) = 0.V;

theorem :: ZMODUL01:14
  for R being Ring,
      V being LeftMod of R, a being Element of R,
      v, u being Vector of V holds
    a * Sum<* v,u *> = a * v + a * u;

theorem :: ZMODUL01:15
  for R being Ring
  for V being LeftMod of R, a being Element of R, v, u, w being Vector of V
  holds a * Sum<* v,u,w *> = a * v + a * u + a * w;

theorem :: ZMODUL01:16
  for V being LeftMod of INT.Ring, a being Element of INT.Ring,
      v being Vector of V holds
    (- a) * v = - a * v;

theorem :: ZMODUL01:17
  len F = len G & (for k st k in dom F holds G.k = a * F/.k )
  implies Sum(G) = a * Sum(F);

begin :: 2. Submodules and cosets of submodules in Z-module

 reserve R for Ring;
 reserve V, X, Y for LeftMod of R;
 reserve u, u1, u2, v, v1, v2 for Vector of V;
 reserve a for Element of R;
 reserve V1, V2, V3 for Subset of V;
 reserve x for set;

theorem :: ZMODUL01:18
  V1 <> {} & V1 is linearly-closed implies 0.V in V1;

theorem :: ZMODUL01:19
  V1 is linearly-closed implies for v st v in V1 holds - v in V1;

theorem :: ZMODUL01:20
  V1 is linearly-closed implies for v, u st v in V1 & u in V1 holds v - u in V1
;

theorem :: ZMODUL01:21
  the carrier of V = V1 implies V1 is linearly-closed;

theorem :: ZMODUL01:22
  V1 is linearly-closed & V2 is linearly-closed &
    V3 = {v + u : v in V1 & u in V2} implies
    V3 is linearly-closed;

registration let R; let V;
  cluster {0.V} -> linearly-closed for Subset of V;
end;

registration let R; let V;
  cluster linearly-closed for Subset of V;
end;

registration let R; let V;
  let V1,V2 be linearly-closed Subset of V;
  cluster V1 /\ V2 -> linearly-closed for Subset of V;
end;

definition
::$CD 2
end;

definition
  let R be Ring;
  let V be LeftMod of R;
  mode Submodule of V is Subspace of V;
end;

 reserve W, W1, W2 for Submodule of V;
 reserve w, w1, w2 for Vector of W;

theorem :: ZMODUL01:23
  x in W1 & W1 is Submodule of W2 implies x in W2;

theorem :: ZMODUL01:24
  for x being object holds x in W implies x in V;

theorem :: ZMODUL01:25
  w is Vector of V;

theorem :: ZMODUL01:26
  0.W = 0.V;

theorem :: ZMODUL01:27
  0.W1 = 0.W2;

theorem :: ZMODUL01:28
  w1 = v & w2 = u implies w1 + w2 = v + u;

theorem :: ZMODUL01:29
  w = v implies a * w = a * v;

theorem :: ZMODUL01:30
  w = v implies - v = - w;

theorem :: ZMODUL01:31
  w1 = v & w2 = u implies w1 - w2 = v - u;

theorem :: ZMODUL01:32
  V is Submodule of V;

theorem :: ZMODUL01:33
  0.V in W;

theorem :: ZMODUL01:34
  0.W1 in W2;

theorem :: ZMODUL01:35
  0.W in V;

theorem :: ZMODUL01:36
  u in W & v in W implies u + v in W;

theorem :: ZMODUL01:37
  v in W implies a * v in W;

theorem :: ZMODUL01:38
  v in W implies - v in W;

theorem :: ZMODUL01:39
  u in W & v in W implies u - v in W;

 reserve D for non empty set;
 reserve d1 for Element of D;
 reserve A for BinOp of D;
 reserve M for Function of [:the carrier of R,D:],D;

theorem :: ZMODUL01:40
  V1 = D & d1 = 0.V & A = (the addF of V) || V1 &
  M = (the lmult of V) | [:the carrier of R,V1:] implies
    ModuleStr (# D,A,d1,M #) is Submodule of V;

theorem :: ZMODUL01:41
  for R being Ring
  for V,X being strict LeftMod of R st V is Submodule of X &
    X is Submodule of V holds V = X;

theorem :: ZMODUL01:42
  V is Submodule of X & X is Submodule of Y implies V is Submodule of Y;

theorem :: ZMODUL01:43
  the carrier of W1 c= the carrier of W2 implies W1 is Submodule of W2;

theorem :: ZMODUL01:44
  (for v st v in W1 holds v in W2) implies W1 is Submodule of W2;

registration
  let R be Ring;
  let V be LeftMod of R;
  cluster strict for Submodule of V;
end;

theorem :: ZMODUL01:45
  for W1, W2 being strict Submodule of V holds
  the carrier of W1 = the carrier of W2 implies W1 = W2;

theorem :: ZMODUL01:46
  for W1, W2 being strict Submodule of V holds
  (for v holds v in W1 iff v in W2) implies W1 = W2;

theorem :: ZMODUL01:47
  for V being strict LeftMod of R, W being strict Submodule of V holds
  the carrier of W = the carrier of V implies W = V;

theorem :: ZMODUL01:48
  for V being strict LeftMod of R, W being strict Submodule of V holds
  (for v being Vector of V holds v in W iff v in V) implies W = V;

theorem :: ZMODUL01:49
  the carrier of W = V1 implies V1 is linearly-closed;

theorem :: ZMODUL01:50
  V1 <> {} & V1 is linearly-closed implies
  ex W being strict Submodule of V st V1 = the carrier of W;

theorem :: ZMODUL01:51
  (0).W = (0).V;

theorem :: ZMODUL01:52
  (0).W1 = (0).W2;

theorem :: ZMODUL01:53
  (0).W is Submodule of V;

theorem :: ZMODUL01:54
  (0).V is Submodule of W;

theorem :: ZMODUL01:55
  (0).W1 is Submodule of W2;

theorem :: ZMODUL01:56
  for V being LeftMod of R holds V is Submodule of (Omega).V;

definition
::$CD 4
end;

reserve B,C for Coset of W;

theorem :: ZMODUL01:57
  0.V in v + W iff v in W;

theorem :: ZMODUL01:58
  v in v + W;

theorem :: ZMODUL01:59
  0.V + W = the carrier of W;

theorem :: ZMODUL01:60
  v + (0).V = {v};

theorem :: ZMODUL01:61
  v + (Omega).V = the carrier of V;

theorem :: ZMODUL01:62
  0.V in v + W iff v + W = the carrier of W;

theorem :: ZMODUL01:63
  v in W iff v + W = the carrier of W;

theorem :: ZMODUL01:64
  v in W implies (a * v) + W = the carrier of W;

theorem :: ZMODUL01:65
  u in W iff v + W = (v + u) + W;

theorem :: ZMODUL01:66
  u in W iff v + W = (v - u) + W;

theorem :: ZMODUL01:67
  v in u + W iff u + W = v + W;

theorem :: ZMODUL01:68
  u in v1 + W & u in v2 + W implies v1 + W = v2 + W;

theorem :: ZMODUL01:69
  v in W implies a * v in v + W;

theorem :: ZMODUL01:70
  u + v in v + W iff u in W;

theorem :: ZMODUL01:71
  v - u in v + W iff u in W;

theorem :: ZMODUL01:72
  u in v + W iff ex v1 st v1 in W & u = v + v1;

theorem :: ZMODUL01:73
  u in v + W iff ex v1 st v1 in W & u = v - v1;

theorem :: ZMODUL01:74
  (ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W;

theorem :: ZMODUL01:75
  v + W = u + W implies ex v1 st v1 in W & v + v1 = u;

theorem :: ZMODUL01:76
  v + W = u + W implies ex v1 st v1 in W & v - v1 = u;

theorem :: ZMODUL01:77
  for W1, W2 being strict Submodule of V st v + W1 = v + W2 holds W1 = W2;

theorem :: ZMODUL01:78
  for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds W1 = W2;

theorem :: ZMODUL01:79
  C is linearly-closed iff C = the carrier of W;

theorem :: ZMODUL01:80
  for W1, W2 being strict Submodule of V, C1 being Coset of W1,
  C2 being Coset of W2 st C1 = C2 holds W1 = W2;

theorem :: ZMODUL01:81
  {v} is Coset of (0).V;

theorem :: ZMODUL01:82
  V1 is Coset of (0).V implies ex v st V1 = {v};

theorem :: ZMODUL01:83
  the carrier of W is Coset of W;

theorem :: ZMODUL01:84
  the carrier of V is Coset of (Omega).V;

theorem :: ZMODUL01:85
  V1 is Coset of (Omega).V implies V1 = the carrier of V;

theorem :: ZMODUL01:86
  0.V in C iff C = the carrier of W;

theorem :: ZMODUL01:87
  u in C iff C = u + W;

theorem :: ZMODUL01:88
  u in C & v in C implies ex v1 st v1 in W & u + v1 = v;

theorem :: ZMODUL01:89
  u in C & v in C implies ex v1 st v1 in W & u - v1 = v;

theorem :: ZMODUL01:90
  (ex C st v1 in C & v2 in C) iff v1 - v2 in W;

theorem :: ZMODUL01:91
  u in B & u in C implies B = C;

begin :: 3. Operations on submodules in Z-module

 reserve V for LeftMod of R;
 reserve W, W1, W2, W3 for Submodule of V;
 reserve u, u1, u2, v, v1, v2 for Vector of V;
 reserve a, a1, a2 for Element of R;
 reserve X, Y, y, y1, y2 for set;

definition let GF be Ring;
  let M be Abelian add-associative right_zeroed right_complementable
  vector-distributive scalar-distributive scalar-associative scalar-unital
   non empty ModuleStr over GF;
  let W1, W2 be Subspace of M;
  redefine func W1 + W2;
  commutativity;
end;

theorem :: ZMODUL01:92
  x in W1 + W2 iff ex v1, v2 st v1 in W1 & v2 in W2 & x = v1 + v2;

theorem :: ZMODUL01:93
  v in W1 or v in W2 implies v in W1 + W2;

theorem :: ZMODUL01:94
  for x being object holds x in W1 /\ W2 iff x in W1 & x in W2;

theorem :: ZMODUL01:95
  for W being strict Submodule of V holds W + W = W;

theorem :: ZMODUL01:96
  W1 + (W2 + W3) = (W1 + W2) + W3;

theorem :: ZMODUL01:97
  W1 is Submodule of W1 + W2;

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

theorem :: ZMODUL01:99
  for W being strict Submodule of V holds (0).V + W = W;

theorem :: ZMODUL01:100
  (0).V + (Omega).V = the ModuleStr of V;

theorem :: ZMODUL01:101
  (Omega).V + W = the ModuleStr of V;

theorem :: ZMODUL01:102
  for V being strict LeftMod of R holds (Omega).V + (Omega).V = V;

theorem :: ZMODUL01:103
  for W being strict Submodule of V holds W /\ W = W;

theorem :: ZMODUL01:104
  W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3;

theorem :: ZMODUL01:105
  W1 /\ W2 is Submodule of W1;

theorem :: ZMODUL01:106
  for W1 being strict Submodule of V holds W1 is Submodule of W2 iff
  W1 /\ W2 = W1;

theorem :: ZMODUL01:107
  (0).V /\ W = (0).V;

theorem :: ZMODUL01:108
  (0).V /\ (Omega).V = (0).V;

theorem :: ZMODUL01:109
  for W being strict Submodule of V holds (Omega).V /\ W = W;

theorem :: ZMODUL01:110
  for V being strict LeftMod of R holds (Omega).V /\ (Omega).V = V;

theorem :: ZMODUL01:111
  W1 /\ W2 is Submodule of W1 + W2;

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

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

theorem :: ZMODUL01:114
  (W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3);

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

theorem :: ZMODUL01:116
  W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3);

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

theorem :: ZMODUL01:118
  W1 is strict Submodule of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3;

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

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

theorem :: ZMODUL01:121
  (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;

notation let GF be Ring;
  let V be Abelian add-associative right_zeroed right_complementable
     vector-distributive scalar-distributive scalar-associative
     scalar-unital non empty ModuleStr over GF;
  synonym Submodules V for Subspaces(V);
end;

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

theorem :: ZMODUL01:122
  for V being strict LeftMod of R holds V in Submodules(V);

definition
::$CD 3
  let R;
  let V be LeftMod of R;
  let W be Submodule of V;
  attr W is with_Linear_Compl means
:: ZMODUL01:def 17
  ex C being Submodule of V st V is_the_direct_sum_of C,W;
end;

registration
  let R;
  let V be LeftMod of R;
  cluster with_Linear_Compl for Submodule of V;
end;

definition
  let R;
  let V be LeftMod of R;
  let W be Submodule of V;
  assume  W is with_Linear_Compl;
  mode Linear_Compl of W -> Submodule of V means
:: ZMODUL01:def 18
  V is_the_direct_sum_of it,W;
end;

theorem :: ZMODUL01:123
  for W1, W2 being Submodule of V holds V
  is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1;

theorem :: ZMODUL01:124
  for W being with_Linear_Compl Submodule of V,
  L being Linear_Compl of W holds
  V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L;

theorem :: ZMODUL01:125
  for W being with_Linear_Compl Submodule of V, L being
  Linear_Compl of W holds W + L = the ModuleStr of V;

theorem :: ZMODUL01:126
  for W being with_Linear_Compl Submodule of V,
  L being Linear_Compl of W holds W /\ L = (0).V;

theorem :: ZMODUL01:127
  V is_the_direct_sum_of W1,W2
  implies V is_the_direct_sum_of W2,W1;

theorem :: ZMODUL01:128
  for V being Z_Module, W being with_Linear_Compl Submodule of V,
  L being Linear_Compl of W holds W is Linear_Compl of L;

theorem :: ZMODUL01:129
  for V being Z_Module holds V is_the_direct_sum_of (0).V, (Omega).V &
    V is_the_direct_sum_of (Omega).V,(0).V;

theorem :: ZMODUL01:130
  for V being Z_Module holds (0).V is Linear_Compl of (Omega).V &
  (Omega).V is Linear_Compl of (0).V;

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

theorem :: ZMODUL01:131
  C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2;

theorem :: ZMODUL01:132
  for V being Z_Module, 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 :: ZMODUL01:133
  for V being LeftMod of R, W1,W2 being Submodule of V holds
  W1 + W2 = the ModuleStr 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;

theorem :: ZMODUL01:134
  V is_the_direct_sum_of W1,W2 & v1 + v2 = u1 + u2 & v1 in
  W1 & u1 in W1 & v2 in W2 & u2 in W2 implies v1 = u1 & v2 = u2;

theorem :: ZMODUL01:135
  V = W1 + W2 & (ex v st for v1,v2,u1,u2 st v1 + v2 = 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
::$CD
end;

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

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

theorem :: ZMODUL01:138
  for V being Z_Module, W being with_Linear_Compl Submodule of V,
  L being Linear_Compl of W, v being Vector of V,
  t being Element of [:the carrier of V, the carrier of V:]
  holds t`1 + t`2 = v & t`1 in W & t`2 in L implies t = v |-- (W,L);

theorem :: ZMODUL01:139
  for V being Z_Module, W being with_Linear_Compl Submodule of V,
  L being Linear_Compl of W, v being Vector of V holds
  (v |-- (W,L))`1 + (v |-- (W,L))`2 = v;

theorem :: ZMODUL01:140
  for V being Z_Module, W being with_Linear_Compl Submodule of V,
  L being Linear_Compl of W, v being Vector of V holds
  (v |-- (W,L))`1 in W & (v |-- (W,L))`2 in L;

theorem :: ZMODUL01:141
  for V being Z_Module, W being with_Linear_Compl Submodule of V,
  L being Linear_Compl of W, v being Vector of V holds
  (v |-- (W,L))`1 = (v |-- (L,W))`2;

theorem :: ZMODUL01:142
  for V being Z_Module, W being with_Linear_Compl Submodule of V,
  L being Linear_Compl of W, v being Vector of V holds
  (v |-- (W,L))`2 = (v |-- (L,W))`1;

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

theorem :: ZMODUL01:143
  LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is Lattice;

registration let R; let V;
  cluster LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #)
  -> Lattice-like;
end;

theorem :: ZMODUL01:144
  for V being Z_Module holds LattStr (# Submodules(V),
  SubJoin(V), SubMeet(V) #) is lower-bounded;

theorem :: ZMODUL01:145
  for V being Z_Module holds LattStr (# Submodules(V),
  SubJoin(V), SubMeet(V) #) is upper-bounded;

theorem :: ZMODUL01:146
  for V being Z_Module holds LattStr (# Submodules(V),
  SubJoin(V), SubMeet(V) #) is 01_Lattice;

theorem :: ZMODUL01:147
  for V being Z_Module holds LattStr (# Submodules(V),
  SubJoin(V), SubMeet(V) #) is modular;

theorem :: ZMODUL01:148
  for V being Z_Module, W1,W2,W3 being strict Submodule of V holds
  W1 is Submodule of W2 implies W1 /\ W3 is Submodule of W2 /\ W3;

theorem :: ZMODUL01:149
  for V being Z_Module, W being strict Submodule of V holds
  (for v being Vector of V holds v in W) implies
  W = the ModuleStr of V;

theorem :: ZMODUL01:150
  ex C st v in C;

begin :: 4.Transformation of Abelian group to Z-module

definition
  let AG be non empty addLoopStr;
  func Int-mult-left(AG) -> Function of
  [:the carrier of INT.Ring,
    the carrier of AG:], the carrier of AG means
:: ZMODUL01:def 20
  for i being Element of INT.Ring, a being Element of AG holds
  (i >= 0 implies it.(i,a) = (Nat-mult-left(AG)).(i,a)) &
  (i < 0 implies it.(i,a) = (Nat-mult-left(AG)).(-i,-a));
end;

theorem :: ZMODUL01:151
  for R being non empty addLoopStr, a being Element of R,
     i be Element of INT.Ring, i1 be Element of NAT st i=i1 holds
  (Int-mult-left(R)).(i,a) = i1 * a;

theorem :: ZMODUL01:152
  for R being non empty addLoopStr, a being Element of R,
  i be Integer st i=0 holds
  (Int-mult-left(R)).(i,a) = 0.R;

theorem :: ZMODUL01:153
  for R being add-associative right_zeroed right_complementable
  non empty addLoopStr,
  i be Element of NAT holds
  (Nat-mult-left(R)).(i,0.R) = 0.R;

theorem :: ZMODUL01:154
  for R being add-associative right_zeroed right_complementable
  non empty addLoopStr,
  i be Element of INT.Ring holds
  (Int-mult-left(R)).(i,0.R) = 0.R;

theorem :: ZMODUL01:155
  for R being right_zeroed non empty addLoopStr, a being Element of R,
  i be Integer st i = 1
  holds (Int-mult-left(R)).(i,a) = a;

theorem :: ZMODUL01:156
  for R being Abelian right_zeroed add-associative right_complementable
    non empty addLoopStr,
  a being Element of R, i, j, k being Element of NAT
  st i <= j & k = j-i holds
  (Nat-mult-left(R)).(k,a)
  = (Nat-mult-left(R)).(j,a) - (Nat-mult-left(R)).(i,a);

theorem :: ZMODUL01:157
  for R being Abelian right_zeroed add-associative right_complementable
  non empty addLoopStr,
  a being Element of R, i being Element of NAT
  holds -(Nat-mult-left(R)).(i,a) = (Nat-mult-left(R)).(i,-a);

theorem :: ZMODUL01:158
  for R being Abelian right_zeroed add-associative right_complementable
         non empty addLoopStr,
  a being Element of R, i, j being Element of INT.Ring
  st i in NAT & not j in NAT
  holds (Int-mult-left(R)).(i+j,a)
  = (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a);

theorem :: ZMODUL01:159
  for R being Abelian right_zeroed add-associative
    right_complementable non empty addLoopStr,
  a being Element of R, i, j being Element of INT.Ring
  holds (Int-mult-left(R)).(i+j,a)
  = (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a);

theorem :: ZMODUL01:160
  for R being Abelian right_zeroed add-associative
  right_complementable non empty addLoopStr,
  a, b being Element of R, i being Element of NAT
  holds (Nat-mult-left(R)).(i,a+b)
  = (Nat-mult-left(R)).(i,a) + (Nat-mult-left(R)).(i,b);

theorem :: ZMODUL01:161
  for R being Abelian right_zeroed add-associative
        right_complementable non empty addLoopStr,
      a, b being Element of R, i being Element of INT.Ring
  holds (Int-mult-left(R)).(i,a+b)
  = (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(i,b);

theorem :: ZMODUL01:162
  for R being Abelian right_zeroed add-associative
  right_complementable non empty addLoopStr,
  a being Element of R, i, j being Element of NAT holds
  (Nat-mult-left(R)).(i*j,a) = (Nat-mult-left(R)).(i,(Nat-mult-left(R)).(j,a));

theorem :: ZMODUL01:163
  for R being Abelian right_zeroed add-associative right_complementable
    non empty addLoopStr,
  a being Element of R, i, j being Element of INT.Ring holds
  (Int-mult-left(R)).(i*j,a) = (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a));

theorem :: ZMODUL01:164
  for AG be non empty Abelian add-associative right_zeroed
    right_complementable addLoopStr holds
  ModuleStr (# the carrier of AG, the addF of AG, the ZeroF of AG,
  Int-mult-left(AG) #) is Z_Module;