:: 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-2012 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, FUNCSDOM, VECTSP_2, VECTSP_4, VECTSP_5,
      VECTSP_6, LMOD_5, MOD_3, LMOD_6;
 constructors BINOP_1, DOMAIN_1, SETWISEO, MULTOP_1, FINSOP_1, LATTICES,
      VECTSP_6, LMOD_5, MOD_3, LMOD_6, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, STRUCT_0, LATTICES, VECTSP_1, VECTSP_4,
      VECTSP_5, LATTICE2, ALGSTR_0;
 requirements BOOLE, SUBSET;
 definitions RLVECT_1, STRUCT_0, XBOOLE_0, ALGSTR_0;
 theorems BINOP_1, FUNCT_2, RLVECT_1, LMOD_5, LMOD_6, MOD_3, MULTOP_1,
      SETWISEO, SUBSET_1, TARSKI, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6,
      ZFMISC_1, XBOOLE_0, XBOOLE_1, STRUCT_0, ALGSTR_0;
 schemes BINOP_1, DOMAIN_1, FUNCT_2, XBOOLE_0, BINOP_2;

begin ::  Schemes

scheme ElementEq {A()->set,P[set]} : for X1,X2 being Element of A() st
  (for x being set holds x in X1 iff P[x]) &
  (for x being set holds x in X2 iff P[x]) holds X1 = X2
proof
  let X1,X2 be Element of A() such that
A1: for x being set holds x in X1 iff P[x] and
A2: for x being set holds x in X2 iff P[x];
  now
    let x be set;
    x in X1 iff P[x] by A1;
    hence x in X1 iff x in X2 by A2;
  end;
  hence thesis by TARSKI:1;
end;

scheme UnOpEq {A() -> non empty set, F(Element of A()) -> set}:
  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
proof
  let f1,f2 be UnOp of A() such that
A1: for a being Element of A() holds f1.(a) = F(a) and
A2: for a being Element of A() holds f2.(a) = F(a);
  now
    let a be Element of A();
    thus f1.(a) = F(a) by A1
      .= f2.(a) by A2;
  end;
  hence thesis by FUNCT_2:63;
end;

scheme TriOpEq {A() -> non empty set,
  F(Element of A(),Element of A(),Element of A()) -> set}:
  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
proof
  let f1,f2 be TriOp of A() such that
A1: for a,b,c being Element of A() holds f1.(a,b,c) = F(a,b,c) and
A2: for a,b,c being Element of A() holds f2.(a,b,c) = F(a,b,c);
  now
    let a,b,c be Element of A();
    thus f1.(a,b,c) = F(a,b,c) by A1
      .= f2.(a,b,c) by A2;
  end;
  hence thesis by MULTOP_1:3;
end;

scheme QuaOpEq {A() -> non empty set,
  F(Element of A(),Element of A(),Element of A(),Element of A()) -> set}:
  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
proof
  let f1,f2 be QuaOp of A() such that
A1: for a,b,c,d being Element of A() holds f1.(a,b,c,d) = F(a,b,c,d) and
A2: for a,b,c,d being Element of A() holds f2.(a,b,c,d) = F(a,b,c,d);
  now
    let a,b,c,d be Element of A();
    thus f1.(a,b,c,d) = F(a,b,c,d) by A1
      .= f2.(a,b,c,d) by A2;
  end;
  hence thesis by MULTOP_1:6;
end;

scheme Fraenkel1Ex {A, D() -> non empty set,
  F(set) -> Element of D(), P[set]} : ex S being Subset of D()
  st S = {F(x) where x is Element of A() : P[x]}
proof
  reconsider S={F(x) where x is Element of A() : P[x]} as Subset of D()
  from DOMAIN_1:sch 8;
  take S;
  thus thesis;
end;

scheme Fr0 {A() -> non empty set, x() -> Element of A(), P[set]} : P[x()]
provided
A1: x() in {a where a is Element of A() : P[a]}
proof
  ex a being Element of A() st x()=a & P[a] by A1;
  hence thesis;
end;

scheme Fr1 {X() -> set, A() -> non empty set, a() -> Element of A(), P[set]} :
  a() in X() iff P[a()]
provided
A1: X() = {a where a is Element of A() : P[a]}
proof
  thus a() in X() implies P[a()]
  proof
    assume a() in X();
    then
