:: 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


begin

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

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

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

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

scheme :: LMOD_7:sch 5
Fraenkel1Ex{ F1() ->  non empty set , F2() ->  non empty set , F3( set ) ->  Element of F2(), P1[ set ] } :
 ex S being Subset of F2() st S =  {  F3(x) where x is Element of F1() : P1[x]  }
proofend;

scheme :: LMOD_7:sch 6
Fr0{ F1() ->  non empty set , F2() ->  Element of F1(), P1[ set ] } :
 P1[F2()]
provided
A1: F2() in  {  a where a is Element of F1() : P1[a]  }
proofend;

scheme :: LMOD_7:sch 7
Fr1{ F1() ->  set , F2() ->  non empty set , F3() ->  Element of F2(), P1[ set ] } :
 ( F3() in F1() iff P1[F3()] )
provided
A1: F1() =  {  a where a is Element of F2() : P1[a]  }
proofend;

scheme :: LMOD_7:sch 8
Fr2{ F1() ->  set , F2() ->  non empty set , F3() ->  Element of F2(), P1[ set ] } :
 P1[F3()]
provided
A1: F3() in F1() and
A2: F1() =  {  a where a is Element of F2() : P1[a]  }
proofend;

scheme :: LMOD_7:sch 9
Fr3{ F1() ->  set , F2() ->  set , F3() ->  non empty set , P1[ set ] } :
 ( F1() in F2() iff ex a being Element of F3() st
( F1() = a & P1[a] ) )
provided
A1: F2() =  {  a where a is Element of F3() : P1[a]  }
proofend;

scheme :: LMOD_7:sch 10
Fr4{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  set , F4() ->  Element of F1(), F5( set ) ->  set , P1[ set , set ], P2[ set , set ] } :
 ( F4() in F5(F3()) iff for b being Element of F2() st b in F3() holds
P1[F4(),b] )
provided
A1: F5(F3()) =  {  a where a is Element of F1() : P2[a,F3()]  }  and
A2: ( P2[F4(),F3()] iff for b being Element of F2() st b in F3() holds
P1[F4(),b] )
proofend;

begin

Lm1:  for G being AbGroup
for a, b, c being Element of G holds
( - (a - b) = (- a) - (- b) & (a - b) + c = (a + c) - b )
proofend;

:: 1. Auxiliary theorems about free-modules
theorem Th1: :: LMOD_7:1
for K being Ring
for V being LeftMod of K
for A being Subset of V st not K is trivial & A is linearly-independent holds
not 0. V in A
proofend;

theorem Th2: :: LMOD_7:2
for K being Ring
for V being LeftMod of K
for a being Vector of V
for A being Subset of V
for l being Linear_Combination of A st not a in A holds
l . a = 0. K
proofend;

theorem :: LMOD_7:3
for K being Ring
for V being LeftMod of K
for A being Subset of V st K is trivial holds
( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )
proofend;

theorem Th4: :: LMOD_7:4
for K being Ring
for V being LeftMod of K st not V is trivial holds
for A being Subset of V st A is base holds
A <> {}
proofend;

theorem Th5: :: LMOD_7:5
for K being Ring
for V being LeftMod of K
for A1, A2 being Subset of V st A1 \/ A2 is linearly-independent &amp; A1 misses A2 holds
(Lin A1) /\ (Lin A2) = (0). V
proofend;

theorem Th6: :: LMOD_7:6
for K being Ring
for V being LeftMod of K
for A, A1, A2 being Subset of V st A is base &amp; A = A1 \/ A2 &amp; A1 misses A2 holds
V is_the_direct_sum_of Lin A1, Lin A2
proofend;

begin

definition
let K be Ring;
let V be LeftMod of K;
mode SUBMODULE_DOMAIN of V ->  non empty set  means :Def1: :: LMOD_7:def 1
 for x being set st x in it holds
x is strict Subspace of V;
existence
 ex b1 being non empty set st
for x being set st x in b1 holds
x is strict Subspace of V
proofend;
end;

:: deftheorem Def1 defines SUBMODULE_DOMAIN LMOD_7:def_1_:_
 for K being Ring
for V being LeftMod of K
for b3 being non empty set holds
( b3 is SUBMODULE_DOMAIN of V iff for x being set st x in b3 holds
x is strict Subspace of V );

