:: LMOD_7 semantic presentation

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
let X1, X2 be Element of F1(); ::_thesis: ( ( for x being set holds
( x in X1 iff P1[x] ) ) & ( for x being set holds
( x in X2 iff P1[x] ) ) implies X1 = X2 )
assume that
A1: for x being set holds
( x in X1 iff P1[x] ) and
A2: for x being set holds
( x in X2 iff P1[x] ) ; ::_thesis: X1 = X2
now__::_thesis:_for_x_being_set_holds_
(_x_in_X1_iff_x_in_X2_)
let x be set ; ::_thesis: ( x in X1 iff x in X2 )
 ( x in X1 iff P1[x] ) by A1;
hence  ( x in X1 iff x in X2 ) by A2; ::_thesis: verum
end;
hence  X1 = X2 by TARSKI:1; ::_thesis: verum
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
let f1, f2 be UnOp of F1(); ::_thesis: ( ( for a being Element of F1() holds f1 . a = F2(a) ) & ( for a being Element of F1() holds f2 . a = F2(a) ) implies f1 = f2 )
assume that
A1: for a being Element of F1() holds f1 . a = F2(a) and
A2: for a being Element of F1() holds f2 . a = F2(a) ; ::_thesis: f1 = f2
now__::_thesis:_for_a_being_Element_of_F1()_holds_f1_._a_=_f2_._a
let a be Element of F1(); ::_thesis: f1 . a = f2 . a
thus f1 . a = F2(a) by A1
.= f2 . a by A2 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
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
let f1, f2 be TriOp of F1(); ::_thesis: ( ( 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) ) implies f1 = f2 )
assume that
A1: for a, b, c being Element of F1() holds f1 . (a,b,c) = F2(a,b,c) and
A2: for a, b, c being Element of F1() holds f2 . (a,b,c) = F2(a,b,c) ; ::_thesis: f1 = f2
now__::_thesis:_for_a,_b,_c_being_Element_of_F1()_holds_f1_._(a,b,c)_=_f2_._(a,b,c)
let a, b, c be Element of F1(); ::_thesis: f1 . (a,b,c) = f2 . (a,b,c)
thus f1 . (a,b,c) = F2(a,b,c) by A1
.= f2 . (a,b,c) by A2 ; ::_thesis: verum
end;
hence  f1 = f2 by MULTOP_1:3; ::_thesis: verum
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
let f1, f2 be QuaOp of F1(); ::_thesis: ( ( 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) ) implies f1 = f2 )
assume that
A1: for a, b, c, d being Element of F1() holds f1 . (a,b,c,d) = F2(a,b,c,d) and
A2: for a, b, c, d being Element of F1() holds f2 . (a,b,c,d) = F2(a,b,c,d) ; ::_thesis: f1 = f2
now__::_thesis:_for_a,_b,_c,_d_being_Element_of_F1()_holds_f1_._(a,b,c,d)_=_f2_._(a,b,c,d)
let a, b, c, d be Element of F1(); ::_thesis: f1 . (a,b,c,d) = f2 . (a,b,c,d)
thus f1 . (a,b,c,d) = F2(a,b,c,d) by A1
.= f2 . (a,b,c,d) by A2 ; ::_thesis: verum
end;
hence  f1 = f2 by MULTOP_1:6; ::_thesis: verum
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
reconsider S =  {  F3(x) where x is Element of F1() : P1[x]  }  as Subset of F2() from DOMAIN_1:sch_8();
take  S ; ::_thesis: S =  {  F3(x) where x is Element of F1() : P1[x]  }
thus  S =  {  F3(x) where x is Element of F1() : P1[x]  }  ; ::_thesis: verum
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
 ex a being Element of F1() st
( F2() = a & P1[a] ) by A1;
hence  P1[F2()] ; ::_thesis: verum
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
thus  ( F3() in F1() implies P1[F3()] ) ::_thesis: ( P1[F3()] implies F3() in F1() )
proof
assume  F3() in F1() ; ::_thesis: P1[F3()]
then A2: F3() in  {  a where a is Element of F2() : P1[a]  }  by A1;
thus  P1[F3()] from LMOD_7:sch_6(A2); ::_thesis: verum
end;
assume  P1[F3()] ; ::_thesis: F3() in F1()
hence  F3() in F1() by A1; ::_thesis: verum
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
A3: F3() in  {  a where a is Element of F2() : P1[a]  }  by A1, A2;
thus  P1[F3()] from LMOD_7:sch_6(A3); ::_thesis: verum
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
thus  ( F1() in F2() iff ex a being Element of F3() st
( F1() = a & P1[a] ) ) by A1; ::_thesis: verum
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
thus  ( F4() in F5(F3()) implies for b being Element of F2() st b in F3() holds
P1[F4(),b] ) ::_thesis: ( ( for b being Element of F2() st b in F3() holds
P1[F4(),b] ) implies F4() in F5(F3()) )
proof
defpred S1[ set ] means P2[$1,F3()];
assume  F4() in F5(F3()) ; ::_thesis: for b being Element of F2() st b in F3() holds
P1[F4(),b]
then A3: F4() in  {  a where a is Element of F1() : S1[a]  }  by A1;
 S1[F4()] from LMOD_7:sch_6(A3);