A2: a() in {a where a is Element of A() : P[a]} by A1;
    thus P[a()] from Fr0(A2);
  end;
  assume P[a()];
  hence thesis by A1;
end;

scheme Fr2 {X() -> set, A() -> non empty set, a() -> Element of A(), P[set]}:
  P[a()]
provided
A1: a() in X() and
A2: X() = {a where a is Element of A() : P[a]}
proof
A3: a() in {a where a is Element of A() : P[a]} by A1,A2;
  thus P[a()] from Fr0(A3);
end;

scheme Fr3 {x() -> set, X() -> set, A() -> non empty set, P[set]} :
  x() in X() iff ex a being Element of A() st x()=a & P[a]
provided
A1: X() = {a where a is Element of A() : P[a]}
proof
  thus thesis by A1;
end;

scheme Fr4 {D1,D2() -> non empty set, B() -> set,
  a() -> Element of D1(), F(set) -> set, P[set,set], Q[set,set]} :
  a() in F(B()) iff for b being Element of D2() st b in B() holds P[a(),b]
provided
A1: F(B()) = {a where a is Element of D1() : Q[a,B()]} and
A2: Q[a(),B()] iff for b being Element of D2() st b in B() holds P[a(),b]
proof
  thus a() in F(B()) implies for b being Element of D2() st b in
  B() holds P[a(),b]
  proof
    defpred X[set] means Q[$1,B()];
    assume a() in F(B());
    then
A3: a() in {a where a is Element of D1() : X[a]} by A1;
    X[a()] from Fr0(A3);
    hence thesis by A2;
  end;
  assume for b being Element of D2() st b in B() holds P[a(),b];
  hence thesis by A1,A2;
end;

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);

Lm1: for G being AbGroup, a,b,c being Element of G holds
-(a-b) = -a-(-b) & a-b+c = a+c-b
proof
  let G be AbGroup, a,b,c be Element of G;
  thus -(a-b) = -a+b by VECTSP_1:17
    .= -a-(-b) by RLVECT_1:17;
  thus thesis by RLVECT_1:def 3;
end;

::    1. Auxiliary theorems about free-modules

theorem Th1:
  K is non trivial & A is linearly-independent implies not 0.V in A
proof
  assume that
A1: K is non trivial and
A2: A is linearly-independent;
  0.K <> 1_K by A1,LMOD_6:def 1;
  hence thesis by A2,LMOD_5:2;
end;

theorem Th2:
  not a in A implies l.a = 0.K
proof
  assume
A1: not a in A;
  Carrier l c= A by VECTSP_6:def 4;
  then not a in Carrier l by A1;
  hence thesis by VECTSP_6:2;
end;

theorem
  K is trivial implies (for l holds Carrier(l) = {}) & Lin A is trivial
proof
  assume
A1: K is trivial;
  thus
A2: for l holds Carrier l = {}
  proof
    let l;
    assume
A3: Carrier l <> {};
    set x = the Element of Carrier l;
    ex a st ( x = a)&( l.a <> 0.K) by A3,VECTSP_6:1;
    hence contradiction by A1,LMOD_6:5;
  end;
  now
    let a be Vector of Lin A;
    a in Lin A by RLVECT_1:1;
    then consider l such that
A4: a = Sum(l) by MOD_3:4;
    Carrier l = {} by A2;
    then a = 0.V by A4,VECTSP_6:19;
    hence a=0.(Lin A) by VECTSP_4:11;
  end;
  hence thesis by STRUCT_0:def 18;
end;

theorem Th4:
  V is non trivial implies for A st A is base holds A <> {}
proof
  assume
A1: V is non trivial;
  let A such that
A2: A is base and
A3: A = {};
A4: A = {}(the carrier of V) by A3;
  the VectSpStr of V = Lin A by A2,MOD_3:def 2
    .= (0).V by A4,MOD_3:6;
  hence contradiction by A1,LMOD_6:7;
end;

theorem Th5:
  A1 \/ A2 is linearly-independent & A1 misses A2
  implies Lin A1 /\ Lin A2 = (0).V
proof
  assume that
A1: A1 \/ A2 is linearly-independent and
A2: A1 /\ A2 = {};
  reconsider P=Lin A1 /\ Lin A2 as strict Subspace of V;
  set Z=the carrier of P;
A3: Z=(the carrier of Lin A1)/\ (the carrier of Lin A2) by VECTSP_5:def 2;
A4: now
    let x;
    assume
A5: x in Z;
    then
