:: Submodule of free $\mathbb Z$-module
::  by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 31, 2013
:: Copyright (c) 2013-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 GAUSSINT, NUMBERS, FINSEQ_1, SUBSET_1, RLVECT_1, STRUCT_0,
      FUNCT_1, RAT_1, XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, RLSUB_2,
      EQREL_1, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1, NAT_1,
      FUNCT_2, FINSET_1, VALUED_1, RLSUB_1, BINOP_1, ZFMISC_1, INT_1, ORDINAL1,
      RLVECT_2, ZMODUL01, ZMODUL03, RLVECT_3, RMOD_2, RANKNULL, MSAFREE2,
      VECTSP_1, MESFUNC1, REALSET1, MONOID_0, VECTSP10, EC_PF_1, MOD_3,
      ZMODUL02, RLVECT_5, ORDINAL2, ZMODUL04, INT_2, INT_3, FUNCSDOM, VECTSP_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, ORDINAL2, FINSET_1,
      ORDERS_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, INT_2,
      RAT_1, REALSET1, FINSEQ_1, EQREL_1, STRUCT_0, ALGSTR_0, GROUP_1,
      RLVECT_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7,
      VECTSP_9, MATRLIN, INT_3, EC_PF_1, ZMODUL01, ZMODUL02, ZMODUL03,
      GAUSSINT, VECTSP10;
 constructors BINOP_2, RELSET_1, ORDERS_1, REALSET1, GR_CY_1, VECTSP_6,
      GROUP_1, REAL_1, RLVECT_2, VECTSP_2, VECTSP_9, VECTSP10, ALGSTR_1,
      ZMODUL02, ORDINAL3, ZMODUL03, GAUSSINT, VECTSP_4, VECTSP_7, ZMODUL01,
      VECTSP_5, INT_3, VFUNCT_1;
 registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
      XREAL_0, STRUCT_0, RLVECT_1, MEMBERED, FINSEQ_1, CARD_1, INT_1, XBOOLE_0,
      ORDINAL1, XXREAL_0, NAT_1, INT_3, RELAT_1, ZMODUL02, GAUSSINT, EQREL_1,
      RAT_1, XCMPLX_0, ZMODUL03, ZMODUL01, VECTSP_7;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: 1. Vector space of rational field generated by a free Z-module

reserve V for Z_Module;
reserve W, W1, W2 for Submodule of V;

theorem :: ZMODUL04:1
  for R being Ring
  for V being LeftMod of R, W1, W2 being Subspace of V,
  WW1, WW2 being Subspace of W1 + W2
  st WW1 = W1 & WW2 = W2 holds
  W1 + W2 = WW1 + WW2;

theorem :: ZMODUL04:2
  for R being Ring
  for V being LeftMod of R, W1, W2 being Subspace of V,
  WW1, WW2 being Subspace of W1 + W2
  st WW1 = W1 & WW2 = W2 holds
  W1 /\ W2 = WW1 /\ WW2;

registration ::: generalize for arbitrary products
  let V be Z_Module;
  cluster [:the carrier of V,INT \ {0}:] -> non empty;
end;

definition
  let V be Z_Module;
  assume  V is Mult-cancelable;
  func EQRZM(V) -> Equivalence_Relation of [:the carrier of V,INT \{0}:]
  means
:: ZMODUL04:def 1
  for S,T being object holds
  [S,T] in it
  iff ( S in [:the carrier of V,INT \{0}:]
  & T in [:the carrier of V,INT \{0}:]
  & ex z1,z2 be Element of V,i1,i2 be Element of INT.Ring
  st S=[z1,i1] & T=[z2,i2] & i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2);
end;

theorem :: ZMODUL04:3
  for V be Z_Module,
  z1, z2 be Element of V, i1, i2 be Element of INT.Ring
  st V is Mult-cancelable holds
  [[z1,i1],[z2,i2]] in EQRZM(V) iff
  i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2;

definition
  let V be Z_Module;
  assume  V is Mult-cancelable;
  func addCoset(V) -> BinOp of Class EQRZM(V) means
:: ZMODUL04:def 2
  for A, B be object st A in Class EQRZM(V) & B in Class EQRZM(V) holds
  for z1,z2 be Element of V,i1,i2 be Element of INT.Ring
  st i1 <> 0.INT.Ring & i2 <> 0.INT.Ring
  & A=Class(EQRZM(V),[z1,i1]) & B=Class(EQRZM(V),[z2,i2]) holds
  it.(A,B) = Class(EQRZM(V),[i2*z1+i1*z2,i1*i2]);