hence  for b being Element of F2() st b in F3() holds
P1[F4(),b] by A2; ::_thesis: verum
end;
assume  for b being Element of F2() st b in F3() holds
P1[F4(),b] ; ::_thesis: F4() in F5(F3())
hence  F4() in F5(F3()) by A1, A2; ::_thesis: verum
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
let G be AbGroup; ::_thesis: for a, b, c being Element of G holds
( - (a - b) = (- a) - (- b) & (a - b) + c = (a + c) - b )
let a, b, c be Element of G; ::_thesis: ( - (a - b) = (- a) - (- b) & (a - b) + c = (a + c) - b )
thus  - (a - b) = (- a) + b by VECTSP_1:17
.= (- a) - (- b) by RLVECT_1:17 ; ::_thesis: (a - b) + c = (a + c) - b
thus  (a - b) + c = (a + c) - b by RLVECT_1:def_3; ::_thesis: verum
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
let K be Ring; ::_thesis: 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
let V be LeftMod of K; ::_thesis: for A being Subset of V st not K is trivial & A is linearly-independent holds
not 0. V in A
let A be Subset of V; ::_thesis: ( not K is trivial & A is linearly-independent implies not 0. V in A )
assume that
A1: not K is trivial and
A2: A is linearly-independent ; ::_thesis: not 0. V in A
 0. K <> 1_ K by A1, LMOD_6:def_1;
hence  not 0. V in A by A2, LMOD_5:2; ::_thesis: verum
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
let K be Ring; ::_thesis: 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
let V be LeftMod of K; ::_thesis: 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
let a be Vector of V; ::_thesis: for A being Subset of V
for l being Linear_Combination of A st not a in A holds
l . a = 0. K
let A be Subset of V; ::_thesis: for l being Linear_Combination of A st not a in A holds
l . a = 0. K
let l be Linear_Combination of A; ::_thesis: ( not a in A implies l . a = 0. K )
assume A1: not a in A ; ::_thesis: l . a = 0. K
 Carrier l c= A by VECTSP_6:def_4;
then  not a in Carrier l by A1;
hence  l . a = 0. K by VECTSP_6:2; ::_thesis: verum
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
let K be Ring; ::_thesis: 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 )
let V be LeftMod of K; ::_thesis: 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 )
let A be Subset of V; ::_thesis: ( K is trivial implies ( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial ) )
assume A1: K is trivial ; ::_thesis: ( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )
thus A2: for l being Linear_Combination of A holds Carrier l = {} ::_thesis: Lin A is trivial
proof
let l be Linear_Combination of A; ::_thesis: Carrier l = {}
assume A3: Carrier l <> {} ; ::_thesis: contradiction
set x = the Element of Carrier l;
 ex a being Vector of V st
( the Element of Carrier l = a & l . a <> 0. K ) by A3, VECTSP_6:1;
hence  contradiction by A1, LMOD_6:5; ::_thesis: verum
end;
now__::_thesis:_for_a_being_Vector_of_(Lin_A)_holds_a_=_0._(Lin_A)
let a be Vector of (Lin A); ::_thesis: a = 0. (Lin A)
 a in Lin A by RLVECT_1:1;
then consider l being Linear_Combination of A 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; ::_thesis: verum
end;
hence  Lin A is trivial by STRUCT_0:def_18; ::_thesis: verum
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
let K be Ring; ::_thesis: for V being LeftMod of K st not V is trivial holds
for A being Subset of V st A is base holds
A <> {}
let V be LeftMod of K; ::_thesis: ( not V is trivial implies for A being Subset of V st A is base holds
A <> {} )
assume A1: not V is trivial ; ::_thesis: for A being Subset of V st A is base holds
A <> {}
let A be Subset of V; ::_thesis: ( A is base implies A <> {} )
assume that
A2: A is base and
A3: A = {} ; ::_thesis: contradiction
A4: A = {} the carrier of V by A3;
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = Lin A by A2, MOD_3:def_2
.= (0). V by A4, MOD_3:6 ;
hence  contradiction by A1, LMOD_6:7; ::_thesis: verum
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
let K be Ring; ::_thesis: 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
let V be LeftMod of K; ::_thesis: for A1, A2 being Subset of V st A1 \/ A2 is linearly-independent & A1 misses A2 holds
(Lin A1) /\ (Lin A2) = (0). V
let A1, A2 be Subset of V; ::_thesis: ( A1 \/ A2 is linearly-independent & A1 misses A2 implies (Lin A1) /\ (Lin A2) = (0). V )
assume that
A1: A1 \/ A2 is linearly-independent and
A2: A1 /\ A2 = {} ; :: according to XBOOLE_0:def_7 ::_thesis: (Lin A1) /\ (Lin A2) = (0). V
reconsider P = (Lin A1) /\ (Lin A2) as strict Subspace of V ;
set Z = the carrier of P;
A3: the carrier of P = the carrier of (Lin A1) /\ the carrier of (Lin A2) by VECTSP_5:def_2;
A4: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_P_holds_
x_=_0._V
let x be set ; ::_thesis: ( x in the carrier of P implies x = 0. V )
assume A5: x in the carrier of P ; ::_thesis: x = 0. V
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 <> {} ; ::_thesis: contradiction
set x = the Element of Carrier l1;
consider b being Vector of V such that
A16: the Element of Carrier l1 = 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; ::_thesis: verum
end;
hence  x = 0. V by A10, VECTSP_6:19; ::_thesis: verum
end;
 0. V in (Lin A1) /\ (Lin A2) by VECTSP_4:17;