A6: x in the carrier of Lin A1 by A3,XBOOLE_0:def 4;
A7: x in the carrier of Lin A2 by A3,A5,XBOOLE_0:def 4;
A8: x in Lin A1 by A6,STRUCT_0:def 5;
A9: x in Lin A2 by A7,STRUCT_0:def 5;
    consider l1 being Linear_Combination of A1 such that
A10: x = Sum(l1) by A8,MOD_3:4;
    consider l2 being Linear_Combination of A2 such that
A11: x = Sum(l2) by A9,MOD_3:4;
A12: Carrier l1 c= A1 by VECTSP_6:def 4;
    Carrier l2 c= A2 by VECTSP_6:def 4;
    then
A13: Carrier l1 \/ Carrier l2 c= A1 \/ A2 by A12,XBOOLE_1:13;
    Carrier(l1 - l2) c= Carrier l1 \/ Carrier l2 by VECTSP_6:41;
    then Carrier(l1 - l2) c= A1 \/ A2 by A13,XBOOLE_1:1;
    then reconsider l = l1 - l2 as Linear_Combination of A1 \/ A2
    by VECTSP_6:def 4;
    Sum(l) = Sum(l1) - Sum(l2) by VECTSP_6:47
      .= 0.V by A10,A11,VECTSP_1:19;
    then
A14: Carrier l = {} by A1,LMOD_5:def 1;
    Carrier l1 = {}
    proof
      assume
A15:  Carrier l1 <> {};
      set x = the Element of Carrier l1;
      consider b such that
A16:  x = b and
A17:  l1.b <> 0.K by A15,VECTSP_6:1;
      b in A1 by A12,A15,A16,TARSKI:def 3;
      then
A18:  not b in A2 by A2,XBOOLE_0:def 4;
      0.K = l.b by A14,VECTSP_6:2
        .= l1.b - l2.b by VECTSP_6:40;
      then l1.b = l2.b by RLVECT_1:21
        .= 0.K by A18,Th2;
      hence contradiction by A17;
    end;
    hence x = 0.V by A10,VECTSP_6:19;
  end;
  0.V in Lin A1 /\ Lin A2 by VECTSP_4:17;
  then x in Z iff x=0.V by A4,STRUCT_0:def 5;
  then Z = {0.V} by TARSKI:def 1;
  hence thesis by VECTSP_4:def 3;
end;

theorem Th6:
  A is base & A = A1 \/ A2 & A1 misses A2 implies
  V is_the_direct_sum_of Lin A1,Lin A2
proof
  assume that
A1: A is base and
A2: A = A1 \/ A2 and
A3: A1 misses A2;
  set W=the VectSpStr of V;
A4: A is linearly-independent by A1,MOD_3:def 2;
  Lin A = W by A1,MOD_3:def 2;
  then
A5: W = Lin A1 + Lin A2 by A2,MOD_3:12;
  Lin A1 /\ Lin A2 = (0).V by A2,A3,A4,Th5;
  hence thesis by A5,VECTSP_5:def 4;
end;

begin :: 2. Domains of submodules

definition
  let K,V;
  mode SUBMODULE_DOMAIN of V -> non empty set means
    :Def1:
    x in it implies x is strict Subspace of V;
  existence
  proof
    set a = the strict Subspace of V;
    set D = {a};
    take D;
    thus thesis by TARSKI:def 1;
  end;
end;

definition
  let K,V;
  redefine func Submodules(V) -> SUBMODULE_DOMAIN of V;
  coherence
  proof
    now
      let x;
      assume x in Submodules(V);
      then ex W being strict Subspace of V st ( W = x) by VECTSP_5:def 3;
      hence x is strict Subspace of V;
    end;
    hence thesis by Def1;
  end;
end;

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

registration
  let K,V;
  let D be SUBMODULE_DOMAIN of V;
  cluster strict for Element of D;
  existence
  proof
    set x = the Element of D;
    take x;
    thus thesis;
  end;
end;

definition
  let K,V;
  assume
A1: V is non trivial;
  mode LINE of V -> strict Subspace of V means
    ex a st a<>0.V & it = <:a:>;
  existence
  proof consider a such that
A2: a<>0.V by A1,STRUCT_0:def 18;
    take <:a:>;
    thus thesis by A2;
  end;
end;