definition
let K be Ring;
let V be LeftMod of K;
:: original:Subspaces
redefine func Submodules V ->  SUBMODULE_DOMAIN of V;
coherence
 Subspaces V is SUBMODULE_DOMAIN of V
proofend;
end;

definition
let K be Ring;
let V be LeftMod of K;
let D be SUBMODULE_DOMAIN of V;
:: original:Element
redefine mode Element of D ->  strict Subspace of V;
coherence
 for b1 being Element of D holds b1 is strict Subspace of V by Def1;
end;

registration
let K be Ring;
let V be LeftMod of K;
let D be SUBMODULE_DOMAIN of V;
cluster non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed for Element of D;
existence
 ex b1 being Element of D st b1 is strict
proofend;
end;

definition
let K be Ring;
let V be LeftMod of K;
assume A1: not V is trivial ;
mode LINE of V ->  strict Subspace of V means :: LMOD_7:def 2
 ex a being Vector of V st
( a <> 0. V &amp; it = <:a:> );
existence
 ex b1 being strict Subspace of V ex a being Vector of V st
( a <> 0. V &amp; b1 = <:a:> )
proofend;
end;

:: deftheorem  defines LINE LMOD_7:def_2_:_
 for K being Ring
for V being LeftMod of K st not V is trivial holds
for b3 being strict Subspace of V holds
( b3 is LINE of V iff ex a being Vector of V st
( a <> 0. V &amp; b3 = <:a:> ) );

definition
let K be Ring;
let V be LeftMod of K;
mode LINE_DOMAIN of V ->  non empty set  means :Def3: :: LMOD_7:def 3
 for x being set st x in it holds
x is LINE of V;
existence
 ex b1 being non empty set st
for x being set st x in b1 holds
x is LINE of V
proofend;
end;

:: deftheorem Def3 defines LINE_DOMAIN LMOD_7:def_3_:_
 for K being Ring
for V being LeftMod of K
for b3 being non empty set holds
( b3 is LINE_DOMAIN of V iff for x being set st x in b3 holds
x is LINE of V );

definition
let K be Ring;
let V be LeftMod of K;
func lines V ->  LINE_DOMAIN of V means :: LMOD_7:def 4
 for x being set holds
( x in it iff x is LINE of V );
existence
 ex b1 being LINE_DOMAIN of V st