then  for x being set holds
( x in the carrier of P iff x = 0. V ) by A4, STRUCT_0:def_5;
then  the carrier of P = {(0. V)} by TARSKI:def_1;
hence  (Lin A1) /\ (Lin A2) = (0). V by VECTSP_4:def_3; ::_thesis: verum
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
let K be Ring; ::_thesis: 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
let V be LeftMod of K; ::_thesis: 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
let A, A1, A2 be Subset of V; ::_thesis: ( A is base & A = A1 \/ A2 & A1 misses A2 implies V is_the_direct_sum_of Lin A1, Lin A2 )
assume that
A1: A is base and
A2: A = A1 \/ A2 and
A3: A1 misses A2 ; ::_thesis: V is_the_direct_sum_of Lin A1, Lin A2
set W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #);
A4: A is linearly-independent by A1, MOD_3:def_2;
 Lin A = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by A1, MOD_3:def_2;
then A5: VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (Lin A1) + (Lin A2) by A2, MOD_3:12;
 (Lin A1) /\ (Lin A2) = (0). V by A2, A3, A4, Th5;
hence  V is_the_direct_sum_of Lin A1, Lin A2 by A5, VECTSP_5:def_4; ::_thesis: verum
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
set a = the strict Subspace of V;
set D = { the strict Subspace of V};
take  { the strict Subspace of V} ; ::_thesis: for x being set st x in { the strict Subspace of V} holds
x is strict Subspace of V
thus  for x being set st x in { the strict Subspace of V} holds
x is strict Subspace of V by TARSKI:def_1; ::_thesis: verum
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
now__::_thesis:_for_x_being_set_st_x_in_Submodules_V_holds_
x_is_strict_Subspace_of_V
let x be set ; ::_thesis: ( x in Submodules V implies x is strict Subspace of V )
assume  x in Submodules V ; ::_thesis: x is strict Subspace of V
then  ex W being strict Subspace of V st W = x by VECTSP_5:def_3;
hence  x is strict Subspace of V ; ::_thesis: verum
end;
hence  Subspaces V is SUBMODULE_DOMAIN of V by Def1; ::_thesis: verum
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 for Element of D;
existence
 ex b1 being Element of D st b1 is strict
proof
set x = the Element of D;
take  the Element of D ; ::_thesis: the Element of D is strict
thus  the Element of D is strict ; ::_thesis: verum
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
consider a being Vector of V such that
A2: a <> 0. V by A1, STRUCT_0:def_18;
take  <:a:> ; ::_thesis: ex a being Vector of V st
( a <> 0. V & <:a:> = <:a:> )
thus  ex a being Vector of V st
( a <> 0. V & <:a:> = <:a:> ) by A2; ::_thesis: verum
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
set a = the LINE of V;
set D = { the LINE of V};
take  { the LINE of V} ; ::_thesis: for x being set st x in { the LINE of V} holds
x is LINE of V
thus  for x being set st x in { the LINE of V} holds
x is LINE of V by TARSKI:def_1; ::_thesis: verum
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
set D =  {  a where a is Element of Submodules V : a is LINE of V  }  ;
set a1 = the LINE of V;
reconsider a2 = the LINE of V as Element of Submodules V by VECTSP_5:def_3;
 a2 in  {  a where a is Element of Submodules V : a is LINE of V  }  ;
then reconsider D =  {  a where a is Element of Submodules V : a is LINE of V  }  as non empty set ;
A1: now__::_thesis:_for_x_being_set_st_x_in_D_holds_
x_is_LINE_of_V
let x be set ; ::_thesis: ( x in D implies x is LINE of V )
assume  x in D ; ::_thesis: x is LINE of V
then  ex a being Element of Submodules V st
( x = a & a is LINE of V ) ;
hence  x is LINE of V ; ::_thesis: verum
end;
then reconsider D9 = D as LINE_DOMAIN of V by Def3;
take  D9 ; ::_thesis: for x being set holds
( x in D9 iff x is LINE of V )
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_D9_implies_x_is_LINE_of_V_)_&_(_x_is_LINE_of_V_implies_x_in_D9_)_)
let x be set ; ::_thesis: ( ( x in D9 implies x is LINE of V ) & ( x is LINE of V implies x in D9 ) )
thus  ( x in D9 implies x is LINE of V ) by A1; ::_thesis: ( x is LINE of V implies x in D9 )
thus  ( x is LINE of V implies x in D9 ) ::_thesis: verum
proof
assume A2: x is LINE of V ; ::_thesis: x in D9
then reconsider x1 = x as Element of Submodules V by VECTSP_5:def_3;
 x1 in D by A2;
hence  x in D9 ; ::_thesis: verum
end;
end;
hence  for x being set holds
( x in D9 iff x is LINE of V ) ; ::_thesis: verum
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
let D1, D2 be LINE_DOMAIN of V; ::_thesis: ( ( for x being set holds
( x in D1 iff x is LINE of V ) ) & ( for x being set holds
( x in D2 iff x is LINE of V ) ) implies D1 = D2 )
assume that
A3: for x being set holds
( x in D1 iff x is LINE of V ) and
A4: for x being set holds
( x in D2 iff x is LINE of V ) ; ::_thesis: D1 = D2
now__::_thesis:_for_x_being_set_holds_
(_x_in_D1_iff_x_in_D2_)
let x be set ; ::_thesis: ( x in D1 iff x in D2 )
 ( x in D1 iff x is LINE of V ) by A3;
hence  ( x in D1 iff x in D2 ) by A4; ::_thesis: verum
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
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
consider A being Subset of V such that
A3: A is base by A2, MOD_3:def_3;
reconsider A = 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 = the Element of A as Vector of V by A5, TARSKI:def_3;
reconsider A1 = {a} as Subset of V ;
set A2 = A \ A1;
set H = Lin (A \ A1);
 A1 c= A by A5, ZFMISC_1:31;