definition
  let K,V;
  mode LINE_DOMAIN of V -> non empty set means
    :Def3:
    x in it implies x is LINE of V;
  existence
  proof
    set a = the LINE of V;
    set D = {a};
    take D;
    thus thesis by TARSKI:def 1;
  end;
end;

definition
  let K,V;
  func lines(V) -> LINE_DOMAIN of V means
  x in it iff x is LINE of V;
  existence
  proof
    set D = {a where a is Element of Submodules(V): a is LINE of V};
    set a1 = the LINE of V;
    reconsider a2 = a1 as Element of Submodules(V) by VECTSP_5:def 3;
    a2 in D;
    then reconsider D as non empty set;
A1: now
      let x;
      assume x in D;
      then ex a being Element of Submodules(V) st ( x = a)&( a is LINE of V);
      hence x is LINE of V;
    end;
    then reconsider D9 = D as LINE_DOMAIN of V by Def3;
    take D9;
    now
      let x;
      thus x in D9 implies x is LINE of V by A1;
      thus x is LINE of V implies x in D9
      proof
        assume
A2:     x is LINE of V;
        then reconsider x1 = x as Element of Submodules(V) by VECTSP_5:def 3;
        x1 in D by A2;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let D1,D2 be LINE_DOMAIN of V such that
A3: x in D1 iff x is LINE of V and
A4: x in D2 iff x is LINE of V;
    now
      let x;
      x in D1 iff x is LINE of V by A3;
      hence x in D1 iff x in D2 by A4;
    end;
    hence thesis by TARSKI:1;
  end;
end;

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

definition
  let K,V;
  assume that
A1: V is non trivial and
A2: V is free;
  mode HIPERPLANE of V -> strict Subspace of V means
    ex a st a<>0.V & V is_the_direct_sum_of <:a:>,it;
  existence
  proof
    consider A being Subset of V such that
A3: A is base by A2,MOD_3:def 3;
    reconsider A as Subset of V;
A4: A is linearly-independent by A3,MOD_3:def 2;
A5: A <> {} by A1,A3,Th4;
    set x = the Element of A;
    reconsider a = x as Vector of V by A5,TARSKI:def 3;
    reconsider A1 = {a} as Subset of V;
    set A2 = A\A1;
    set H = Lin(A2);
    A1 c= A by A5,ZFMISC_1:31;
    then
A6: A = A1 \/ A2 by XBOOLE_1:45;
    A1 misses A2 by XBOOLE_1:79;
    then
A7: V is_the_direct_sum_of Lin(A1),H by A3,A6,Th6;
A8: ex a st a<>0.V & V is_the_direct_sum_of <:a:>,H
    proof
      take a;
      thus thesis by A1,A4,A5,A7,Th1,LMOD_6:6,def 4;
    end;
    take H;
    thus thesis by A8;
  end;
end;

definition
  let K,V;
  mode HIPERPLANE_DOMAIN of V -> non empty set means
    :Def6:
    x in it implies x is HIPERPLANE of V;
  existence
  proof
    set a = the HIPERPLANE of V;
    set D = {a};
    take D;
    thus thesis by TARSKI:def 1;
  end;
end;

definition
  let K,V;
  func hiperplanes(V) -> HIPERPLANE_DOMAIN of V means
  x in it iff x is HIPERPLANE of V;
  existence
  proof
    set D = {a where a is Element of Submodules(V): a is HIPERPLANE of V};
    set a1 = the HIPERPLANE of V;
    reconsider a2 = a1 as Element of Submodules(V) by VECTSP_5:def 3;
    a2 in D;
    then reconsider D as non empty set;
A1: now
      let x;
      assume x in D;
      then ex a being Element of Submodules(V) st ( x = a)&( a is
      HIPERPLANE of V);
      hence x is HIPERPLANE of V;
    end;
    then reconsider D9 = D as HIPERPLANE_DOMAIN of V by Def6;
    take D9;
    now
      let x;
      thus x in D9 implies x is HIPERPLANE of V by A1;
      thus x is HIPERPLANE of V implies x in D9
      proof
        assume x is HIPERPLANE of V;
        then reconsider W=x as HIPERPLANE of V;
        reconsider x1 = W as Element of Submodules(V) by VECTSP_5:def 3;
        x1 in D;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let D1,D2 be HIPERPLANE_DOMAIN of V such that
A2: x in D1 iff x is HIPERPLANE of V and
A3: x in D2 iff x is HIPERPLANE of V;
    now
      let x;
      x in D1 iff x is HIPERPLANE of V by A2;
      hence x in D1 iff x in D2 by A3;
    end;
    hence thesis by TARSKI:1;
  end;
