:: Domains of Submodules, Join and Meet of Finite Sequences of Submodules
:: and Quotient Modules
::  by Micha{\l} Muzalewski
::
:: Received March 29, 1993
:: Copyright (c) 1993-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 SUBSET_1, XBOOLE_0, BINOP_1, FUNCT_1, MULTOP_1, FUNCSDOM,
      VECTSP_1, VECTSP_2, RLVECT_2, RLSUB_1, FINSEQ_1, RMOD_3, ARYTM_1,
      ARYTM_3, ZFMISC_1, RLVECT_3, SUPINF_2, GROUP_1, TARSKI, CARD_3, MOD_3,
      STRUCT_0, RLSUB_2, INCSP_1, PARTFUN1, PRELAMB, SETWISEO, LATTICES,
      QC_LANG1, FINSEQ_4, ALGSTR_0, RLVECT_1, RELAT_1, LMOD_7;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, STRUCT_0, ALGSTR_0,
      FUNCT_2, BINOP_1, FINSEQ_1, SETWISEO, SETWOP_2, LATTICES, MULTOP_1,
      RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6,
      VECTSP_7, LMOD_6;
 constructors BINOP_1, DOMAIN_1, SETWISEO, MULTOP_1, FINSOP_1, LATTICES,
      VECTSP_6, VECTSP_7, LMOD_6, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, STRUCT_0, LATTICES, VECTSP_1, VECTSP_4,
      VECTSP_5, LATTICE2, ALGSTR_0;
 requirements BOOLE, SUBSET;


begin ::  Schemes

scheme :: LMOD_7:sch 1
 ElementEq {A()->set,P[object]} :
 for X1,X2 being Element of A() st
  (for x being object holds x in X1 iff P[x]) &
  (for x being object holds x in X2 iff P[x]) holds X1 = X2;

scheme :: LMOD_7:sch 2
 UnOpEq {A() -> non empty set, F(Element of A()) -> object}:
  for f1,f2 being UnOp of A() st
  (for a being Element of A() holds f1.(a) = F(a))
  & (for a being Element of A() holds f2.(a) = F(a)) holds f1 = f2;

scheme :: LMOD_7:sch 3
 TriOpEq {A() -> non empty set,
  F(Element of A(),Element of A(),Element of A()) -> object}:
  for f1,f2 being TriOp of A() st
  (for a,b,c being Element of A() holds f1.(a,b,c) = F(a,b,c))
  & (for a,b,c being Element of A() holds f2.(a,b,c) = F(a,b,c)) holds f1 = f2;

scheme :: LMOD_7:sch 4
 QuaOpEq {A() -> non empty set,
  F(Element of A(),Element of A(),Element of A(),Element of A()) -> object}:
  for f1,f2 being QuaOp of A() st
  (for a,b,c,d being Element of A() holds f1.(a,b,c,d) = F(a,b,c,d))
  & (for a,b,c,d being Element of A() holds f2.(a,b,c,d) = F(a,b,c,d))
  holds f1 = f2;

scheme :: LMOD_7:sch 5
 Fraenkel1Ex {A, D() -> non empty set,
  F(object) -> Element of D(), P[object]} : ex S being Subset of D()
  st S = {F(x) where x is Element of A() : P[x]};

scheme :: LMOD_7:sch 6
 Fr0 {A() -> non empty set, x() -> Element of A(), P[object]} : P[x()]
provided
 x() in {a where a is Element of A() : P[a]};

scheme :: LMOD_7:sch 7
 Fr1
  {X() -> set, A() -> non empty set, a() -> Element of A(), P[object]}:
  a() in X() iff P[a()]
provided
 X() = {a where a is Element of A() : P[a]};

scheme :: LMOD_7:sch 8
 Fr2
  {X() -> set, A() -> non empty set, a() -> Element of A(), P[object]}:
  P[a()]
provided
 a() in X() and
 X() = {a where a is Element of A() : P[a]};

scheme :: LMOD_7:sch 9
 Fr3 {x() -> set, X() -> set, A() -> non empty set, P[object]} :
  x() in X() iff ex a being Element of A() st x()=a & P[a]
provided
 X() = {a where a is Element of A() : P[a]};