then A6: A = A1 \/ (A \ A1) by XBOOLE_1:45;
 A1 misses A \ A1 by XBOOLE_1:79;
then A7: V is_the_direct_sum_of Lin A1, Lin (A \ A1) by A3, A6, Th6;
A8: ex a being Vector of V st
( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) )
proof
take  a ; ::_thesis: ( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) )
thus  ( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) ) by A1, A4, A5, A7, Th1, LMOD_6:6, LMOD_6:def_4; ::_thesis: verum
end;
take  Lin (A \ A1) ; ::_thesis: ex a being Vector of V st
( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) )
thus  ex a being Vector of V st
( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) ) by A8; ::_thesis: verum
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
set a = the HIPERPLANE of V;
set D = { the HIPERPLANE of V};
take  { the HIPERPLANE of V} ; ::_thesis: for x being set st x in { the HIPERPLANE of V} holds
x is HIPERPLANE of V
thus  for x being set st x in { the HIPERPLANE of V} holds
x is HIPERPLANE of V by TARSKI:def_1; ::_thesis: verum
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
set D =  {  a where a is Element of Submodules V : a is HIPERPLANE of V  }  ;
set a1 = the HIPERPLANE of V;
reconsider a2 = the HIPERPLANE of V as Element of Submodules V by VECTSP_5:def_3;
 a2 in  {  a where a is Element of Submodules V : a is HIPERPLANE of V  }  ;
then reconsider D =  {  a where a is Element of Submodules V : a is HIPERPLANE of V  }  as non empty set ;
A1: now__::_thesis:_for_x_being_set_st_x_in_D_holds_
x_is_HIPERPLANE_of_V
let x be set ; ::_thesis: ( x in D implies x is HIPERPLANE of V )
assume  x in D ; ::_thesis: x is HIPERPLANE of V
then  ex a being Element of Submodules V st
( x = a & a is HIPERPLANE of V ) ;
hence  x is HIPERPLANE of V ; ::_thesis: verum
end;
then reconsider D9 = D as HIPERPLANE_DOMAIN of V by Def6;
take  D9 ; ::_thesis: for x being set holds
( x in D9 iff x is HIPERPLANE of V )
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_D9_implies_x_is_HIPERPLANE_of_V_)_&_(_x_is_HIPERPLANE_of_V_implies_x_in_D9_)_)
let x be set ; ::_thesis: ( ( x in D9 implies x is HIPERPLANE of V ) & ( x is HIPERPLANE of V implies x in D9 ) )
thus  ( x in D9 implies x is HIPERPLANE of V ) by A1; ::_thesis: ( x is HIPERPLANE of V implies x in D9 )
thus  ( x is HIPERPLANE of V implies x in D9 ) ::_thesis: verum
proof
assume  x is HIPERPLANE of V ; ::_thesis: x in D9
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  x in D9 ; ::_thesis: verum
end;
end;
hence  for x being set holds
( x in D9 iff x is HIPERPLANE of V ) ; ::_thesis: verum
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
let D1, D2 be HIPERPLANE_DOMAIN of V; ::_thesis: ( ( for x being set holds
( x in D1 iff x is HIPERPLANE of V ) ) & ( for x being set holds
( x in D2 iff x is HIPERPLANE of V ) ) implies D1 = D2 )
assume that
A2: for x being set holds
( x in D1 iff x is HIPERPLANE of V ) and
A3: for x being set holds
( x in D2 iff x is HIPERPLANE of V ) ; ::_thesis: D1 = D2
now__::_thesis:_for_x_being_set_holds_
(_x_in_D1_iff_x_in_D2_)
let x be set ; ::_thesis: ( x in D1 iff x in D2 )
 ( x in D1 iff x is HIPERPLANE of V ) by A2;
hence  ( x in D1 iff x in D2 ) by A3; ::_thesis: verum
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
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
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
let K be Ring; ::_thesis: 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) )
let V be LeftMod of K; ::_thesis: ( SubJoin V is commutative & SubJoin V is associative & SubJoin V is having_a_unity & (0). V = the_unity_wrt (SubJoin V) )
set S0 = Submodules V;
set S1 = SubJoin V;
reconsider L = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) as Lattice by VECTSP_5:57;
 SubJoin V = the L_join of L ;
hence  ( SubJoin V is commutative & SubJoin V is associative ) ; ::_thesis: ( SubJoin V is having_a_unity & (0). V = the_unity_wrt (SubJoin V) )
set e = (0). V;
reconsider e9 = @ ((0). V) as Element of Submodules V ;
A1: e9 = (0). V by LMOD_6:def_2;
now__::_thesis:_for_a9_being_Element_of_Submodules_V_holds_
(_(SubJoin_V)_._(e9,a9)_=_a9_&_(SubJoin_V)_._(a9,e9)_=_a9_)
let a9 be Element of Submodules V; ::_thesis: ( (SubJoin V) . (e9,a9) = a9 & (SubJoin V) . (a9,e9) = a9 )
reconsider b = a9 as Element of Submodules V ;
reconsider a = b as strict Subspace of V ;
thus (SubJoin V) . (e9,a9) = ((0). V) + a by A1, VECTSP_5:def_7
.= a9 by VECTSP_5:9 ; ::_thesis: (SubJoin V) . (a9,e9) = a9
thus (SubJoin V) . (a9,e9) = a + ((0). V) by A1, VECTSP_5:def_7
.= a9 by VECTSP_5:9 ; ::_thesis: verum
end;
then A2: e9 is_a_unity_wrt SubJoin V by BINOP_1:3;
hence  SubJoin V is having_a_unity by SETWISEO:def_2; ::_thesis: (0). V = the_unity_wrt (SubJoin V)
thus  (0). V = the_unity_wrt (SubJoin V) by A1, A2, BINOP_1:def_8; ::_thesis: verum
end;

