:: Quotient Module of $\mathbb Z$-module
::  by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received May 7, 2012
:: Copyright (c) 2012-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, FINSEQ_1, SUBSET_1, RLVECT_1, STRUCT_0, FUNCT_1,
      XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, ORDINAL4, XXREAL_0, TARSKI,
      CARD_1, SUPINF_2, ARYTM_1, NAT_1, FUNCT_2, FINSET_1, VALUED_1, RLSUB_1,
      QC_LANG1, BINOP_1, ZFMISC_1, INT_1, RLVECT_2, ZMODUL01, ZMODUL02,
      RLVECT_3, RMOD_2, INT_3, VECTSP_1, VECTSP_2, LOPBAN_1, MESFUNC1,
      REALSET1, RSSPACE, MONOID_0, SETFAM_1, VECTSP10, EC_PF_1, INT_2,
      ORDINAL1, FUNCSDOM, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
      ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1,
      FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, INT_2,
      REALSET1, FINSEQ_1, VALUED_1, FINSEQ_4, STRUCT_0, ALGSTR_0, RLVECT_1,
      VECTSP_1, RLVECT_2, INT_3, EC_PF_1, GROUP_1, VFUNCT_1, VECTSP_2,
      VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, ZMODUL01, VECTSP10;
 constructors BINOP_2, FINSEQ_4, RELSET_1, RLVECT_2, ZMODUL01, VECTSP_4,
      REALSET1, FUNCT_7, INT_3, NAT_D, GCD_1, VECTSP10, ALGSTR_1, VECTSP_6,
      BINOP_1, VECTSP_7, VECTSP_5, PARTFUN1, DOMAIN_1, FUNCOP_1, XXREAL_0,
      NAT_1, MEMBERED, VFUNCT_1;
 registrations RELSET_1, FINSET_1, XREAL_0, STRUCT_0, INT_1, ZMODUL01,
      XXREAL_0, ALGSTR_0, INT_3, VECTSP_1, XCMPLX_0, ORDINAL1, VECTSP_7,
      MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET;


begin :: 1. Quotient module of Z-module and vector space

reserve x, y, y1, y2 for set;
reserve R for Ring;
reserve V for LeftMod of R;
reserve u, v, w for VECTOR of V;
reserve F, G, H, I for FinSequence of V;
reserve i, j, k, n for Element of NAT;
reserve f, f9, g for sequence of V;

definition
  let R be Ring;
  let V be LeftMod of R;
  let a be Element of R;
  func a * V -> non empty Subset of V equals
:: ZMODUL02:def 1
  the set of all a * v where v is Element of V;
end;

definition
  let R be Ring;
  let V be LeftMod of R;
  let a be Element of R;
  func Zero_(a,V) -> Element of a*V equals
:: ZMODUL02:def 2
  0.V;
end;

definition
  let R be Ring;
  let V be LeftMod of R;
  let a be Element of R;
  func Add_(a,V) -> Function of [:a*V,a*V :], a*V equals
:: ZMODUL02:def 3
  (the addF of V) | [:a*V,a*V:];
end;

definition
  let R be commutative Ring;
  let V be VectSp of R;
  let a be Element of R;
  func Mult_(a,V) -> Function of [:the carrier of R,a*V :], a*V equals
:: ZMODUL02:def 4
  (the lmult of V) | [:the carrier of R, a*V:];
end;

definition
  let R be commutative Ring;
  let V be LeftMod of R;
  let a be Element of R;
  func a (*) V -> Subspace of V equals