for x being set holds
( x in b1 iff x is LINE of V )
proofend;
uniqueness
 for b1, b2 being LINE_DOMAIN of V st ( for x being set holds
( x in b1 iff x is LINE of V ) ) &amp; ( for x being set holds
( x in b2 iff x is LINE of V ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines lines LMOD_7:def_4_:_
 for K being Ring
for V being LeftMod of K
for b3 being LINE_DOMAIN of V holds
( b3 = lines V iff for x being set holds
( x in b3 iff x is LINE of V ) );

definition
let K be Ring;
let V be LeftMod of K;
let D be LINE_DOMAIN of V;
:: original:Element
redefine mode Element of D ->  LINE of V;
coherence
 for b1 being Element of D holds b1 is LINE of V by Def3;
end;

definition
let K be Ring;
let V be LeftMod of K;
assume that
A1: not V is trivial and
A2: V is free ;
mode HIPERPLANE of V ->  strict Subspace of V means :: LMOD_7:def 5
 ex a being Vector of V st
( a <> 0. V &amp; V is_the_direct_sum_of <:a:>,it );
existence
 ex b1 being strict Subspace of V ex a being Vector of V st
( a <> 0. V &amp; V is_the_direct_sum_of <:a:>,b1 )
proofend;
end;

:: deftheorem  defines HIPERPLANE LMOD_7:def_5_:_
 for K being Ring
for V being LeftMod of K st not V is trivial &amp; V is free holds
for b3 being strict Subspace of V holds
( b3 is HIPERPLANE of V iff ex a being Vector of V st
( a <> 0. V &amp; V is_the_direct_sum_of <:a:>,b3 ) );

definition
let K be Ring;
let V be LeftMod of K;
mode HIPERPLANE_DOMAIN of V ->  non empty set  means :Def6: :: LMOD_7:def 6
 for x being set st x in it holds
x is HIPERPLANE of V;
existence
 ex b1 being non empty set st
for x being set st x in b1 holds
x is HIPERPLANE of V
proofend;
end;

:: deftheorem Def6 defines HIPERPLANE_DOMAIN LMOD_7:def_6_:_
 for K being Ring
for V being LeftMod of K
for b3 being non empty set holds
( b3 is HIPERPLANE_DOMAIN of V iff for x being set st x in b3 holds
x is HIPERPLANE of V );

definition
let K be Ring;
let V be LeftMod of K;
func hiperplanes V ->  HIPERPLANE_DOMAIN of V means :: LMOD_7:def 7
 for x being set holds
( x in it iff x is HIPERPLANE of V );
existence
 ex b1 being HIPERPLANE_DOMAIN of V st
for x being set holds
( x in b1 iff x is HIPERPLANE of V )
proofend;
uniqueness
 for b1, b2 being HIPERPLANE_DOMAIN of V st ( for x being set holds
( x in b1 iff x is HIPERPLANE of V ) ) &amp; ( for x being set holds
( x in b2 iff x is HIPERPLANE of V ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines hiperplanes LMOD_7:def_7_:_
 for K being Ring
for V being LeftMod of K
for b3 being HIPERPLANE_DOMAIN of V holds
( b3 = hiperplanes V iff for x being set holds
( x in b3 iff x is HIPERPLANE of V ) );

definition
let K be Ring;
let V be LeftMod of K;
let D be HIPERPLANE_DOMAIN of V;
:: original:Element
redefine mode Element of D ->  HIPERPLANE of V;
coherence
 for b1 being Element of D holds b1 is HIPERPLANE of V by Def6;
end;

begin

definition
let K be Ring;
let V be LeftMod of K;
let Li be FinSequence of Submodules V;
func Sum Li ->  Element of Submodules V equals :: LMOD_7:def 8
(SubJoin V) $$ Li;
coherence
 (SubJoin V) $$ Li is Element of Submodules V ;
func /\ Li ->  Element of Submodules V equals :: LMOD_7:def 9
(SubMeet V) $$ Li;
coherence
 (SubMeet V) $$ Li is Element of Submodules V ;
end;

:: deftheorem  defines Sum LMOD_7:def_8_:_
 for K being Ring
for V being LeftMod of K
for Li being FinSequence of Submodules V holds Sum Li = (SubJoin V) $$ Li;

:: deftheorem  defines /\ LMOD_7:def_9_:_
 for K being Ring
for V being LeftMod of K
for Li being FinSequence of Submodules V holds /\ Li = (SubMeet V) $$ Li;

theorem :: LMOD_7:7
for K being Ring
for V being LeftMod of K holds
( SubJoin V is commutative &amp; SubJoin V is associative &amp; SubJoin V is having_a_unity &amp; (0). V = the_unity_wrt (SubJoin V) )
proofend;

theorem :: LMOD_7:8
for K being Ring
for V being LeftMod of K holds
( SubMeet V is commutative &amp; SubMeet V is associative &amp; SubMeet V is having_a_unity &amp; (Omega). V = the_unity_wrt (SubMeet V) )
proofend;

begin

definition
let K be Ring;
let V be LeftMod of K;
let A1, A2 be Subset of V;
funcA1 + A2 ->  Subset of V means :: LMOD_7:def 10
 for x being set holds
( x in it iff ex a1, a2 being Vector of V st
( a1 in A1 &amp; a2 in A2 &amp; x = a1 + a2 ) );
existence
 ex b1 being Subset of V st
for x being set holds
( x in b1 iff ex a1, a2 being Vector of V st
( a1 in A1 &amp; a2 in A2 &amp; x = a1 + a2 ) )
proofend;
uniqueness
 for b1, b2 being Subset of V st ( for x being set holds
( x in b1 iff ex a1, a2 being Vector of V st
( a1 in A1 &amp; a2 in A2 &amp; x = a1 + a2 ) ) ) &amp; ( for x being set holds
( x in b2 iff ex a1, a2 being Vector of V st
( a1 in A1 &amp; a2 in A2 &amp; x = a1 + a2 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines + LMOD_7:def_10_:_
 for K being Ring
for V being LeftMod of K
for A1, A2, b5 being Subset of V holds
( b5 = A1 + A2 iff for x being set holds
( x in b5 iff ex a1, a2 being Vector of V st
( a1 in A1 &amp; a2 in A2 &amp; x = a1 + a2 ) ) );

begin

definition
let K be Ring;
let V be LeftMod of K;
let A be Subset of V;
assume A1: A <> {} ;
mode Vector of A ->  Vector of V means :Def11: :: LMOD_7:def 11
it is Element of A;
existence
 ex b1 being Vector of V st b1 is Element of A
proofend;
end;

:: deftheorem Def11 defines Vector LMOD_7:def_11_:_
 for K being Ring
for V being LeftMod of K
for A being Subset of V st A <> {} holds
for b4 being Vector of V holds
( b4 is Vector of A iff b4 is Element of A );

theorem :: LMOD_7:9
for K being Ring
for V being LeftMod of K
for A1, A2 being Subset of V st A1 <> {} &amp; A1 c= A2 holds
for x being set st x is Vector of A1 holds
x is Vector of A2
proofend;

:: 6. Quotient modules
theorem Th10: :: LMOD_7:10
for K being Ring
for V being LeftMod of K
for a2, a1 being Vector of V
for W being Subspace of V holds
( a2 in a1 + W iff a1 - a2 in W )
proofend;

theorem Th11: :: LMOD_7:11
for K being Ring
for V being LeftMod of K
for a1, a2 being Vector of V
for W being Subspace of V holds
( a1 + W = a2 + W iff a1 - a2 in W )
proofend;

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
funcV .. W ->  set  means :Def12: :: LMOD_7:def 12
 for x being set holds
( x in it iff ex a being Vector of V st x = a + W );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex a being Vector of V st x = a + W )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex a being Vector of V st x = a + W ) ) &amp; ( for x being set holds
( x in b2 iff ex a being Vector of V st x = a + W ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines .. LMOD_7:def_12_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V
for b4 being set holds
( b4 = V .. W iff for x being set holds
( x in b4 iff ex a being Vector of V st x = a + W ) );

registration
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
clusterV .. W ->  non empty ;
coherence
 not V .. W is empty
proofend;
end;

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let a be Vector of V;
funca .. W ->  Element of V .. W equals :: LMOD_7:def 13
a + W;
coherence
 a + W is Element of V .. W by Def12;
end;

:: deftheorem  defines .. LMOD_7:def_13_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V
for a being Vector of V holds a .. W = a + W;

theorem Th12: :: LMOD_7:12
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for x being Element of V .. W ex a being Vector of V st x = a .. W
proofend;

theorem :: LMOD_7:13
for K being Ring
for V being LeftMod of K
for a1, a2 being Vector of V
for W being Subspace of V holds
( a1 .. W = a2 .. W iff a1 - a2 in W ) by Th11;

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let S1 be Element of V .. W;
func - S1 ->  Element of V .. W means :: LMOD_7:def 14
 for a being Vector of V st S1 = a .. W holds
it = (- a) .. W;
existence
 ex b1 being Element of V .. W st
for a being Vector of V st S1 = a .. W holds
b1 = (- a) .. W
proofend;
uniqueness
 for b1, b2 being Element of V .. W st ( for a being Vector of V st S1 = a .. W holds
b1 = (- a) .. W ) &amp; ( for a being Vector of V st S1 = a .. W holds
b2 = (- a) .. W ) holds
b1 = b2
proofend;
let S2 be Element of V .. W;
funcS1 + S2 ->  Element of V .. W means :Def15: :: LMOD_7:def 15
 for a1, a2 being Vector of V st S1 = a1 .. W &amp; S2 = a2 .. W holds
it = (a1 + a2) .. W;
existence
 ex b1 being Element of V .. W st
for a1, a2 being Vector of V st S1 = a1 .. W &amp; S2 = a2 .. W holds
b1 = (a1 + a2) .. W
proofend;
uniqueness
 for b1, b2 being Element of V .. W st ( for a1, a2 being Vector of V st S1 = a1 .. W &amp; S2 = a2 .. W holds
b1 = (a1 + a2) .. W ) &amp; ( for a1, a2 being Vector of V st S1 = a1 .. W &amp; S2 = a2 .. W holds
b2 = (a1 + a2) .. W ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines - LMOD_7:def_14_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V
for S1, b5 being Element of V .. W holds
( b5 = - S1 iff for a being Vector of V st S1 = a .. W holds
b5 = (- a) .. W );

:: deftheorem Def15 defines + LMOD_7:def_15_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V
for S1, S2, b6 being Element of V .. W holds
( b6 = S1 + S2 iff for a1, a2 being Vector of V st S1 = a1 .. W &amp; S2 = a2 .. W holds
b6 = (a1 + a2) .. W );

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
deffunc H1( Element of V .. W) ->  Element of V .. W = - $1;
func COMPL W ->  UnOp of (V .. W) means :: LMOD_7:def 16
 for S1 being Element of V .. W holds it . S1 = - S1;
existence
 ex b1 being UnOp of (V .. W) st
for S1 being Element of V .. W holds b1 . S1 = - S1
proofend;
uniqueness
 for b1, b2 being UnOp of (V .. W) st ( for S1 being Element of V .. W holds b1 . S1 = - S1 ) &amp; ( for S1 being Element of V .. W holds b2 . S1 = - S1 ) holds
b1 = b2
proofend;
deffunc H2( Element of V .. W, Element of V .. W) ->  Element of V .. W = $1 + $2;
func ADD W ->  BinOp of (V .. W) means :Def17: :: LMOD_7:def 17
 for S1, S2 being Element of V .. W holds it . (S1,S2) = S1 + S2;
existence
 ex b1 being BinOp of (V .. W) st
for S1, S2 being Element of V .. W holds b1 . (S1,S2) = S1 + S2
proofend;
uniqueness
 for b1, b2 being BinOp of (V .. W) st ( for S1, S2 being Element of V .. W holds b1 . (S1,S2) = S1 + S2 ) &amp; ( for S1, S2 being Element of V .. W holds b2 . (S1,S2) = S1 + S2 ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines COMPL LMOD_7:def_16_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V
for b4 being UnOp of (V .. W) holds
( b4 = COMPL W iff for S1 being Element of V .. W holds b4 . S1 = - S1 );

:: deftheorem Def17 defines ADD LMOD_7:def_17_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V
for b4 being BinOp of (V .. W) holds
( b4 = ADD W iff for S1, S2 being Element of V .. W holds b4 . (S1,S2) = S1 + S2 );

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
funcV . W ->  strict addLoopStr  equals :: LMOD_7:def 18
 addLoopStr(# (V .. W),(ADD W),((0. V) .. W) #);
coherence
 addLoopStr(# (V .. W),(ADD W),((0. V) .. W) #) is strict addLoopStr ;
end;

:: deftheorem  defines . LMOD_7:def_18_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V holds V . W = addLoopStr(# (V .. W),(ADD W),((0. V) .. W) #);

registration
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
clusterV . W ->  non empty strict ;
coherence
 not V . W is empty ;
end;

theorem :: LMOD_7:14
for K being Ring
for V being LeftMod of K
for a being Vector of V
for W being Subspace of V holds a .. W is Element of (V . W) ;

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let a be Vector of V;
funca . W ->  Element of (V . W) equals :: LMOD_7:def 19
a .. W;
coherence
 a .. W is Element of (V . W) ;
end;

:: deftheorem  defines . LMOD_7:def_19_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V
for a being Vector of V holds a . W = a .. W;

theorem Th15: :: LMOD_7:15
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for x being Element of (V . W) ex a being Vector of V st x = a . W
proofend;

theorem :: LMOD_7:16
for K being Ring
for V being LeftMod of K
for a1, a2 being Vector of V
for W being Subspace of V holds
( a1 . W = a2 . W iff a1 - a2 in W ) by Th11;

theorem Th17: :: LMOD_7:17
for K being Ring
for V being LeftMod of K
for a, b being Vector of V
for W being Subspace of V holds
( (a . W) + (b . W) = (a + b) . W &amp; 0. (V . W) = (0. V) . W )
proofend;

registration
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
clusterV . W ->  strict right_complementable Abelian add-associative right_zeroed ;
coherence
 ( V . W is Abelian &amp; V . W is add-associative &amp; V . W is right_zeroed &amp; V . W is right_complementable )
proofend;
end;

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let r be Scalar of K;
let S be Element of (V . W);
funcr * S ->  Element of (V . W) means :Def20: :: LMOD_7:def 20
 for a being Vector of V st S = a . W holds
it = (r * a) . W;
existence
 ex b1 being Element of (V . W) st
for a being Vector of V st S = a . W holds
b1 = (r * a) . W
proofend;
uniqueness
 for b1, b2 being Element of (V . W) st ( for a being Vector of V st S = a . W holds
b1 = (r * a) . W ) &amp; ( for a being Vector of V st S = a . W holds
b2 = (r * a) . W ) holds
b1 = b2
proofend;
end;

:: deftheorem Def20 defines * LMOD_7:def_20_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V
for r being Scalar of K
for S, b6 being Element of (V . W) holds
( b6 = r * S iff for a being Vector of V st S = a . W holds
b6 = (r * a) . W );

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
func LMULT W ->  Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W) means :Def21: :: LMOD_7:def 21
 for r being Scalar of K
for S being Element of (V . W) holds it . (r,S) = r * S;
existence
 ex b1 being Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W) st
for r being Scalar of K
for S being Element of (V . W) holds b1 . (r,S) = r * S
proofend;
uniqueness
 for b1, b2 being Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W) st ( for r being Scalar of K
for S being Element of (V . W) holds b1 . (r,S) = r * S ) &amp; ( for r being Scalar of K
for S being Element of (V . W) holds b2 . (r,S) = r * S ) holds
b1 = b2
proofend;
end;

:: deftheorem Def21 defines LMULT LMOD_7:def_21_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V
for b4 being Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W) holds
( b4 = LMULT W iff for r being Scalar of K
for S being Element of (V . W) holds b4 . (r,S) = r * S );

begin

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
funcV / W ->  strict VectSpStr over K equals :: LMOD_7:def 22
 VectSpStr(# the carrier of (V . W), the addF of (V . W),((0. V) . W),(LMULT W) #);
coherence
 VectSpStr(# the carrier of (V . W), the addF of (V . W),((0. V) . W),(LMULT W) #) is strict VectSpStr over K ;
end;

:: deftheorem  defines / LMOD_7:def_22_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V holds V / W = VectSpStr(# the carrier of (V . W), the addF of (V . W),((0. V) . W),(LMULT W) #);

registration
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
clusterV / W ->  non empty strict ;
coherence
 not V / W is empty ;
end;

theorem :: LMOD_7:18
for K being Ring
for V being LeftMod of K
for a being Vector of V
for W being Subspace of V holds a . W is Vector of (V / W) ;

theorem :: LMOD_7:19
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for x being Vector of (V / W) holds x is Element of (V . W) ;

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let a be Vector of V;
funca / W ->  Vector of (V / W) equals :: LMOD_7:def 23
a . W;
coherence
 a . W is Vector of (V / W) ;
end;

:: deftheorem  defines / LMOD_7:def_23_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V
for a being Vector of V holds a / W = a . W;

theorem Th20: :: LMOD_7:20
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for x being Vector of (V / W) ex a being Vector of V st x = a / W
proofend;

theorem :: LMOD_7:21
for K being Ring
for V being LeftMod of K
for a1, a2 being Vector of V
for W being Subspace of V holds
( a1 / W = a2 / W iff a1 - a2 in W ) by Th11;

theorem Th22: :: LMOD_7:22
for K being Ring
for r being Scalar of K
for V being LeftMod of K
for a, b being Vector of V
for W being Subspace of V holds
( (a / W) + (b / W) = (a + b) / W &amp; r * (a / W) = (r * a) / W )
proofend;

Lm2:  for K being Ring
for V being LeftMod of K
for W being Subspace of V holds
( V / W is Abelian &amp; V / W is add-associative &amp; V / W is right_zeroed &amp; V / W is right_complementable )
proofend;

theorem Th23: :: LMOD_7:23
for K being Ring
for V being LeftMod of K
for W being Subspace of V holds V / W is strict LeftMod of K
proofend;

registration
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
clusterV / W ->  strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( V / W is vector-distributive &amp; V / W is scalar-distributive &amp; V / W is scalar-associative &amp; V / W is scalar-unital ) by Th23;
end;