theorem :: LMOD_7:8
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
let K be Ring; ::_thesis: 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) )
let V be LeftMod of K; ::_thesis: ( SubMeet V is commutative & SubMeet V is associative & SubMeet V is having_a_unity & (Omega). V = the_unity_wrt (SubMeet V) )
set S0 = Submodules V;
set S2 = SubMeet V;
reconsider L = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) as Lattice by VECTSP_5:57;
 SubMeet V = the L_meet of L ;
hence  ( SubMeet V is commutative & SubMeet V is associative ) ; ::_thesis: ( SubMeet V is having_a_unity & (Omega). V = the_unity_wrt (SubMeet V) )
set e = (Omega). V;
reconsider e9 = @ ((Omega). V) as Element of Submodules V ;
A1: e9 = (Omega). V by LMOD_6:def_2;
now__::_thesis:_for_a9_being_Element_of_Submodules_V_holds_
(_(SubMeet_V)_._(e9,a9)_=_a9_&_(SubMeet_V)_._(a9,e9)_=_a9_)
let a9 be Element of Submodules V; ::_thesis: ( (SubMeet V) . (e9,a9) = a9 & (SubMeet V) . (a9,e9) = a9 )
reconsider b = a9 as Element of Submodules V ;
reconsider a = b as strict Subspace of V ;
thus (SubMeet V) . (e9,a9) = ((Omega). V) /\ a by A1, VECTSP_5:def_8
.= a9 by VECTSP_5:21 ; ::_thesis: (SubMeet V) . (a9,e9) = a9
thus (SubMeet V) . (a9,e9) = a /\ ((Omega). V) by A1, VECTSP_5:def_8
.= a9 by VECTSP_5:21 ; ::_thesis: verum
end;
then A2: e9 is_a_unity_wrt SubMeet V by BINOP_1:3;
hence  SubMeet V is having_a_unity by SETWISEO:def_2; ::_thesis: (Omega). V = the_unity_wrt (SubMeet V)
thus  (Omega). V = the_unity_wrt (SubMeet V) by A1, A2, BINOP_1:def_8; ::_thesis: verum
end;

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 & 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
set S =  {  (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 )  }  ;
A1: now__::_thesis:_for_x_being_set_st_x_in__{__(a1_+_a2)_where_a1,_a2_is_Vector_of_V_:_(_a1_in_A1_&_a2_in_A2_)__}__holds_
ex_a1,_a2_being_Vector_of_V_st_
(_a1_in_A1_&_a2_in_A2_&_x_=_a1_+_a2_)
let x be set ; ::_thesis: ( x in  {  (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 )  }  implies ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) )
assume  x in  {  (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 )  }  ; ::_thesis: ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 )
then  ex a1, a2 being Vector of V st
( x = a1 + a2 & a1 in A1 & a2 in A2 ) ;
hence  ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in__{__(a1_+_a2)_where_a1,_a2_is_Vector_of_V_:_(_a1_in_A1_&_a2_in_A2_)__}__holds_
x_in_the_carrier_of_V
let x be set ; ::_thesis: ( x in  {  (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 )  }  implies x in the carrier of V )
assume  x in  {  (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 )  }  ; ::_thesis: x in the carrier of V
then  ex a1, a2 being Vector of V st
( x = a1 + a2 & a1 in A1 & a2 in A2 ) ;
hence  x in the carrier of V ; ::_thesis: verum
end;
then reconsider S9 =  {  (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 )  }  as Subset of V by TARSKI:def_3;
take  S9 ; ::_thesis: for x being set holds
( x in S9 iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) )
thus  for x being set holds
( x in S9 iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) by A1; ::_thesis: verum
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
let D1, D2 be Subset of V; ::_thesis: ( ( for x being set holds
( x in D1 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 D2 iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ) implies D1 = D2 )
assume that
A2: for x being set holds
( x in D1 iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) and
A3: for x being set holds
( x in D2 iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ; ::_thesis: D1 = D2
now__::_thesis:_for_x_being_set_holds_
(_x_in_D1_iff_x_in_D2_)
let x be set ; ::_thesis: ( x in D1 iff x in D2 )
 ( x in D1 iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) by A2;
hence  ( x in D1 iff x in D2 ) by A3; ::_thesis: verum
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
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
consider x being Element of V such that
A2: x in A by A1, SUBSET_1:4;
take  x ; ::_thesis: x is Element of A
thus  x is Element of A by A2; ::_thesis: verum
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:9
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
let K be Ring; ::_thesis: 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
let V be LeftMod of K; ::_thesis: 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
let A1, A2 be Subset of V; ::_thesis: ( A1 <> {} & A1 c= A2 implies for x being set st x is Vector of A1 holds
x is Vector of A2 )
assume that
A1: A1 <> {} and
A2: A1 c= A2 ; ::_thesis: for x being set st x is Vector of A1 holds
x is Vector of A2
let x be set ; ::_thesis: ( x is Vector of A1 implies x is Vector of A2 )
assume  x is Vector of A1 ; ::_thesis: x is Vector of A2
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  x is Vector of A2 by Def11; ::_thesis: verum
end;

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 )
proof
let K be Ring; ::_thesis: 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 )
let V be LeftMod of K; ::_thesis: for a2, a1 being Vector of V
for W being Subspace of V holds
( a2 in a1 + W iff a1 - a2 in W )
let a2, a1 be Vector of V; ::_thesis: for W being Subspace of V holds
( a2 in a1 + W iff a1 - a2 in W )
let W be Subspace of V; ::_thesis: ( a2 in a1 + W iff a1 - a2 in W )
a1 - (a1 - a2) = (a1 - a1) + a2 by RLVECT_1:29
.= (0. V) + a2 by VECTSP_1:19
.= a2 by RLVECT_1:def_4 ;
hence  ( a2 in a1 + W iff a1 - a2 in W ) by VECTSP_4:61; ::_thesis: verum
end;

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 )
proof
let K be Ring; ::_thesis: 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 )
let V be LeftMod of K; ::_thesis: for a1, a2 being Vector of V
for W being Subspace of V holds
( a1 + W = a2 + W iff a1 - a2 in W )
let a1, a2 be Vector of V; ::_thesis: for W being Subspace of V holds
( a1 + W = a2 + W iff a1 - a2 in W )
let W be Subspace of V; ::_thesis: ( a1 + W = a2 + W iff a1 - a2 in W )
 ( a2 in a1 + W iff a1 + W = a2 + W ) by VECTSP_4:55;