:: ZMODUL02:def 5
  ModuleStr (# a * V, Add_(a,V), Zero_(a,V), Mult_(a,V) #);
end;

definition
::$CD 5
end;

theorem :: ZMODUL02:1
  for p be Element of INT.Ring, V be Z_Module, W be Submodule of V,
      x be VECTOR of VectQuot(V, W) st W = p (*) V
  holds p * x = 0.VectQuot(V, W);

theorem :: ZMODUL02:2
  for p, i be Element of INT.Ring, V be Z_Module, W be Submodule of V,
      x be VECTOR of VectQuot(V, W)
  st p <> 0 & W = p (*) V
  holds i * x = (i mod p) * x;

theorem :: ZMODUL02:3
  for p, q be Element of INT.Ring, V be Z_Module, W be Submodule of V,
  v be VECTOR of V
  st W = p (*) V & p > 1 & q > 1 & p,q are_coprime
  holds q * v = 0.V implies v + W = 0.VectQuot(V, W);

registration
  cluster prime for Element of INT.Ring;
end;

registration
  cluster prime -> natural for integer Number;
end;

definition
  let p be prime Element of INT.Ring;
  let V be Z_Module;
  func Mult_Mod_pV(V,p) -> Function of
  [:the carrier of GF(p), the carrier of VectQuot(V,p(*)V):],
  the carrier of VectQuot(V,p(*)V) means
:: ZMODUL02:def 11

  for a being Element of GF(p), i being Element of INT.Ring,
  x being Element of VectQuot(V,p(*)V) st a = i mod p
  holds it.(a,x) = (i mod p) * x;
end;

definition
  let p be prime Element of INT.Ring, V be Z_Module;
  func Z_MQ_VectSp(V,p) -> non empty strict ModuleStr over GF(p) equals
:: ZMODUL02:def 12
  ModuleStr (# the carrier of VectQuot(V,p(*)V),
  the addF of VectQuot(V,p(*)V), the ZeroF of VectQuot(V,p(*)V),
  Mult_Mod_pV(V,p) #);
end;

registration
  let p be prime Element of INT.Ring, V be Z_Module;
  cluster Z_MQ_VectSp(V,p) -> scalar-distributive vector-distributive
    scalar-associative scalar-unital add-associative right_zeroed
    right_complementable Abelian;
end;

definition
  let p be prime Element of INT.Ring, V be Z_Module, v be VECTOR of V;
  func ZMtoMQV(V,p,v) -> Vector of Z_MQ_VectSp(V,p) equals
:: ZMODUL02:def 13
  v + p(*)V;
end;

definition
  let R be Ring; let X be LeftMod of R;
  func Mult_INT*(X) -> Function of
  [:the carrier of R,the carrier of X:], the carrier of X equals
:: ZMODUL02:def 14
  the lmult of X;
end;

definition
  let R be Ring;
  let X be LeftMod of R;
  func modetrans(X) -> non empty strict ModuleStr over R equals
:: ZMODUL02:def 15
  ModuleStr (#the carrier of X, the addF of X, the ZeroF of X, Mult_INT*(X) #);
end;

registration
  let R be Ring; let X be LeftMod of R;
  cluster modetrans(X) -> Abelian add-associative right_zeroed
    right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital;
end;

definition
::$CD 13
end;

::$CT 4

begin :: 2. Linear combination of Z-module

reserve K,L,L1,L2,L3 for Linear_Combination of V;

theorem :: ZMODUL02:8
  for R being Ring
  for V be LeftMod of R, L be Linear_Combination of V,
      v be Element of V holds L.v = 0.R iff not v in Carrier(L);

theorem :: ZMODUL02:9
  for R being Ring
  for V be LeftMod of R, v be Element of V holds (ZeroLC(V)).v = 0.R;

reserve a, b for Element of R;
reserve G, H1, H2, F, F1, F2, F3 for FinSequence of V;
reserve A, B for Subset of V,
  v1, v2, v3, u1, u2, u3 for Vector of V,
  f for Function of V, R,
  i for Element of NAT;
reserve l, l1, l2 for Linear_Combination of A;

theorem :: ZMODUL02:10
  A c= B implies l is Linear_Combination of B;

theorem :: ZMODUL02:11
  ZeroLC(V) is Linear_Combination of A;

theorem :: ZMODUL02:12
  for l being Linear_Combination of {}the carrier of V holds l = ZeroLC(V);

theorem :: ZMODUL02:13
  i in dom F & v = F.i implies (f (#) F).i = f.v * v;

theorem :: ZMODUL02:14
  f (#) <*>(the carrier of V) = <*>(the carrier of V);

theorem :: ZMODUL02:15
  f (#) <* v *> = <* f.v * v *>;

theorem :: ZMODUL02:16
  f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>;

theorem :: ZMODUL02:17
  f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *>;

theorem :: ZMODUL02:18
  R is non degenerated implies
   (A <> {} & A is linearly-closed iff for l holds Sum(l) in A);

theorem :: ZMODUL02:19
  Sum(ZeroLC(V)) = 0.V;

theorem :: ZMODUL02:20
  for l being Linear_Combination of {}(the carrier of V) holds Sum(l) = 0.V;

theorem :: ZMODUL02:21
  for l being Linear_Combination of {v} holds Sum(l) = l.v * v;

theorem :: ZMODUL02:22
  v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds
    Sum(l) = l.v1 * v1 + l.v2 * v2;

theorem :: ZMODUL02:23
  Carrier(L) = {} implies Sum(L) = 0.V;

theorem :: ZMODUL02:24
  Carrier(L) = {v} implies Sum(L) = L.v * v;

theorem :: ZMODUL02:25
  Carrier(L) = {v1,v2} & v1 <> v2 implies Sum(L) = L.v1 * v1 + L.v2 * v2;

theorem :: ZMODUL02:26
  Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2);

theorem :: ZMODUL02:27
  L1 is Linear_Combination of A & L2 is Linear_Combination of A
  implies L1 + L2 is Linear_Combination of A;

theorem :: ZMODUL02:28
  L1 + (L2 + L3) = L1 + L2 + L3;

registration let R,V,L;
  reduce L + ZeroLC(V) to L;
end;

theorem :: ZMODUL02:29
  for V being Z_Module,
      a being Element of INT.Ring,
      L being Linear_Combination of V holds
  a <> 0.INT.Ring implies Carrier(a * L) = Carrier(L);

theorem :: ZMODUL02:30
  0.R * L = ZeroLC(V);

theorem :: ZMODUL02:31
  L is Linear_Combination of A implies a * L is Linear_Combination of A;

theorem :: ZMODUL02:32
  (a + b) * L = a * L + b * L;

theorem :: ZMODUL02:33
  a * (L1 + L2) = a * L1 + a * L2;

theorem :: ZMODUL02:34
  a * (b * L) = (a * b) * L;

registration let R,V,L;
  reduce (1.R)*L to L;
end;

theorem :: ZMODUL02:35
  (- L).v = - L.v;

theorem :: ZMODUL02:36
  L1 + L2 = ZeroLC(V) implies L2 = - L1;

theorem :: ZMODUL02:37
  Carrier(- L) = Carrier(L);

theorem :: ZMODUL02:38
  L is Linear_Combination of A
  implies - L is Linear_Combination of A;

theorem :: ZMODUL02:39
  (L1 - L2).v = L1.v - L2.v;

theorem :: ZMODUL02:40
  Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2);

theorem :: ZMODUL02:41
  L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
  L1 - L2 is Linear_Combination of A;

theorem :: ZMODUL02:42
  L - L = ZeroLC(V);

definition
  let R,V;
  func LinComb(V) -> set means
:: ZMODUL02:def 29
  x in it iff x is Linear_Combination of V;
end;

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

 reserve e, e1, e2 for Element of LinComb(V);

definition
  let R,V, e;
  func @e -> Linear_Combination of V equals
:: ZMODUL02:def 30
  e;
end;

definition
  let R,V, L;
  func @L -> Element of LinComb(V) equals
:: ZMODUL02:def 31
  L;
end;

definition
  let R,V;
  func LCAdd(V) -> BinOp of LinComb(V) means
:: ZMODUL02:def 32
  for e1, e2 holds it.(e1,e2) = @e1 + @e2;
end;

definition
  let R,V;
  func LCMult(V) -> Function of [:the carrier of R, LinComb(V):],
    LinComb(V) means
:: ZMODUL02:def 33
  for a, e holds it. [a,e] = a * @e;
end;

definition let R,V;
  func LC_Z_Module V -> ModuleStr over R equals
:: ZMODUL02:def 34
    ModuleStr (# LinComb(V), LCAdd(V), @ZeroLC(V), LCMult(V) #);
end;

registration let R,V;
  cluster LC_Z_Module V -> strict non empty;
end;

registration let R,V;
  cluster LC_Z_Module V -> Abelian add-associative right_zeroed
    right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital;
end;

theorem :: ZMODUL02:43
  the carrier of LC_Z_Module(V) = LinComb(V);

theorem :: ZMODUL02:44
  0.LC_Z_Module(V) = ZeroLC(V);

theorem :: ZMODUL02:45
  the addF of LC_Z_Module(V) = LCAdd(V);

theorem :: ZMODUL02:46
  the lmult of LC_Z_Module(V) = LCMult(V);

theorem :: ZMODUL02:47
  vector(LC_Z_Module(V),L1) + vector(LC_Z_Module(V),L2) = L1 + L2;

theorem :: ZMODUL02:48
  a * vector(LC_Z_Module(V),L) = a * L;

theorem :: ZMODUL02:49
  - vector(LC_Z_Module(V),L) = - L;

theorem :: ZMODUL02:50
  vector(LC_Z_Module(V),L1) - vector(LC_Z_Module(V),L2) = L1 - L2;

definition
  let R,V,A;
  func LC_Z_Module(A) -> strict Submodule of LC_Z_Module(V) means
:: ZMODUL02:def 35
  the carrier of it = the set of all l;
end;

begin :: 3. Linearly independent subset of Z-module

reserve W, W1, W2, W3 for Submodule of V;
reserve v, v1, v2, u for Vector of V;
reserve A, B, C for Subset of V;
reserve T for finite Subset of V;
reserve L, L1, L2 for Linear_Combination of V;
reserve l for Linear_Combination of A;
reserve F, G, H for FinSequence of V;
reserve f, g for Function of V, R;

theorem :: ZMODUL02:51
  f (#) (F ^ G) = (f (#) F) ^ (f (#) G);

theorem :: ZMODUL02:52
  Sum(L1 + L2) = Sum(L1) + Sum(L2);

theorem :: ZMODUL02:53
  Sum(a * L) = a * Sum(L);

theorem :: ZMODUL02:54
  Sum(- L) = - Sum(L);

theorem :: ZMODUL02:55
  Sum(L1 - L2) = Sum(L1) - Sum(L2);

theorem :: ZMODUL02:56
  R is commutative &
  A c= B & B is linearly-independent implies A is linearly-independent;

theorem :: ZMODUL02:57
  R is non degenerated &
  A is linearly-independent implies not 0.V in A;

theorem :: ZMODUL02:58
  {}(the carrier of V) is linearly-independent;

registration
  let R be Ring;
  let V be LeftMod of R;
  cluster linearly-independent for Subset of V;
end;

theorem :: ZMODUL02:59
  R is non degenerated & V is Mult-cancelable implies
  ({v} is linearly-independent iff v <> 0.V);

registration let R be non degenerated Ring;
             let V be LeftMod of R;
  cluster {0.V} -> linearly-dependent for Subset of V;
end;

theorem :: ZMODUL02:60
  R is commutative non degenerated &
  {v1,v2} is linearly-independent implies v1 <> 0.V;

theorem :: ZMODUL02:61
  R is commutative non degenerated implies
    {v,0.V} is linearly-dependent;

theorem :: ZMODUL02:62
  R = INT.Ring &
:::  R is commutative non degenerated &
  V is Mult-cancelable implies
  (v1 <> v2 & {v1,v2} is linearly-independent iff v2 <> 0.V &
  for a, b being Element of R st b <> 0.R holds
    b * v1 <> a * v2);

theorem :: ZMODUL02:63
  R = INT.Ring &
  V is Mult-cancelable implies
  (v1 <> v2 & {v1,v2} is linearly-independent iff
  for a,b st a * v1 + b * v2 = 0.V holds a = 0.R & b = 0.R);

theorem :: ZMODUL02:64
  x in Lin(A) iff ex l st x = Sum(l);

theorem :: ZMODUL02:65
  x in A implies x in Lin(A);

theorem :: ZMODUL02:66
  for x being object holds x in (0).V iff x = 0.V;

theorem :: ZMODUL02:67
  Lin({}(the carrier of V)) = (0).V;

theorem :: ZMODUL02:68
  Lin(A) = (0).V implies A = {} or A = {0.V};

theorem :: ZMODUL02:69
  for V being strict LeftMod of R,A being Subset of V holds
  A = the carrier of V implies Lin(A) = V;

theorem :: ZMODUL02:70
  A c= B implies Lin(A) is Submodule of Lin(B);

theorem :: ZMODUL02:71
  for V being strict Z_Module,A,B being Subset of V holds
  Lin(A) = V & A c= B implies Lin(B) = V;

theorem :: ZMODUL02:72
  Lin(A \/ B) = Lin(A) + Lin(B);

theorem :: ZMODUL02:73
  Lin(A /\ B) is Submodule of Lin(A) /\ Lin(B);

begin :: 4. Theorems related to submodule

theorem :: ZMODUL02:74
  W1 is Submodule of W3 implies W1 /\ W2 is Submodule of W3;

theorem :: ZMODUL02:75
  W1 is Submodule of W2 & W1 is Submodule of W3 implies W1 is Submodule of
  W2 /\ W3;

theorem :: ZMODUL02:76
  W1 is Submodule of W3 & W2 is Submodule of W3 implies W1 + W2 is
  Submodule of W3;

theorem :: ZMODUL02:77
  W1 is Submodule of W2 implies W1 is Submodule of W2 + W3;