scheme :: LMOD_7:sch 10
 Fr4 {D1,D2() -> non empty set, B() -> set,
  a() -> Element of D1(), F(object) -> set, P,Q[object,object]} :
  a() in F(B()) iff for b being Element of D2() st b in B() holds P[a(),b]
provided
 F(B()) = {a where a is Element of D1() : Q[a,B()]} and
 Q[a(),B()] iff for b being Element of D2() st b in B() holds P[a(),b];

begin :: Main Part

reserve x for set,
  K for Ring,
  r for Scalar of K,
  V for LeftMod of K,
  a,b,a1,a2 for Vector of V,
  A,A1,A2 for Subset of V,
  l for Linear_Combination of A,
  W for Subspace of V,
  Li for FinSequence of Submodules(V);

::    1. Auxiliary theorems about free-modules

theorem :: LMOD_7:1
  K is non trivial & A is linearly-independent implies not 0.V in A;

theorem :: LMOD_7:2
  not a in A implies l.a = 0.K;

theorem :: LMOD_7:3
  K is trivial implies (for l holds Carrier(l) = {}) & Lin A is trivial;

theorem :: LMOD_7:4
  V is non trivial implies for A st A is base holds A <> {};

theorem :: LMOD_7:5
  A1 \/ A2 is linearly-independent & A1 misses A2
  implies Lin A1 /\ Lin A2 = (0).V;

theorem :: LMOD_7:6
  A is base & A = A1 \/ A2 & A1 misses A2 implies
  V is_the_direct_sum_of Lin A1,Lin A2;

begin :: 2. Domains of submodules

definition
  let K,V;
  mode SUBMODULE_DOMAIN of V -> non empty set means
:: LMOD_7:def 1

    x in it implies x is strict Subspace of V;
end;

definition
  let K,V;
  redefine func Submodules(V) -> SUBMODULE_DOMAIN of V;
end;

definition
  let K,V;
  let D be SUBMODULE_DOMAIN of V;
  redefine mode Element of D -> strict Subspace of V;
end;

registration
  let K,V;
  let D be SUBMODULE_DOMAIN of V;
  cluster strict for Element of D;
end;

definition
  let K,V;
  assume
 V is non trivial;
  mode LINE of V -> strict Subspace of V means
:: LMOD_7:def 2
    ex a st a<>0.V & it = <:a:>;
end;

definition
  let K,V;
  mode LINE_DOMAIN of V -> non empty set means
:: LMOD_7:def 3

    x in it implies x is LINE of V;
end;

definition
  let K,V;
  func lines(V) -> LINE_DOMAIN of V means
:: LMOD_7:def 4
  for x being object holds x in it iff x is LINE of V;
end;

definition
  let K,V;
  let D be LINE_DOMAIN of V;
  redefine mode Element of D -> LINE of V;
end;

definition
  let K,V;
  assume that
 V is non trivial and
 V is free;
  mode HIPERPLANE of V -> strict Subspace of V means
:: LMOD_7:def 5
    ex a st a<>0.V & V is_the_direct_sum_of <:a:>,it;
end;

definition
  let K,V;
  mode HIPERPLANE_DOMAIN of V -> non empty set means
:: LMOD_7:def 6

    x in it implies x is HIPERPLANE of V;
end;

definition
  let K,V;
  func hiperplanes(V) -> HIPERPLANE_DOMAIN of V means
:: LMOD_7:def 7
  for x being object holds x in it iff x is HIPERPLANE of V;
end;

definition
  let K,V;
  let D be HIPERPLANE_DOMAIN of V;
  redefine mode Element of D -> HIPERPLANE of V;
end;

begin :: 3. Join and meet of finite sequences of submodules

definition
  let K,V,Li;
  func Sum Li -> Element of Submodules(V) equals
:: LMOD_7:def 8
  SubJoin(V) $$ Li;
  func /\ Li -> Element of Submodules(V) equals
:: LMOD_7:def 9
  SubMeet(V) $$ Li;
end;

theorem :: LMOD_7:7
  SubJoin(V) is commutative associative & SubJoin(V) is having_a_unity
  & (0).V = the_unity_wrt SubJoin(V);

theorem :: LMOD_7:8
  SubMeet(V) is commutative associative & SubMeet(V)
  is having_a_unity & (Omega).V = the_unity_wrt SubMeet(V);

begin :: 4. Sum of subsets of module