hence  ( a1 + W = a2 + W iff a1 - a2 in W ) by Th10; ::_thesis: verum
end;

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 )
proof
take   {  (a + W) where a is Vector of V : verum  }  ; ::_thesis: for x being set holds
( x in  {  (a + W) where a is Vector of V : verum  }  iff ex a being Vector of V st x = a + W )
thus  for x being set holds
( x in  {  (a + W) where a is Vector of V : verum  }  iff ex a being Vector of V st x = a + W ) ; ::_thesis: verum
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
defpred S1[ set ] means  ex a being Vector of V st $1 = a + W;
thus  for S1, S2 being set st ( for x being set holds
( x in S1 iff S1[x] ) ) & ( for x being set holds
( x in S2 iff S1[x] ) ) holds
S1 = S2 from XBOOLE_0:sch_3(); ::_thesis: verum
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;
clusterV .. W ->  non empty ;
coherence
 not V .. W is empty
proof
 for a being Vector of V holds a + W in V .. W by Def12;
hence  not V .. W is empty ; ::_thesis: verum
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;
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
proof
let K be Ring; ::_thesis: 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
let V be LeftMod of K; ::_thesis: for W being Subspace of V
for x being Element of V .. W ex a being Vector of V st x = a .. W
let W be Subspace of V; ::_thesis: for x being Element of V .. W ex a being Vector of V st x = a .. W
let x be Element of V .. W; ::_thesis: ex a being Vector of V st x = a .. W
consider a being Vector of V such that
A1: x = a + W by Def12;
take  a ; ::_thesis: x = a .. W
thus  x = a .. W by A1; ::_thesis: verum
end;

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
proof
consider a1 being Vector of V such that
A1: S1 = a1 .. W by Th12;
A2: now__::_thesis:_for_a_being_Vector_of_V_st_S1_=_a_.._W_holds_
(-_a1)_.._W_=_(-_a)_.._W
let a be Vector of V; ::_thesis: ( S1 = a .. W implies (- a1) .. W = (- a) .. W )
assume  S1 = a .. W ; ::_thesis: (- a1) .. W = (- 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; ::_thesis: verum
end;
take  (- a1) .. W ; ::_thesis: for a being Vector of V st S1 = a .. W holds
(- a1) .. W = (- a) .. W
thus  for a being Vector of V st S1 = a .. W holds
(- a1) .. W = (- a) .. W by A2; ::_thesis: verum
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
let S, T be Element of V .. W; ::_thesis: ( ( for a being Vector of V st S1 = a .. W holds
S = (- a) .. W ) & ( for a being Vector of V st S1 = a .. W holds
T = (- a) .. W ) implies S = T )
assume that
A3: for a being Vector of V st S1 = a .. W holds
S = (- a) .. W and
A4: for a being Vector of V st S1 = a .. W holds
T = (- a) .. W ; ::_thesis: S = T
consider a1 being Vector of V such that
A5: S1 = a1 .. W by Th12;
thus S = (- a1) .. W by A3, A5
.= T by A4, A5 ; ::_thesis: verum
end;
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 & 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
consider a1 being Vector of V such that
A6: S1 = a1 .. W by Th12;
consider a2 being Vector of V such that
A7: S2 = a2 .. W by Th12;
A8: now__::_thesis:_for_b1,_b2_being_Vector_of_V_st_S1_=_b1_.._W_&_S2_=_b2_.._W_holds_
(a1_+_a2)_.._W_=_(b1_+_b2)_.._W
let b1, b2 be Vector of V; ::_thesis: ( S1 = b1 .. W & S2 = b2 .. W implies (a1 + a2) .. W = (b1 + b2) .. W )
assume that
A9: S1 = b1 .. W and
A10: S2 = b2 .. W ; ::_thesis: (a1 + a2) .. W = (b1 + 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; ::_thesis: verum
end;
take  (a1 + a2) .. W ; ::_thesis: for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
(a1 + a2) .. W = (a1 + a2) .. W
thus  for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
(a1 + a2) .. W = (a1 + a2) .. W by A8; ::_thesis: verum
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
let S, T be Element of V .. W; ::_thesis: ( ( for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
S = (a1 + a2) .. W ) & ( for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
T = (a1 + a2) .. W ) implies S = T )
assume that
A13: for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
S = (a1 + a2) .. W and
A14: for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
T = (a1 + a2) .. W ; ::_thesis: S = T
consider a1 being Vector of V such that
A15: S1 = a1 .. W by Th12;
consider a2 being Vector of V such that
A16: S2 = a2 .. W by Th12;
thus S = (a1 + a2) .. W by A13, A15, A16
.= T by A14, A15, A16 ; ::_thesis: verum
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
thus  ex U being UnOp of (V .. W) st
for S1 being Element of V .. W holds U . S1 = H1(S1) from FUNCT_2:sch_4(); ::_thesis: verum
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
thus  for U1, U2 being UnOp of (V .. W) st ( for S1 being Element of V .. W holds U1 . S1 = H1(S1) ) & ( for S1 being Element of V .. W holds U2 . S1 = H1(S1) ) holds
U1 = U2 from LMOD_7:sch_2(); ::_thesis: verum
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
thus  ex B being BinOp of (V .. W) st
for S1, S2 being Element of V .. W holds B . (S1,S2) = H2(S1,S2) from BINOP_1:sch_4(); ::_thesis: verum
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
thus  for B1, B2 being BinOp of (V .. W) st ( for S1, S2 being Element of V .. W holds B1 . (S1,S2) = H2(S1,S2) ) & ( for S1, S2 being Element of V .. W holds B2 . (S1,S2) = H2(S1,S2) ) holds
B1 = B2 from BINOP_2:sch_2(); ::_thesis: verum
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;
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
proof
let K be Ring; ::_thesis: 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
let V be LeftMod of K; ::_thesis: for W being Subspace of V
for x being Element of (V . W) ex a being Vector of V st x = a . W
let W be Subspace of V; ::_thesis: for x being Element of (V . W) ex a being Vector of V st x = a . W
let x be Element of (V . W); ::_thesis: ex a being Vector of V st x = a . W
consider a being Vector of V such that
A1: x = a .. W by Th12;
take  a ; ::_thesis: x = a . W
thus  x = a . W by A1; ::_thesis: verum
end;

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 & 0. (V . W) = (0. V) . W )
proof
let K be Ring; ::_thesis: 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 )
let V be LeftMod of K; ::_thesis: 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 )
let a, b be Vector of V; ::_thesis: for W being Subspace of V holds
( (a . W) + (b . W) = (a + b) . W & 0. (V . W) = (0. V) . W )
let W be Subspace of V; ::_thesis: ( (a . W) + (b . W) = (a + b) . W & 0. (V . W) = (0. V) . W )
thus (a . W) + (b . W) = (a .. W) + (b .. W) by Def17
.= (a + b) . W by Def15 ; ::_thesis: 0. (V . W) = (0. V) . W
thus  0. (V . W) = (0. V) . W ; ::_thesis: verum
end;

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 & V . W is add-associative & V . W is right_zeroed & V . W is right_complementable )
proof
set G = V . W;
hereby  :: according to RLVECT_1:def_2 ::_thesis: ( V . W is add-associative & V . W is right_zeroed & V . W is right_complementable )
let x, y be Element of (V . W); ::_thesis: x + y = y + x
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; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_3 ::_thesis: ( V . W is right_zeroed & V . W is right_complementable )
let x, y, z be Element of (V . W); ::_thesis: (x + y) + z = x + (y + z)
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 ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_4 ::_thesis: V . W is right_complementable
let x be Element of (V . W); ::_thesis: x + (0. (V . W)) = x
consider a being Vector of V such that
A8: x = a . W by Th15;
 0. (V . W) = (0. V) . W ;
