:: 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-2011 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
proof end;

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
proof end;

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
proof end;

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
proof end;

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] }
proof end;

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] }
proof end;

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] }
proof end;

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] }
proof end;

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] }
proof end;

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] )
proof end;

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

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
proof end;

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
proof end;

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

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 <> {}
proof end;

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 & A1 misses A2 holds
(Lin A1) /\ (Lin A2) = (0). V
proof end;

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 & A = A1 \/ A2 & A1 misses A2 holds
V is_the_direct_sum_of Lin A1, Lin A2
proof end;

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
proof end;
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
proof end;
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 Element of D;
existence
ex b1 being Element of D st b1 is strict
proof end;
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 & it = <:a:> );
existence
ex b1 being strict Subspace of V ex a being Vector of V st
( a <> 0. V & b1 = <:a:> )
proof end;
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 & 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
proof end;
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 )
proof end;
uniqueness
for b1, b2 being LINE_DOMAIN of V st ( for x being set holds
( x in b1 iff x is LINE of V ) ) & ( for x being set holds
( x in b2 iff x is LINE of V ) ) holds
b1 = b2
proof end;
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 & 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 & V is_the_direct_sum_of <:a:>,b1 )
proof end;
end;

:: deftheorem defines HIPERPLANE LMOD_7:def 5 :
for K being Ring
for V being LeftMod of K st not V is trivial & 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 & 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
proof end;
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 )
proof end;
uniqueness
for b1, b2 being HIPERPLANE_DOMAIN of V st ( for x being set holds
( x in b1 iff x is HIPERPLANE of V ) ) & ( for x being set holds
( x in b2 iff x is HIPERPLANE of V ) ) holds
b1 = b2
proof end;
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
canceled;

theorem :: LMOD_7:8
canceled;

theorem :: LMOD_7:9
canceled;

theorem :: LMOD_7:10
canceled;

theorem :: LMOD_7:11
canceled;

theorem :: LMOD_7:12
canceled;

theorem :: LMOD_7:13
canceled;

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

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

begin

definition
let K be Ring;
let V be LeftMod of K;
let A1, A2 be Subset of V;
func A1 + 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 & a2 in A2 & 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 & a2 in A2 & x = a1 + a2 ) )
proof end;
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 & a2 in A2 & x = a1 + a2 ) ) ) & ( for x being set holds
( x in b2 iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ) holds
b1 = b2
proof end;
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 & a2 in A2 & 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
proof end;
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:16
for K being Ring
for V being LeftMod of K
for A1, A2 being Subset of V st A1 <> {} & A1 c= A2 holds
for x being set st x is Vector of A1 holds
x is Vector of A2
proof end;

theorem Th17: :: LMOD_7:17
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 )
proof end;

theorem Th18: :: LMOD_7:18
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 )
proof end;

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
func V .. 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 )
proof end;
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 ) ) & ( for x being set holds
( x in b2 iff ex a being Vector of V st x = a + W ) ) holds
b1 = b2
proof end;
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;
cluster V .. W -> non empty ;
coherence
not V .. W is empty
proof end;
end;

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let a be Vector of V;
func a .. 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 Th19: :: LMOD_7:19
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
proof end;

theorem :: LMOD_7:20
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 Th18;

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
proof end;
uniqueness
for b1, b2 being Element of V .. W st ( for a being Vector of V st S1 = a .. W holds
b1 = (- a) .. W ) & ( for a being Vector of V st S1 = a .. W holds
b2 = (- a) .. W ) holds
b1 = b2
proof end;
let S2 be Element of V .. W;
func S1 + S2 -> Element of V .. W means :Def15: :: LMOD_7:def 15
 for a1, a2 being Vector of V st S1 = a1 .. W & 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 & S2 = a2 .. W holds
b1 = (a1 + a2) .. W
proof end;
uniqueness
for b1, b2 being Element of V .. W st ( for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
b1 = (a1 + a2) .. W ) & ( for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
b2 = (a1 + a2) .. W ) holds
b1 = b2
proof end;
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 & 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
proof end;
uniqueness
for b1, b2 being UnOp of (V .. W) st ( for S1 being Element of V .. W holds b1 . S1 = - S1 ) & ( for S1 being Element of V .. W holds b2 . S1 = - S1 ) holds
b1 = b2
proof end;
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
proof end;
uniqueness
for b1, b2 being BinOp of (V .. W) st ( for S1, S2 being Element of V .. W holds b1 . (S1,S2) = S1 + S2 ) & ( for S1, S2 being Element of V .. W holds b2 . (S1,S2) = S1 + S2 ) holds
b1 = b2
proof end;
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;
func V . 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;
cluster V . W -> non empty strict ;
coherence
not V . W is empty ;
end;

theorem :: LMOD_7:21
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;
func a . 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 Th22: :: LMOD_7:22
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
proof end;

theorem :: LMOD_7:23
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 Th18;

theorem Th24: :: LMOD_7:24
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 & 0. (V . W) = (0. V) . W )
proof end;

registration
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
cluster V . W -> strict right_complementable Abelian add-associative right_zeroed ;
coherence
( V . W is Abelian & V . W is add-associative & V . W is right_zeroed & V . W is right_complementable )
proof end;
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);
func r * 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
proof end;
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 ) & ( for a being Vector of V st S = a . W holds
b2 = (r * a) . W ) holds
b1 = b2
proof end;
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
proof end;
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 ) & ( for r being Scalar of K
for S being Element of (V . W) holds b2 . (r,S) = r * S ) holds
b1 = b2
proof end;
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;
func V / W -> strict VectSpStr of 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 of 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;
cluster V / W -> non empty strict ;
coherence
not V / W is empty ;
end;

theorem :: LMOD_7:25
canceled;

theorem :: LMOD_7:26
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:27
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;
func a / 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 Th28: :: LMOD_7:28
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
proof end;

theorem :: LMOD_7:29
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 Th18;

theorem Th30: :: LMOD_7:30
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 & r * (a / W) = (r * a) / W )
proof end;

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

theorem Th31: :: LMOD_7:31
for K being Ring
for V being LeftMod of K
for W being Subspace of V holds V / W is strict LeftMod of K
proof end;

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