end;

definition
  let V be Z_Module;
  assume  V is Mult-cancelable;
  func zeroCoset(V) -> Element of Class EQRZM(V) means
:: ZMODUL04:def 3
  for i be Integer st i <> 0 holds it = Class(EQRZM(V),[0.V,i]);
end;

definition
  let V be Z_Module;
  assume  V is Mult-cancelable;
  func lmultCoset(V) -> Function of
  [:the carrier of F_Rat, Class EQRZM(V):], Class EQRZM(V) means
:: ZMODUL04:def 4

  for q be object, A be object st q in RAT & A in Class EQRZM(V) holds
  for m,n,i be Integer, mm being Element of INT.Ring, z be Element of V
  st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class(EQRZM(V),[z,i])
  holds it.(q,A) = Class(EQRZM(V),[mm*z,n*i]);
end;

theorem :: ZMODUL04:4
  for V be Z_Module,
  z be Element of V,
  i, n be Element of INT.Ring
  st i <> 0.INT.Ring & n <> 0.INT.Ring & V is Mult-cancelable holds
  Class(EQRZM(V),[z,i]) = Class(EQRZM(V),[n*z,n*i]);

theorem :: ZMODUL04:5
  for V be Z_Module,
  v be Element of
  ModuleStr (# Class EQRZM(V), addCoset(V), zeroCoset(V), lmultCoset(V) #)
  st V is Mult-cancelable holds
  ex i be Element of INT.Ring, z be Element of V
  st i <> 0.INT.Ring & v = Class(EQRZM(V),[z,i]);

definition
  let V be Z_Module;
  assume  V is Mult-cancelable;
  func Z_MQ_VectSp(V) -> VectSp of F_Rat equals
:: ZMODUL04:def 5
  ModuleStr (# Class EQRZM(V), addCoset(V), zeroCoset(V), lmultCoset(V) #);
end;

definition
  let V be Z_Module;
  assume  V is Mult-cancelable;
  func MorphsZQ(V) -> Function of V, Z_MQ_VectSp(V) means
:: ZMODUL04:def 6

  it is one-to-one
  & (for v be Element of V holds it.v = Class(EQRZM(V),[v,1]) )
  & (for v,w be Element of V holds it.(v+w) = it.v + it.w)
  & (for v be Element of V, i be Element of INT.Ring, q be Element of F_Rat
  st i = q holds it.(i*v) = q*(it.v) )
  & it.(0.V) = 0.(Z_MQ_VectSp(V));
end;

theorem :: ZMODUL04:6
  for V be Z_Module st V is Mult-cancelable holds
  for s be FinSequence of V,
  t be FinSequence of Z_MQ_VectSp(V)
  st len s = len t & for i be Element of NAT
  st i in dom s holds ex si be Vector of V
  st si = s.i & t.i = (MorphsZQ(V)).si holds
  Sum(t) = (MorphsZQ(V)).Sum(s);

theorem :: ZMODUL04:7
  for V be Z_Module,
  I being Subset of V,
  IQ being Subset of Z_MQ_VectSp(V),
  l be Linear_Combination of I,
  lq being Linear_Combination of IQ
  st V is Mult-cancelable
  & IQ =(MorphsZQ(V)).:I
  & l = lq*MorphsZQ(V) holds
  Sum(lq) = (MorphsZQ(V)).(Sum(l));

theorem :: ZMODUL04:8
  for V be Z_Module, IQ being Subset of Z_MQ_VectSp(V) holds
  for lq being Linear_Combination of IQ holds
  ex m be Integer, a be Element of F_Rat
  st m <> 0 & m = a & rng (a * lq) c= INT;

theorem :: ZMODUL04:9
  for V be Z_Module,
  I being Subset of V,
  IQ being Subset of Z_MQ_VectSp(V),
  lq being Linear_Combination of IQ
  st V is Mult-cancelable & IQ =(MorphsZQ(V)).:(I) holds
  ex m be Element of INT.Ring, a be Element of F_Rat,
  l be Linear_Combination of I
  st m <> 0.INT.Ring & m = a & l = (a * lq) * (MorphsZQ(V))
  & (MorphsZQ(V))"Carrier(lq) = Carrier(l);

theorem :: ZMODUL04:10
  for V be Z_Module,
  I being Subset of V,
  IQ being Subset of Z_MQ_VectSp(V),
  lq being Linear_Combination of IQ,
  m be Integer, a be Element of F_Rat,
  l be Linear_Combination of I
  st V is Mult-cancelable & IQ =(MorphsZQ(V)).:(I)
  & m <> 0 & m = a
  & l = (a * lq) *(MorphsZQ(V))
  holds a*(Sum(lq)) = (MorphsZQ(V)).(Sum(l));

theorem :: ZMODUL04:11
  for V be Z_Module,
  I being Subset of V,
  IQ being Subset of Z_MQ_VectSp(V)
  st V is Mult-cancelable & IQ =(MorphsZQ(V)).:(I)
  & I is linearly-independent
  holds IQ is linearly-independent;

theorem :: ZMODUL04:12
  for V be Z_Module,
  I being Subset of V,
  l being Linear_Combination of I,
  IQ being Subset of Z_MQ_VectSp(V)
  st V is Mult-cancelable & IQ =(MorphsZQ(V)).:I holds
  ex lq be Linear_Combination of IQ
  st l = lq*(MorphsZQ(V)) &
  Carrier(lq) = (MorphsZQ(V)).:(Carrier(l));

theorem :: ZMODUL04:13
  for V be free Z_Module,
  I being Subset of V,
  IQ being Subset of Z_MQ_VectSp(V),
  l be Linear_Combination of I,
  i be Element of INT.Ring
  st i <> 0.INT.Ring & IQ =(MorphsZQ(V)).:I
  holds Class(EQRZM(V),[Sum(l),i]) in Lin(IQ);

theorem :: ZMODUL04:14
  for V be free Z_Module,
  I being Subset of V,
  IQ being Subset of Z_MQ_VectSp(V)
  st IQ =(MorphsZQ(V)).:I
  holds card(I) = card(IQ);

theorem :: ZMODUL04:15
  for V be free Z_Module,
  I being Subset of V,
  IQ being Subset of Z_MQ_VectSp(V)
  st IQ =(MorphsZQ(V)).:I & I is Basis of V
  holds IQ is Basis of Z_MQ_VectSp(V);

registration
  let V be finite-rank free Z_Module;
  cluster Z_MQ_VectSp(V) -> finite-dimensional;
end;

theorem :: ZMODUL04:16
  for V be finite-rank free Z_Module holds
  rank V = dim Z_MQ_VectSp(V);

theorem :: ZMODUL04:17
  for V be free Z_Module, I, A be finite Subset of V
  st I is Basis of V & card (I) + 1 = card (A)
  holds A is linearly-dependent;

theorem :: ZMODUL04:18
  for V be free Z_Module, A, B be Subset of V
  st A is linearly-dependent & A c= B
  holds B is linearly-dependent;

theorem :: ZMODUL04:19
  for V be free Z_Module,D,A be Subset of V
  st D is Basis of V & D is finite & card (D) c< card(A)
  holds A is linearly-dependent;

theorem :: ZMODUL04:20
  for V be free Z_Module, I, A be Subset of V
  st I is Basis of V & I is finite & A is linearly-independent
  holds card (A) c= card (I);

begin :: 2. Subspace of free $\mathbb Z$-module

theorem :: ZMODUL04:21
  for V being Z_Module st (Omega).V is free holds V is free;

theorem :: ZMODUL04:22
  for R being Ring
  for V being LeftMod of R, W1, W2 being Subspace of V,
  W1s, W2s being strict Subspace of V st W1s = (Omega).W1 & W2s = (Omega).W2
  holds W1s + W2s = W1 + W2;

theorem :: ZMODUL04:23
  for R being Ring
  for V being LeftMod of R, W1, W2 being Subspace of V,
  W1s, W2s being strict Subspace of V st W1s = (Omega).W1 & W2s = (Omega).W2
  holds W1s /\ W2s = W1 /\ W2;

theorem :: ZMODUL04:24
  for R being Ring
  for V be LeftMod of R, W be strict Subspace of V st W <> (0).V holds
  ex v be Vector of V st v in W & v <> 0.V;

theorem :: ZMODUL04:25
  for K being Ring
  for V being VectSp of K
  for A being Subset of V, l1, l2 being Linear_Combination of A
  st Carrier(l1) /\ Carrier(l2) = {} holds
  Carrier(l1 + l2) = Carrier(l1) \/ Carrier(l2);

theorem :: ZMODUL04:26
  for R being Ring
  for V being VectSp of R
  for A1, A2 being Subset of V, l being Linear_Combination of A1 \/ A2
  st A1 /\ A2 = {} holds
  ex l1 being Linear_Combination of A1, l2 being Linear_Combination of A2
  st l = l1 + l2;

theorem :: ZMODUL04:27
  for V being Z_Module, W1, W2 being free Subspace of V,
  I1 being Basis of W1, I2 being Basis of W2 st V is_the_direct_sum_of W1,W2
  holds I1 /\ I2 = {};

theorem :: ZMODUL04:28
  for V being Z_Module, W1, W2 being free Subspace of V,
  I1 being Basis of W1, I2 being Basis of W2, I being Subset of V
  st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2
  holds Lin(I) = the ModuleStr of V;

theorem :: ZMODUL04:29
  for V being LeftMod of INT.Ring, W1, W2 being free Subspace of V,
  I1 being Basis of W1, I2 being Basis of W2, I being Subset of V
  st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2
  holds I is linearly-independent;

theorem :: ZMODUL04:30
  for V being Z_Module, W1, W2 being free Subspace of V
  st V is_the_direct_sum_of W1,W2
  holds V is free;

theorem :: ZMODUL04:31
  for V being Z_Module, W1, W2 being free Subspace of V
  st W1 /\ W2 = (0).V holds
  W1 + W2 is free;

theorem :: ZMODUL04:32
  for V being free Z_Module, I being Basis of V, v being Vector of V
  st v in I holds
  Lin(I \ {v}) is free & Lin{v} is free;

theorem :: ZMODUL04:33
  for V being free Z_Module, I being Basis of V, v being Vector of V
  st v in I holds
  V is_the_direct_sum_of Lin(I \ {v}),Lin{v};

registration
  let V be finite-rank free Z_Module;
  cluster -> free for Subspace of V;
end;

theorem :: ZMODUL04:34
  for V being Z_Module, W being Subspace of V,
      W1, W2 being free Subspace of V st
  W1 /\ W2 = (0).V & the ModuleStr of W = W1 + W2
  holds W is free;

theorem :: ZMODUL04:35
  for p being prime Element of INT.Ring, V being free Z_Module
  st Z_MQ_VectSp(V,p) is finite-dimensional
  holds V is finite-rank;

theorem :: ZMODUL04:36
  for p being prime Element of INT.Ring, V being Z_Module,
  s be Element of V, a be Element of INT.Ring, b be Element of GF(p)
  st b = a mod p holds
  b*ZMtoMQV(V,p,s) = ZMtoMQV(V,p,a*s);

theorem :: ZMODUL04:37
  for p being prime Element of INT.Ring,
      V being free Z_Module, I being Subset of V,
  IQ being Subset of Z_MQ_VectSp(V,p),
  l be Linear_Combination of I
  st IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I}
  holds
  ZMtoMQV(V,p,Sum(l)) in Lin(IQ);

theorem :: ZMODUL04:38
  for p being prime Element of INT.Ring,
      V being free Z_Module, I being Subset of V,
  IQ being Subset of Z_MQ_VectSp(V,p)
  st Lin(I) = the ModuleStr of V &
  IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} holds
  Lin(IQ) = the ModuleStr of Z_MQ_VectSp(V,p);

theorem :: ZMODUL04:39
  for V being finitely-generated free Z_Module
  holds ex A being finite Subset of V st A is Basis of V;

registration
  cluster -> finite-rank for finitely-generated free Z_Module;
end;

registration
  cluster -> finitely-generated for finite-rank free Z_Module;
end;

theorem :: ZMODUL04:40
  for V be finite-rank free Z_Module holds for A being Subset of V
  st A is linearly-independent holds A is finite;

registration
  let V be Z_Module, W1, W2 be finite-rank free Subspace of V;
  cluster W1 /\ W2 -> free;
end;

registration
  let V be Z_Module, W1, W2 be finite-rank free Subspace of V;
  cluster W1 /\ W2 -> finite-rank;
end;

registration
  let V be finite-rank free Z_Module;
  cluster -> finite-rank for Subspace of V;
end;