hence x + (0. (V . W)) = (a + (0. V)) . W by A8, Th17
.= x by A8, RLVECT_1:4 ;
::_thesis: verum
end;
let x be Element of (V . W); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
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 (V . W) ;
take  b9 ; :: according to ALGSTR_0:def_11 ::_thesis: x + b9 = 0. (V . W)
thus x + b9 = (0. V) . W by A9, A10, Th17
.= 0. (V . W) ; ::_thesis: verum
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);
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
proof
consider a1 being Vector of V such that
A1: S = a1 . W by Th15;
A2: now__::_thesis:_for_a_being_Vector_of_V_st_S_=_a_._W_holds_
(r_*_a)_._W_=_(r_*_a1)_._W
let a be Vector of V; ::_thesis: ( S = a . W implies (r * a) . W = (r * a1) . W )
assume  S = a . W ; ::_thesis: (r * a) . W = (r * a1) . 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; ::_thesis: verum
end;
take  (r * a1) . W ; ::_thesis: for a being Vector of V st S = a . W holds
(r * a1) . W = (r * a) . W
thus  for a being Vector of V st S = a . W holds
(r * a1) . W = (r * a) . W by A2; ::_thesis: verum
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
let S1, S2 be Element of (V . W); ::_thesis: ( ( for a being Vector of V st S = a . W holds
S1 = (r * a) . W ) & ( for a being Vector of V st S = a . W holds
S2 = (r * a) . W ) implies S1 = S2 )
assume that
A3: for a being Vector of V st S = a . W holds
S1 = (r * a) . W and
A4: for a being Vector of V st S = a . W holds
S2 = (r * a) . W ; ::_thesis: S1 = S2
consider a1 being Vector of V such that
A5: S = a1 . W by Th15;
thus S1 = (r * a1) . W by A3, A5
.= S2 by A4, A5 ; ::_thesis: verum
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
deffunc H1( Scalar of K, Element of (V . W)) ->  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: for r being Scalar of K
for S being Element of (V . W) holds F . (r,S) = H1(r,S) from BINOP_1:sch_4();
take  F ; ::_thesis: for r being Scalar of K
for S being Element of (V . W) holds F . (r,S) = r * S
thus  for r being Scalar of K
for S being Element of (V . W) holds F . (r,S) = r * S by A1; ::_thesis: verum
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
let F, G be Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W); ::_thesis: ( ( for r being Scalar of K
for S being Element of (V . W) holds F . (r,S) = r * S ) & ( for r being Scalar of K
for S being Element of (V . W) holds G . (r,S) = r * S ) implies F = G )
assume that
A2: for r being Scalar of K
for S being Element of (V . W) holds F . (r,S) = r * S and
A3: for r being Scalar of K
for S being Element of (V . W) holds G . (r,S) = r * S ; ::_thesis: F = G
now__::_thesis:_for_r_being_Scalar_of_K
for_S_being_Element_of_(V_._W)_holds_F_._(r,S)_=_G_._(r,S)
let r be Scalar of K; ::_thesis: for S being Element of (V . W) holds F . (r,S) = G . (r,S)
let S be Element of (V . W); ::_thesis: F . (r,S) = G . (r,S)
thus F . (r,S) = r * S by A2
.= G . (r,S) by A3 ; ::_thesis: verum
end;
hence  F = G by BINOP_1:2; ::_thesis: verum
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;
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
proof
let K be Ring; ::_thesis: 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
let V be LeftMod of K; ::_thesis: for W being Subspace of V
for x being Vector of (V / W) ex a being Vector of V st x = a / W
let W be Subspace of V; ::_thesis: for x being Vector of (V / W) ex a being Vector of V st x = a / W
let x be Vector of (V / W); ::_thesis: ex a being Vector of V st x = a / W
consider a being Vector of V such that
A1: x = a . W by Th15;
take  a ; ::_thesis: x = a / W
thus  x = a / W by A1; ::_thesis: verum
end;

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 & r * (a / W) = (r * a) / W )
proof
let K be Ring; ::_thesis: 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 )
let r be Scalar of K; ::_thesis: 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 )
let V be LeftMod of K; ::_thesis: 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 )
let a, b be Vector of V; ::_thesis: for W being Subspace of V holds
( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )
let W be Subspace of V; ::_thesis: ( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )
thus (a / W) + (b / W) = (a . W) + (b . W)
.= (a + b) / W by Th17 ; ::_thesis: r * (a / W) = (r * a) / W
thus r * (a / W) = (LMULT W) . (r,(a . W)) by VECTSP_1:def_12
.= r * (a . W) by Def21
.= (r * a) / W by Def20 ; ::_thesis: verum
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
let K be Ring; ::_thesis: 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 )
let V be LeftMod of K; ::_thesis: 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 )
let W be Subspace of V; ::_thesis: ( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )
A1: for x, y, z being Element of (V . W)
for x9, y9, z9 being Vector of (V / W) st x = x9 & y = y9 & z = z9 holds
x + y = x9 + y9 ;
thus  V / W is Abelian ::_thesis: ( V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )
proof
let x, y be Vector of (V / W); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
reconsider x9 = x, y9 = y as Element of (V . W) ;
thus x + y = x9 + y9
.= y + x by A1 ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_3 ::_thesis: ( V / W is right_zeroed & V / W is right_complementable )
let x, y, z be Vector of (V / W); ::_thesis: (x + y) + z = x + (y + z)
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) ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_4 ::_thesis: V / W is right_complementable
let x be Vector of (V / W); ::_thesis: x + (0. (V / W)) = x
reconsider x9 = x as Element of (V . W) ;
thus x + (0. (V / W)) = x9 + (0. (V . W))
.= x by RLVECT_1:4 ; ::_thesis: verum
end;
let x be Vector of (V / W); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
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 ; :: according to ALGSTR_0:def_11 ::_thesis: x + b9 = 0. (V / W)
thus  x + b9 = 0. (V / W) by A2; ::_thesis: verum
end;

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
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W being Subspace of V holds V / W is strict LeftMod of K
let V be LeftMod of K; ::_thesis: for W being Subspace of V holds V / W is strict LeftMod of K
let W be Subspace of V; ::_thesis: V / W is strict LeftMod of K
now__::_thesis:_for_x,_y_being_Scalar_of_K
for_v,_w_being_Vector_of_(V_/_W)_holds_
(_x_*_(v_+_w)_=_(x_*_v)_+_(x_*_w)_&_(x_+_y)_*_v_=_(x_*_v)_+_(y_*_v)_&_(x_*_y)_*_v_=_x_*_(y_*_v)_&_(1__K)_*_v_=_v_)
let x, y be Scalar of K; ::_thesis: for v, w being Vector of (V / W) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )
let v, w be Vector of (V / W); ::_thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )
consider a being Vector of V such that
A1: v = a / W by Th20;
consider b being Vector of V 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 ; ::_thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )
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 ; ::_thesis: ( (x * y) * v = x * (y * v) & (1_ K) * v = v )
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 ; ::_thesis: (1_ K) * v = v
thus (1_ K) * v = ((1_ K) * a) / W by A1, Th22
.= v by A1, VECTSP_1:def_17 ; ::_thesis: verum
end;
hence  V / W is strict LeftMod of K by Lm2, VECTSP_1:def_14, VECTSP_1:def_15, VECTSP_1:def_16, VECTSP_1:def_17; ::_thesis: verum
end;

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 & V / W is scalar-distributive & V / W is scalar-associative & V / W is scalar-unital ) by Th23;
end;