definition
  let K,V,A1,A2;
  func A1 + A2 -> Subset of V means
:: LMOD_7:def 10
  x in it iff ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2;
end;

begin :: 5. Vector of subset

definition
  let K,V,A;
  assume
 A <> {};
  mode Vector of A -> Vector of V means
:: LMOD_7:def 11

    it is Element of A;
end;

theorem :: LMOD_7:9
  A1 <> {} & A1 c= A2 implies for x st x is Vector of A1 holds x is Vector of
  A2;

::  6. Quotient modules

theorem :: LMOD_7:10
  a2 in a1 + W iff a1 - a2 in W;

theorem :: LMOD_7:11
  a1 + W = a2 + W iff a1 - a2 in W;

definition
  let K,V,W;
  func V..W -> set means
:: LMOD_7:def 12

  x in it iff ex a st x = a + W;
end;

registration
  let K,V,W;
  cluster V..W -> non empty;
end;

definition
  let K,V,W,a;
  func a..W -> Element of V..W equals
:: LMOD_7:def 13
  a + W;
end;

theorem :: LMOD_7:12
  for x being Element of V..W ex a st x = a..W;

theorem :: LMOD_7:13
  a1..W = a2..W iff a1 - a2 in W;

reserve S1,S2 for Element of V..W;

definition
  let K,V,W,S1;
  func -S1 -> Element of V..W means
:: LMOD_7:def 14
  S1 = a..W implies it = (-a)..W;
  let S2;
  func S1 + S2 -> Element of V..W means
:: LMOD_7:def 15

  S1 = a1..W & S2 = a2..W implies it = (a1+a2)..W;
end;

definition
  let K,V,W;
  func COMPL W -> UnOp of V..W means
:: LMOD_7:def 16
  it.S1 = -S1;
  func ADD W -> BinOp of V..W means
:: LMOD_7:def 17

  it.(S1,S2) = S1 + S2;
end;

definition
  let K,V,W;
  func V.W -> strict addLoopStr equals
:: LMOD_7:def 18
  addLoopStr(#V..W,ADD W,(0.V)..W#);
end;

registration
  let K,V,W;
  cluster V.W -> non empty;
end;

theorem :: LMOD_7:14
  a..W is Element of V.W;

definition
  let K,V,W,a;
  func a.W -> Element of V.W equals
:: LMOD_7:def 19
  a..W;
end;

theorem :: LMOD_7:15
  for x being Element of V.W ex a st x = a.W;

theorem :: LMOD_7:16
  a1.W = a2.W iff a1 - a2 in W;

theorem :: LMOD_7:17
  a.W + b.W = (a+b).W & 0.(V.W) = (0.V).W;

registration
  let K,V,W;
  cluster V.W -> Abelian add-associative right_zeroed right_complementable;
end;

reserve S for Element of V.W;

definition
  let K,V,W,r,S;
  func r*S -> Element of V.W means
:: LMOD_7:def 20

  S = a.W implies it = (r*a).W;
end;

definition
  let K,V,W;
  func LMULT W -> Function of [:the carrier of K,the carrier of V.W:],
  the carrier of V.W means
:: LMOD_7:def 21

  it.(r,S) = r*S;
end;

begin

definition
  let K,V,W;
  func V/W -> strict ModuleStr over K equals
:: LMOD_7:def 22
  ModuleStr(#the carrier of V.W,the addF of V.W,0.V.W,LMULT W#);
end;

registration
  let K,V,W;
  cluster V/W -> non empty;
end;

theorem :: LMOD_7:18
  a.W is Vector of V/W;

theorem :: LMOD_7:19
  for x being Vector of V/W holds x is Element of V.W;

definition
  let K,V,W,a;
  func a/W -> Vector of V/W equals
:: LMOD_7:def 23
  a.W;
end;

theorem :: LMOD_7:20
  for x being Vector of V/W ex a st x = a/W;

theorem :: LMOD_7:21
  a1/W = a2/W iff a1 - a2 in W;

theorem :: LMOD_7:22
  a/W + b/W = (a+b)/W & r*(a/W) = (r*a)/W;

theorem :: LMOD_7:23
  V/W is strict LeftMod of K;

registration
  let K,V,W;
  cluster V/W -> vector-distributive scalar-distributive
  scalar-associative scalar-unital;
end;