end;

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

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

definition
  let K,V,Li;
  func Sum Li -> Element of Submodules(V) equals
  SubJoin(V) $$ Li;
  coherence;
  func /\ Li -> Element of Submodules(V) equals
  SubMeet(V) $$ Li;
  coherence;
end;

theorem
  SubJoin(V) is commutative associative & SubJoin(V) is having_a_unity
  & (0).V = the_unity_wrt SubJoin(V)
proof
  set S0=Submodules(V), S1=SubJoin(V);
  reconsider L=LattStr(#(S0 qua non empty set),(S1 qua BinOp of S0),
    (SubMeet(V) qua BinOp of S0)#) as Lattice by VECTSP_5:57;
  S1=the L_join of L;
  hence S1 is commutative associative;
  set e=(0).V;
  reconsider e9=@e as Element of (S0 qua non empty set);
A1: e9=e by LMOD_6:def 2;
  now
    let a9 be Element of (S0 qua non empty set);
    reconsider b=a9 as Element of S0;
    reconsider a=b as strict Subspace of V;
    thus S1.(e9,a9) = e+a by A1,VECTSP_5:def 7
      .= a9 by VECTSP_5:9;
    thus S1.(a9,e9) = a+e by A1,VECTSP_5:def 7
      .= a9 by VECTSP_5:9;
  end;
  then
A2: e9 is_a_unity_wrt (S1 qua BinOp of S0) by BINOP_1:3;
  hence S1 is having_a_unity by SETWISEO:def 2;
  thus thesis by A1,A2,BINOP_1:def 8;
end;

theorem
  SubMeet(V) is commutative associative & SubMeet(V)
  is having_a_unity & (Omega).V = the_unity_wrt SubMeet(V)
proof
  set S0=Submodules(V), S2=SubMeet(V);
  reconsider L=LattStr(#(S0 qua non empty set),(SubJoin(V) qua BinOp of S0),
    (S2 qua BinOp of S0)#) as Lattice by VECTSP_5:57;
  S2=the L_meet of L;
  hence S2 is commutative associative;
  set e=(Omega).V;
  reconsider e9=@e as Element of (S0 qua non empty set);
A1: e9=e by LMOD_6:def 2;
  now
    let a9 be Element of (S0 qua non empty set);
    reconsider b=a9 as Element of S0;
    reconsider a=b as strict Subspace of V;
    thus (S2 qua BinOp of S0).(e9,a9) = e/\a by A1,VECTSP_5:def 8
      .= a9 by VECTSP_5:21;
    thus (S2 qua BinOp of S0).(a9,e9) = a/\e by A1,VECTSP_5:def 8
      .= a9 by VECTSP_5:21;
  end;
  then
A2: e9 is_a_unity_wrt (S2 qua BinOp of S0) by BINOP_1:3;
  hence S2 is having_a_unity by SETWISEO:def 2;
  thus thesis by A1,A2,BINOP_1:def 8;
end;

begin :: 4. Sum of subsets of module

definition
  let K,V,A1,A2;
  func A1 + A2 -> Subset of V means
  x in it iff ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2;
  existence
  proof
    set S = {a1+a2 : a1 in A1 & a2 in A2};
A1: now
      let x;
      assume x in S;
      then ex a1,a2 st ( x = a1+a2)&( a1 in A1)&( a2 in A2);
      hence ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2;
    end;
    now
      let x;
      assume x in S;
      then ex a1,a2 st ( x = a1+a2)&( a1 in A1)&( a2 in A2);
      hence x in the carrier of V;
    end;
    then reconsider S9 = S as Subset of V by TARSKI:def 3;
    take S9;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let D1,D2 be Subset of V such that
A2: x in D1 iff ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2 and
A3: x in D2 iff ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2;
    now
      let x;
      x in D1 iff ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2 by A2;
      hence x in D1 iff x in D2 by A3;
    end;
    hence thesis by TARSKI:1;
  end;
end;

begin :: 5. Vector of subset

definition
  let K,V,A;
  assume
A1: A <> {};
  mode Vector of A -> Vector of V means
    :Def11:
    it is Element of A;
  existence
  proof
    consider x being Element of V such that
A2: x in A by A1,SUBSET_1:4;
    take x;
    thus thesis by A2;
  end;
end;

theorem
  A1 <> {} & A1 c= A2 implies for x st x is Vector of A1 holds x is Vector of
  A2
proof
  assume that
A1: A1 <> {} and
A2: A1 c= A2;
  let x;
  assume x is Vector of A1;
  then reconsider a=x as Vector of A1;
  a is Element of A1 by A1,Def11;
  then a in A2 by A1,A2,TARSKI:def 3;
  hence thesis by Def11;
end;

::  6. Quotient modules

theorem Th10:
  a2 in a1 + W iff a1 - a2 in W
proof
  a1 - (a1 - a2) = a1 - a1 + a2 by RLVECT_1:29
    .= 0.V + a2 by VECTSP_1:19
    .= a2 by RLVECT_1:def 4;
  hence thesis by VECTSP_4:61;
end;

theorem Th11:
  a1 + W = a2 + W iff a1 - a2 in W
proof
  a2 in a1 + W iff a1 + W = a2 + W by VECTSP_4:55;
  hence thesis by Th10;
end;

definition
  let K,V,W;
  func V..W -> set means
  :Def12:
  x in it iff ex a st x = a + W;
  existence
  proof
    take {a + W : not contradiction};
    thus thesis;
  end;
  uniqueness
  proof
    defpred X[set] means ex a st $1 = a + W;
    thus for S1,S2 being set st
    (for x holds x in S1 iff X[x]) & (for x holds x in S2 iff X[x])
    holds S1 = S2 from XBOOLE_0:sch 3;
  end;
end;

registration
  let K,V,W;
  cluster V..W -> non empty;
  coherence
  proof
    a + W in V..W by Def12;
    hence thesis;
  end;
end;

definition
  let K,V,W,a;
  func a..W -> Element of V..W equals
  a + W;
  coherence by Def12;
end;

theorem Th12:
  for x being Element of V..W ex a st x = a..W
proof
  let x be Element of V..W;
  consider a such that
A1: x = a + W by Def12;
  take a;
  thus thesis by A1;
end;

theorem
  a1..W = a2..W iff a1 - a2 in W by Th11;

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

definition
  let K,V,W,S1;
  func -S1 -> Element of V..W means
  S1 = a..W implies it = (-a)..W;
  existence
  proof
    consider a1 such that
A1: S1 = a1..W by Th12;
A2: now
      let a be Vector of V;
      assume S1 = a..W;
      then a1 - a in W by A1,Th11;
      then -(a1 -a) in W by VECTSP_4:22;
      then -a1 - (-a) in W by Lm1;
      hence (-a1)..W = (-a)..W by Th11;
    end;
    take (-a1)..W;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let S,T be Element of V..W such that
A3: S1 = a..W implies S = (-a)..W and
A4: S1 = a..W implies T = (-a)..W;
    consider a1 such that
A5: S1 = a1..W by Th12;
    thus S = (-a1)..W by A3,A5
      .= T by A4,A5;
  end;
  let S2;
  func S1 + S2 -> Element of V..W means
  :Def15:
  S1 = a1..W & S2 = a2..W implies it = (a1+a2)..W;
  existence
  proof
    consider a1 such that
A6: S1 = a1..W by Th12;
    consider a2 such that
A7: S2 = a2..W by Th12;
A8: now
      let b1,b2 be Vector of V such that
A9:   S1 = b1..W and
A10:  S2 = b2..W;
A11:  a1 - b1 in W by A6,A9,Th11;
      a2 - b2 in W by A7,A10,Th11;
      then
A12:  (a1 - b1) + (a2 - b2) in W by A11,VECTSP_4:20;
      (a1-b1) + (a2-b2) = a1-b1+a2-b2 by RLVECT_1:def 3
        .= a1+a2-b1-b2 by Lm1
        .= (a1+a2) - (b1 + b2) by VECTSP_1:17;
      hence (a1 + a2)..W = (b1 + b2)..W by A12,Th11;
    end;
    take (a1 + a2)..W;
    thus thesis by A8;
  end;
  uniqueness
  proof
    let S,T be Element of V..W such that
A13: S1 = a1..W & S2 = a2..W implies S = (a1+a2)..W and
A14: S1 = a1..W & S2 = a2..W implies T = (a1+a2)..W;
    consider a1 such that
A15: S1 = a1..W by Th12;
    consider a2 such that
A16: S2 = a2..W by Th12;
    thus S = (a1+a2)..W by A13,A15,A16
      .= T by A14,A15,A16;
  end;
end;

definition
  let K,V,W;
  deffunc U(Element of V..W) = -$1;
  func COMPL W -> UnOp of V..W means
  it.S1 = -S1;
  existence
  proof
    thus ex U being UnOp of V..W st
    for S1 holds U.S1 = U(S1) from FUNCT_2:sch 4;
  end;
  uniqueness
  proof
    thus for U1,U2 being UnOp of V..W st
    (for S1 holds U1.S1 = U(S1)) & (for S1 holds U2.S1 = U(S1))
    holds U1 = U2 from UnOpEq;
  end;
  deffunc U(Element of V..W,Element of V..W) = $1 + $2;
  func ADD W -> BinOp of V..W means
  :Def17:
  it.(S1,S2) = S1 + S2;
  existence
  proof
    thus ex B being BinOp of V..W st
    for S1,S2 holds B.(S1,S2) = U(S1,S2) from BINOP_1:sch 4;
  end;
  uniqueness
  proof
    thus for B1,B2 being BinOp of V..W st
    (for S1,S2 holds B1.(S1,S2) = U(S1,S2)) &
    (for S1,S2 holds B2.(S1,S2) = U(S1,S2)) holds B1 = B2 from BINOP_2:sch 2;
  end;
end;

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

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

theorem
  a..W is Element of V.W;

definition
  let K,V,W,a;
  func a.W -> Element of V.W equals
  a..W;
  coherence;
end;

theorem Th15:
  for x being Element of V.W ex a st x = a.W
proof
  let x be Element of V.W;
  consider a such that
A1: x = a..W by Th12;
  take a;
  thus thesis by A1;
end;

theorem
  a1.W = a2.W iff a1 - a2 in W by Th11;

theorem Th17:
  a.W + b.W = (a+b).W & 0.(V.W) = (0.V).W
proof
  thus a.W + b.W = a..W + b..W by Def17
    .= (a+b).W by Def15;
  thus thesis;
end;

registration
  let K,V,W;
  cluster V.W -> Abelian add-associative right_zeroed right_complementable;
  coherence
  proof
    set G = V.W;
    hereby
      let x,y be Element of G;
      consider a being Vector of V such that
A1:   x = a.W by Th15;
      consider b being Vector of V such that
A2:   y = b.W by Th15;
      x+y = (a+b).W by A1,A2,Th17;
      hence x+y = y+x by A1,A2,Th17;
    end;
    hereby
      let x,y,z be Element of G;
      consider a being Vector of V such that
A3:   x = a.W by Th15;
      consider b being Vector of V such that
A4:   y = b.W by Th15;
      consider c being Vector of V such that
A5:   z = c.W by Th15;
A6:   x+y = (a+b).W by A3,A4,Th17;
A7:   y+z = (b+c).W by A4,A5,Th17;
      thus (x+y)+z = (a+b+c).W by A5,A6,Th17
        .= (a+(b+c)).W by RLVECT_1:def 3
        .= x+(y+z) by A3,A7,Th17;
    end;
    hereby
      let x be Element of G;
      consider a being Vector of V such that
A8:   x = a.W by Th15;
      0.G = (0.V).W;
      hence x+(0.G) = (a+0.V).W by A8,Th17
        .= x by A8,RLVECT_1:4;
    end;
    let x be Element of G;
    consider a being Vector of V such that
A9: x = a.W by Th15;
    consider b being Vector of V such that
A10: a + b = 0.V by ALGSTR_0:def 11;
    reconsider b9 = b.W as Element of G;
    take b9;
    thus x+b9 = (0.V).W by A9,A10,Th17
      .= 0.G;
  end;
end;

reserve S for Element of V.W;

definition
  let K,V,W,r,S;
  func r*S -> Element of V.W means
  :Def20:
  S = a.W implies it = (r*a).W;
  existence
  proof
    consider a1 such that
A1: S = a1.W by Th15;
A2: now
      let a;
      assume S = a.W;
      then a - a1 in W by A1,Th11;
      then r*(a-a1) in W by VECTSP_4:21;
      then r*a - r*a1 in W by VECTSP_1:23;
      hence (r*a).W = (r*a1).W by Th11;
    end;
    take (r*a1).W;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let S1,S2 be Element of V.W such that
A3: S = a.W implies S1 = (r*a).W and
A4: S = a.W implies S2 = (r*a).W;
    consider a1 such that
A5: S = a1.W by Th15;
    thus S1 = (r*a1).W by A3,A5
      .= S2 by A4,A5;
  end;
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
  :Def21:
  it.(r,S) = r*S;
  existence
  proof
    deffunc U(Scalar of K,Element of V.W) = $1 * $2;
    consider F being Function of [:the carrier of K,the carrier of V.W:],
    the carrier of V.W such that
A1: F.(r,S) = U(r,S) from BINOP_1:sch 4;
    take F;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let F,G be Function of [:the carrier of K,the carrier of V.W:],
    the carrier of V.W such that
A2: F.(r,S) = r*S and
A3: G.(r,S) = r*S;
    now
      let r,S;
      thus F.(r,S) = r*S by A2
        .= G.(r,S) by A3;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

begin

definition
  let K,V,W;
  func V/W -> strict VectSpStr over K equals
  VectSpStr(#the carrier of V.W,the addF of V.W,0.V.W,LMULT W#);
  coherence;
end;

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

theorem
  a.W is Vector of V/W;

theorem
  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
  a.W;
  coherence;
end;

theorem Th20:
  for x being Vector of V/W ex a st x = a/W
proof
  let x be Vector of V/W;
  consider a such that
A1: x = a.W by Th15;
  take a;
  thus thesis by A1;
end;

theorem
  a1/W = a2/W iff a1 - a2 in W by Th11;

theorem Th22:
  a/W + b/W = (a+b)/W & r*(a/W) = (r*a)/W
proof
  thus a/W + b/W = a.W + b.W .= (a+b)/W by Th17;
  thus r*(a/W) = (LMULT W).(r,a.W) by VECTSP_1:def 12
    .= r*(a.W qua Element of V.W) by Def21
    .= (r*a)/W by Def20;
end;

Lm2: V/W is Abelian add-associative right_zeroed right_complementable
proof
A1: for x,y,z be Element of V.W, x9,y9,z9 be Vector of V/W
  st x = x9 & y = y9 & z = z9 holds x + y = x9+ y9;
  thus V/W is Abelian
  proof
    let x,y be Vector of V/W;
    reconsider x9= x, y9= y as Element of V.W;
    thus x+y = x9+ y9 .= y + x by A1;
  end;
  hereby
    let x,y,z be Vector of V/W;
    reconsider x9= x, y9= y, z9= z as Element of V.W;
    thus (x+y)+z = (x9+ y9) + z9 .= x9+ (y9+ z9) by RLVECT_1:def 3
      .=
    x + (y + z);
  end;
  hereby
    let x be Vector of V/W;
    reconsider x9= x as Element of V.W;
    thus x+(0.(V/W)) = x9+ (0.(V.W)) .= x by RLVECT_1:4;
  end;
  let x be Vector of V/W;
  reconsider x9= x as Element of V.W;
  consider b being Element of V.W such that
A2: x9 + b = 0.(V.W) by ALGSTR_0:def 11;
  reconsider b9 = b as Vector of V/W;
  take b9;
  thus thesis by A2;
end;

theorem Th23:
  V/W is strict LeftMod of K
proof
  now
    let x,y be Scalar of K, v,w be Vector of V/W;
    consider a such that
A1: v = a/W by Th20;
    consider b such that
A2: w = b/W by Th20;
A3: (x*a)/W = x*v by A1,Th22;
A4: (x*b)/W = x*w by A2,Th22;
A5: (y*a)/W = y*v by A1,Th22;
    thus x*(v+w) = x*((a+b)/W) by A1,A2,Th22
      .= (x*(a+b))/W by Th22
      .= (x*a+x*b)/W by VECTSP_1:def 14
      .= x*v+x*w by A3,A4,Th22;
    thus (x+y)*v = ((x+y)*a)/W by A1,Th22
      .= (x*a+y*a)/W by VECTSP_1:def 15
      .= x*v+y*v by A3,A5,Th22;
    thus (x*y)*v = ((x*y)*a)/W by A1,Th22
      .= (x*(y*a))/W by VECTSP_1:def 16
      .= x*((y*a)/W) by Th22
      .= x*(y*v) by A1,Th22;
    thus 1_K*v = (1_K*a)/W by A1,Th22
      .= v by A1,VECTSP_1:def 17;
  end;
  hence thesis by Lm2,VECTSP_1:def 14,def 15,def 16,def 17;
end;

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