:: RMOD_4 semantic presentation
begin
Lm1: for R being Ring
for V being RightMod of R
for v being Vector of V
for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds
Sum F = (Sum G) + v
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v being Vector of V
for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds
Sum F = (Sum G) + v
let V be RightMod of R; ::_thesis: for v being Vector of V
for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds
Sum F = (Sum G) + v
let v be Vector of V; ::_thesis: for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds
Sum F = (Sum G) + v
let F, G be FinSequence of V; ::_thesis: ( len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) implies Sum F = (Sum G) + v )
( len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) implies Sum F = (Sum G) + v ) by RLVECT_1:38;
hence ( len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) implies Sum F = (Sum G) + v ) by FINSEQ_1:def_3; ::_thesis: verum
end;
theorem Th1: :: RMOD_4:1
for R being Ring
for V being RightMod of R
for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = v * a ) holds
Sum F = (Sum G) * a
proof
let R be Ring; ::_thesis: for V being RightMod of R
for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = v * a ) holds
Sum F = (Sum G) * a
let V be RightMod of R; ::_thesis: for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = v * a ) holds
Sum F = (Sum G) * a
let a be Scalar of R; ::_thesis: for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = v * a ) holds
Sum F = (Sum G) * a
let F, G be FinSequence of V; ::_thesis: ( len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = v * a ) implies Sum F = (Sum G) * a )
defpred S1[ Nat] means for H, I being FinSequence of V st len H = len I & len H = $1 & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a;
now__::_thesis:_for_n_being_Element_of_NAT_st_(_for_H,_I_being_FinSequence_of_V_st_len_H_=_len_I_&_len_H_=_n_&_(_for_k_being_Nat
for_v_being_Vector_of_V_st_k_in_dom_H_&_v_=_I_._k_holds_
H_._k_=_v_*_a_)_holds_
Sum_H_=_(Sum_I)_*_a_)_holds_
for_H,_I_being_FinSequence_of_V_st_len_H_=_len_I_&_len_H_=_n_+_1_&_(_for_k_being_Nat
for_v_being_Vector_of_V_st_k_in_dom_H_&_v_=_I_._k_holds_
H_._k_=_v_*_a_)_holds_
Sum_H_=_(Sum_I)_*_a
let n be Element of NAT ; ::_thesis: ( ( for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a ) implies for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a )
assume A1: for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a ; ::_thesis: for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) holds
Sum H = (Sum I) * a
let H, I be FinSequence of V; ::_thesis: ( len H = len I & len H = n + 1 & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) implies Sum H = (Sum I) * a )
assume that
A2: len H = len I and
A3: len H = n + 1 and
A4: for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ; ::_thesis: Sum H = (Sum I) * a
reconsider p = H | (Seg n), q = I | (Seg n) as FinSequence of V by FINSEQ_1:18;
A5: n <= n + 1 by NAT_1:12;
then A6: len p = n by A3, FINSEQ_1:17;
A7: len q = n by A2, A3, A5, FINSEQ_1:17;
A8: now__::_thesis:_for_k_being_Nat
for_v_being_Vector_of_V_st_k_in_dom_p_&_v_=_q_._k_holds_
p_._k_=_v_*_a
len p <= len H by A3, A5, FINSEQ_1:17;
then A9: dom p c= dom H by FINSEQ_3:30;
let k be Nat; ::_thesis: for v being Vector of V st k in dom p & v = q . k holds
p . k = v * a
let v be Vector of V; ::_thesis: ( k in dom p & v = q . k implies p . k = v * a )
assume that
A10: k in dom p and
A11: v = q . k ; ::_thesis: p . k = v * a
dom p = dom q by A6, A7, FINSEQ_3:29;
then I . k = q . k by A10, FUNCT_1:47;
then H . k = v * a by A4, A10, A11, A9;
hence p . k = v * a by A10, FUNCT_1:47; ::_thesis: verum
end;
A12: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then ( n + 1 in dom H & n + 1 in dom I ) by A2, A3, FINSEQ_1:def_3;
then reconsider v1 = H . (n + 1), v2 = I . (n + 1) as Vector of V by FINSEQ_2:11;
n + 1 in dom H by A3, A12, FINSEQ_1:def_3;
then A13: v1 = v2 * a by A4;
thus Sum H = (Sum p) + v1 by A3, A6, Lm1
.= ((Sum q) * a) + (v2 * a) by A1, A6, A7, A8, A13
.= ((Sum q) + v2) * a by VECTSP_2:def_9
.= (Sum I) * a by A2, A3, A7, Lm1 ; ::_thesis: verum
end;
then A14: for i being Element of NAT st S1[i] holds
S1[i + 1] ;
now__::_thesis:_for_H,_I_being_FinSequence_of_V_st_len_H_=_len_I_&_len_H_=_0_&_(_for_k_being_Nat
for_v_being_Vector_of_V_st_k_in_dom_H_&_v_=_I_._k_holds_
H_._k_=_v_*_a_)_holds_
Sum_H_=_(Sum_I)_*_a
let H, I be FinSequence of V; ::_thesis: ( len H = len I & len H = 0 & ( for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ) implies Sum H = (Sum I) * a )
assume that
A15: len H = len I and
A16: len H = 0 and
for k being Nat
for v being Vector of V st k in dom H & v = I . k holds
H . k = v * a ; ::_thesis: Sum H = (Sum I) * a
H = <*> the carrier of V by A16;
then A17: Sum H = 0. V by RLVECT_1:43;
I = <*> the carrier of V by A15, A16;
then Sum I = 0. V by RLVECT_1:43;
hence Sum H = (Sum I) * a by A17, VECTSP_2:32; ::_thesis: verum
end;
then A18: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A18, A14);
hence ( len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = v * a ) implies Sum F = (Sum G) * a ) ; ::_thesis: verum
end;
Lm2: for R being Ring
for V being RightMod of R
for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = (F /. k) * a ) holds
Sum G = (Sum F) * a
proof
let R be Ring; ::_thesis: for V being RightMod of R
for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = (F /. k) * a ) holds
Sum G = (Sum F) * a
let V be RightMod of R; ::_thesis: for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = (F /. k) * a ) holds
Sum G = (Sum F) * a
let a be Scalar of R; ::_thesis: for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = (F /. k) * a ) holds
Sum G = (Sum F) * a
let F, G be FinSequence of V; ::_thesis: ( len F = len G & ( for k being Nat st k in dom F holds
G . k = (F /. k) * a ) implies Sum G = (Sum F) * a )
assume that
A1: len F = len G and
A2: for k being Nat st k in dom F holds
G . k = (F /. k) * a ; ::_thesis: Sum G = (Sum F) * a
now__::_thesis:_for_k_being_Nat
for_v_being_Vector_of_V_st_k_in_dom_G_&_v_=_F_._k_holds_
G_._k_=_v_*_a
let k be Nat; ::_thesis: for v being Vector of V st k in dom G & v = F . k holds
G . k = v * a
let v be Vector of V; ::_thesis: ( k in dom G & v = F . k implies G . k = v * a )
assume that
A3: k in dom G and
A4: v = F . k ; ::_thesis: G . k = v * a
A5: k in dom F by A1, A3, FINSEQ_3:29;
then v = F /. k by A4, PARTFUN1:def_6;
hence G . k = v * a by A2, A5; ::_thesis: verum
end;
hence Sum G = (Sum F) * a by A1, Th1; ::_thesis: verum
end;
theorem :: RMOD_4:2
for R being Ring
for V being RightMod of R
for a being Scalar of R holds (Sum (<*> the carrier of V)) * a = 0. V
proof
let R be Ring; ::_thesis: for V being RightMod of R
for a being Scalar of R holds (Sum (<*> the carrier of V)) * a = 0. V
let V be RightMod of R; ::_thesis: for a being Scalar of R holds (Sum (<*> the carrier of V)) * a = 0. V
let a be Scalar of R; ::_thesis: (Sum (<*> the carrier of V)) * a = 0. V
thus (Sum (<*> the carrier of V)) * a = (0. V) * a by RLVECT_1:43
.= 0. V by VECTSP_2:32 ; ::_thesis: verum
end;
theorem :: RMOD_4:3
for R being Ring
for V being RightMod of R
for a being Scalar of R
for v, u being Vector of V holds (Sum <*v,u*>) * a = (v * a) + (u * a)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for a being Scalar of R
for v, u being Vector of V holds (Sum <*v,u*>) * a = (v * a) + (u * a)
let V be RightMod of R; ::_thesis: for a being Scalar of R
for v, u being Vector of V holds (Sum <*v,u*>) * a = (v * a) + (u * a)
let a be Scalar of R; ::_thesis: for v, u being Vector of V holds (Sum <*v,u*>) * a = (v * a) + (u * a)
let v, u be Vector of V; ::_thesis: (Sum <*v,u*>) * a = (v * a) + (u * a)
thus (Sum <*v,u*>) * a = (v + u) * a by RLVECT_1:45
.= (v * a) + (u * a) by VECTSP_2:def_9 ; ::_thesis: verum
end;
theorem :: RMOD_4:4
for R being Ring
for V being RightMod of R
for a being Scalar of R
for v, u, w being Vector of V holds (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for a being Scalar of R
for v, u, w being Vector of V holds (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a)
let V be RightMod of R; ::_thesis: for a being Scalar of R
for v, u, w being Vector of V holds (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a)
let a be Scalar of R; ::_thesis: for v, u, w being Vector of V holds (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a)
let v, u, w be Vector of V; ::_thesis: (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a)
thus (Sum <*v,u,w*>) * a = ((v + u) + w) * a by RLVECT_1:46
.= ((v + u) * a) + (w * a) by VECTSP_2:def_9
.= ((v * a) + (u * a)) + (w * a) by VECTSP_2:def_9 ; ::_thesis: verum
end;
definition
let R be Ring;
let V be RightMod of R;
let T be finite Subset of V;
func Sum T -> Vector of V means :Def1: :: RMOD_4:def 1
ex F being FinSequence of V st
( rng F = T & F is one-to-one & it = Sum F );
existence
ex b1 being Vector of V ex F being FinSequence of V st
( rng F = T & F is one-to-one & b1 = Sum F )
proof
consider p being FinSequence such that
A1: rng p = T and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of V by A1, FINSEQ_1:def_4;
take Sum p ; ::_thesis: ex F being FinSequence of V st
( rng F = T & F is one-to-one & Sum p = Sum F )
take p ; ::_thesis: ( rng p = T & p is one-to-one & Sum p = Sum p )
thus ( rng p = T & p is one-to-one & Sum p = Sum p ) by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Vector of V st ex F being FinSequence of V st
( rng F = T & F is one-to-one & b1 = Sum F ) & ex F being FinSequence of V st
( rng F = T & F is one-to-one & b2 = Sum F ) holds
b1 = b2 by RLVECT_1:42;
end;
:: deftheorem Def1 defines Sum RMOD_4:def_1_:_
for R being Ring
for V being RightMod of R
for T being finite Subset of V
for b4 being Vector of V holds
( b4 = Sum T iff ex F being FinSequence of V st
( rng F = T & F is one-to-one & b4 = Sum F ) );
theorem Th5: :: RMOD_4:5
for R being Ring
for V being RightMod of R holds Sum ({} V) = 0. V
proof
let R be Ring; ::_thesis: for V being RightMod of R holds Sum ({} V) = 0. V
let V be RightMod of R; ::_thesis: Sum ({} V) = 0. V
Sum (<*> the carrier of V) = 0. V by RLVECT_1:43;
hence Sum ({} V) = 0. V by Def1, RELAT_1:38; ::_thesis: verum
end;
theorem :: RMOD_4:6
for R being Ring
for V being RightMod of R
for v being Vector of V holds Sum {v} = v
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v being Vector of V holds Sum {v} = v
let V be RightMod of R; ::_thesis: for v being Vector of V holds Sum {v} = v
let v be Vector of V; ::_thesis: Sum {v} = v
A1: Sum <*v*> = v by RLVECT_1:44;
( rng <*v*> = {v} & <*v*> is one-to-one ) by FINSEQ_1:39, FINSEQ_3:93;
hence Sum {v} = v by A1, Def1; ::_thesis: verum
end;
theorem :: RMOD_4:7
for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V st v1 <> v2 holds
Sum {v1,v2} = v1 + v2
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v1, v2 being Vector of V st v1 <> v2 holds
Sum {v1,v2} = v1 + v2
let V be RightMod of R; ::_thesis: for v1, v2 being Vector of V st v1 <> v2 holds
Sum {v1,v2} = v1 + v2
let v1, v2 be Vector of V; ::_thesis: ( v1 <> v2 implies Sum {v1,v2} = v1 + v2 )
assume v1 <> v2 ; ::_thesis: Sum {v1,v2} = v1 + v2
then A1: <*v1,v2*> is one-to-one by FINSEQ_3:94;
( rng <*v1,v2*> = {v1,v2} & Sum <*v1,v2*> = v1 + v2 ) by FINSEQ_2:127, RLVECT_1:45;
hence Sum {v1,v2} = v1 + v2 by A1, Def1; ::_thesis: verum
end;
theorem :: RMOD_4:8
for R being Ring
for V being RightMod of R
for v1, v2, v3 being Vector of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds
Sum {v1,v2,v3} = (v1 + v2) + v3
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v1, v2, v3 being Vector of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds
Sum {v1,v2,v3} = (v1 + v2) + v3
let V be RightMod of R; ::_thesis: for v1, v2, v3 being Vector of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds
Sum {v1,v2,v3} = (v1 + v2) + v3
let v1, v2, v3 be Vector of V; ::_thesis: ( v1 <> v2 & v2 <> v3 & v1 <> v3 implies Sum {v1,v2,v3} = (v1 + v2) + v3 )
assume ( v1 <> v2 & v2 <> v3 & v1 <> v3 ) ; ::_thesis: Sum {v1,v2,v3} = (v1 + v2) + v3
then A1: <*v1,v2,v3*> is one-to-one by FINSEQ_3:95;
( rng <*v1,v2,v3*> = {v1,v2,v3} & Sum <*v1,v2,v3*> = (v1 + v2) + v3 ) by FINSEQ_2:128, RLVECT_1:46;
hence Sum {v1,v2,v3} = (v1 + v2) + v3 by A1, Def1; ::_thesis: verum
end;
theorem Th9: :: RMOD_4:9
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V st T misses S holds
Sum (T \/ S) = (Sum T) + (Sum S)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for T, S being finite Subset of V st T misses S holds
Sum (T \/ S) = (Sum T) + (Sum S)
let V be RightMod of R; ::_thesis: for T, S being finite Subset of V st T misses S holds
Sum (T \/ S) = (Sum T) + (Sum S)
let T, S be finite Subset of V; ::_thesis: ( T misses S implies Sum (T \/ S) = (Sum T) + (Sum S) )
consider F being FinSequence of V such that
A1: rng F = T \/ S and
A2: ( F is one-to-one & Sum (T \/ S) = Sum F ) by Def1;
consider G being FinSequence of V such that
A3: rng G = T and
A4: G is one-to-one and
A5: Sum T = Sum G by Def1;
consider H being FinSequence of V such that
A6: rng H = S and
A7: H is one-to-one and
A8: Sum S = Sum H by Def1;
set I = G ^ H;
assume T misses S ; ::_thesis: Sum (T \/ S) = (Sum T) + (Sum S)
then A9: G ^ H is one-to-one by A3, A4, A6, A7, FINSEQ_3:91;
rng (G ^ H) = rng F by A1, A3, A6, FINSEQ_1:31;
hence Sum (T \/ S) = Sum (G ^ H) by A2, A9, RLVECT_1:42
.= (Sum T) + (Sum S) by A5, A8, RLVECT_1:41 ;
::_thesis: verum
end;
theorem Th10: :: RMOD_4:10
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))
proof
let R be Ring; ::_thesis: for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))
let V be RightMod of R; ::_thesis: for T, S being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))
let T, S be finite Subset of V; ::_thesis: Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))
set A = S \ T;
set B = T \ S;
set Z = (S \ T) \/ (T \ S);
set I = T /\ S;
A1: (S \ T) \/ (T /\ S) = S by XBOOLE_1:51;
A2: (T \ S) \/ (T /\ S) = T by XBOOLE_1:51;
A3: (S \ T) \/ (T \ S) = T \+\ S ;
then ((S \ T) \/ (T \ S)) \/ (T /\ S) = T \/ S by XBOOLE_1:93;
then (Sum (T \/ S)) + (Sum (T /\ S)) = ((Sum ((S \ T) \/ (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by A3, Th9, XBOOLE_1:103
.= (((Sum (S \ T)) + (Sum (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by Th9, XBOOLE_1:82
.= ((Sum (S \ T)) + ((Sum (T /\ S)) + (Sum (T \ S)))) + (Sum (T /\ S)) by RLVECT_1:def_3
.= ((Sum (S \ T)) + (Sum (T /\ S))) + ((Sum (T \ S)) + (Sum (T /\ S))) by RLVECT_1:def_3
.= (Sum S) + ((Sum (T \ S)) + (Sum (T /\ S))) by A1, Th9, XBOOLE_1:89
.= (Sum T) + (Sum S) by A2, Th9, XBOOLE_1:89 ;
hence Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) by RLSUB_2:61; ::_thesis: verum
end;
theorem :: RMOD_4:11
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S))
proof
let R be Ring; ::_thesis: for V being RightMod of R
for T, S being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S))
let V be RightMod of R; ::_thesis: for T, S being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S))
let T, S be finite Subset of V; ::_thesis: Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S))
Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) by Th10;
then (Sum T) + (Sum S) = (Sum (T /\ S)) + (Sum (T \/ S)) by RLSUB_2:61;
hence Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S)) by RLSUB_2:61; ::_thesis: verum
end;
theorem Th12: :: RMOD_4:12
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S)
let V be RightMod of R; ::_thesis: for T, S being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S)
let T, S be finite Subset of V; ::_thesis: Sum (T \ S) = (Sum (T \/ S)) - (Sum S)
T \ S misses S by XBOOLE_1:79;
then A1: (T \ S) /\ S = {} V by XBOOLE_0:def_7;
(T \ S) \/ S = T \/ S by XBOOLE_1:39;
then Sum (T \/ S) = ((Sum (T \ S)) + (Sum S)) - (Sum ((T \ S) /\ S)) by Th10;
then Sum (T \/ S) = ((Sum (T \ S)) + (Sum S)) - (0. V) by A1, Th5
.= (Sum (T \ S)) + (Sum S) by VECTSP_1:18 ;
hence Sum (T \ S) = (Sum (T \/ S)) - (Sum S) by RLSUB_2:61; ::_thesis: verum
end;
theorem Th13: :: RMOD_4:13
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))
proof
let R be Ring; ::_thesis: for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))
let V be RightMod of R; ::_thesis: for T, S being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))
let T, S be finite Subset of V; ::_thesis: Sum (T \ S) = (Sum T) - (Sum (T /\ S))
T \ (T /\ S) = T \ S by XBOOLE_1:47;
then Sum (T \ S) = (Sum (T \/ (T /\ S))) - (Sum (T /\ S)) by Th12;
hence Sum (T \ S) = (Sum T) - (Sum (T /\ S)) by XBOOLE_1:22; ::_thesis: verum
end;
theorem :: RMOD_4:14
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))
proof
let R be Ring; ::_thesis: for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))
let V be RightMod of R; ::_thesis: for T, S being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))
let T, S be finite Subset of V; ::_thesis: Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))
T \+\ S = (T \/ S) \ (T /\ S) by XBOOLE_1:101;
hence Sum (T \+\ S) = (Sum (T \/ S)) - (Sum ((T \/ S) /\ (T /\ S))) by Th13
.= (Sum (T \/ S)) - (Sum (((T \/ S) /\ T) /\ S)) by XBOOLE_1:16
.= (Sum (T \/ S)) - (Sum (T /\ S)) by XBOOLE_1:21 ;
::_thesis: verum
end;
theorem :: RMOD_4:15
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \+\ S) = (Sum (T \ S)) + (Sum (S \ T)) by Th9, XBOOLE_1:82;
definition
let R be Ring;
let V be RightMod of R;
mode Linear_Combination of V -> Element of Funcs ( the carrier of V, the carrier of R) means :Def2: :: RMOD_4:def 2
ex T being finite Subset of V st
for v being Vector of V st not v in T holds
it . v = 0. R;
existence
ex b1 being Element of Funcs ( the carrier of V, the carrier of R) ex T being finite Subset of V st
for v being Vector of V st not v in T holds
b1 . v = 0. R
proof
{} V = {} ;
then reconsider P = {} as finite Subset of V ;
reconsider f = the carrier of V --> (0. R) as Function of V,R ;
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
take f ; ::_thesis: ex T being finite Subset of V st
for v being Vector of V st not v in T holds
f . v = 0. R
take P ; ::_thesis: for v being Vector of V st not v in P holds
f . v = 0. R
thus for v being Vector of V st not v in P holds
f . v = 0. R by FUNCOP_1:7; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Linear_Combination RMOD_4:def_2_:_
for R being Ring
for V being RightMod of R
for b3 being Element of Funcs ( the carrier of V, the carrier of R) holds
( b3 is Linear_Combination of V iff ex T being finite Subset of V st
for v being Vector of V st not v in T holds
b3 . v = 0. R );
definition
let R be Ring;
let V be RightMod of R;
let L be Linear_Combination of V;
func Carrier L -> finite Subset of V equals :: RMOD_4:def 3
{ v where v is Vector of V : L . v <> 0. R } ;
coherence
{ v where v is Vector of V : L . v <> 0. R } is finite Subset of V
proof
set A = { v where v is Vector of V : L . v <> 0. R } ;
consider T being finite Subset of V such that
A1: for v being Vector of V st not v in T holds
L . v = 0. R by Def2;
{ v where v is Vector of V : L . v <> 0. R } c= T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Vector of V : L . v <> 0. R } or x in T )
assume x in { v where v is Vector of V : L . v <> 0. R } ; ::_thesis: x in T
then ex v being Vector of V st
( x = v & L . v <> 0. R ) ;
hence x in T by A1; ::_thesis: verum
end;
hence { v where v is Vector of V : L . v <> 0. R } is finite Subset of V by XBOOLE_1:1; ::_thesis: verum
end;
end;
:: deftheorem defines Carrier RMOD_4:def_3_:_
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds Carrier L = { v where v is Vector of V : L . v <> 0. R } ;
theorem :: RMOD_4:16
for R being Ring
for V being RightMod of R
for x being set
for L being Linear_Combination of V holds
( x in Carrier L iff ex v being Vector of V st
( x = v & L . v <> 0. R ) ) ;
theorem :: RMOD_4:17
for R being Ring
for V being RightMod of R
for v being Vector of V
for L being Linear_Combination of V holds
( L . v = 0. R iff not v in Carrier L )
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v being Vector of V
for L being Linear_Combination of V holds
( L . v = 0. R iff not v in Carrier L )
let V be RightMod of R; ::_thesis: for v being Vector of V
for L being Linear_Combination of V holds
( L . v = 0. R iff not v in Carrier L )
let v be Vector of V; ::_thesis: for L being Linear_Combination of V holds
( L . v = 0. R iff not v in Carrier L )
let L be Linear_Combination of V; ::_thesis: ( L . v = 0. R iff not v in Carrier L )
thus ( L . v = 0. R implies not v in Carrier L ) ::_thesis: ( not v in Carrier L implies L . v = 0. R )
proof
assume A1: L . v = 0. R ; ::_thesis: not v in Carrier L
assume v in Carrier L ; ::_thesis: contradiction
then ex u being Vector of V st
( u = v & L . u <> 0. R ) ;
hence contradiction by A1; ::_thesis: verum
end;
assume not v in Carrier L ; ::_thesis: L . v = 0. R
hence L . v = 0. R ; ::_thesis: verum
end;
definition
let R be Ring;
let V be RightMod of R;
func ZeroLC V -> Linear_Combination of V means :Def4: :: RMOD_4:def 4
Carrier it = {} ;
existence
ex b1 being Linear_Combination of V st Carrier b1 = {}
proof
reconsider f = the carrier of V --> (0. R) as Function of V,R ;
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
f is Linear_Combination of V
proof
reconsider T = {} V as empty finite Subset of V ;
take T ; :: according to RMOD_4:def_2 ::_thesis: for v being Vector of V st not v in T holds
f . v = 0. R
thus for v being Vector of V st not v in T holds
f . v = 0. R by FUNCOP_1:7; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V ;
take f ; ::_thesis: Carrier f = {}
set C = { v where v is Vector of V : f . v <> 0. R } ;
now__::_thesis:_not__{__v_where_v_is_Vector_of_V_:_f_._v_<>_0._R__}__<>_{}
set x = the Element of { v where v is Vector of V : f . v <> 0. R } ;
assume { v where v is Vector of V : f . v <> 0. R } <> {} ; ::_thesis: contradiction
then the Element of { v where v is Vector of V : f . v <> 0. R } in { v where v is Vector of V : f . v <> 0. R } ;
then ex v being Vector of V st
( the Element of { v where v is Vector of V : f . v <> 0. R } = v & f . v <> 0. R ) ;
hence contradiction by FUNCOP_1:7; ::_thesis: verum
end;
hence Carrier f = {} ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Linear_Combination of V st Carrier b1 = {} & Carrier b2 = {} holds
b1 = b2
proof
let L, L9 be Linear_Combination of V; ::_thesis: ( Carrier L = {} & Carrier L9 = {} implies L = L9 )
assume that
A1: Carrier L = {} and
A2: Carrier L9 = {} ; ::_thesis: L = L9
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_
L_._x_=_L9_._x
let x be set ; ::_thesis: ( x in the carrier of V implies L . x = L9 . x )
assume x in the carrier of V ; ::_thesis: L . x = L9 . x
then reconsider v = x as Element of V ;
A3: now__::_thesis:_not_L9_._v_<>_0._R
assume L9 . v <> 0. R ; ::_thesis: contradiction
then v in { u where u is Vector of V : L9 . u <> 0. R } ;
hence contradiction by A2; ::_thesis: verum
end;
now__::_thesis:_not_L_._v_<>_0._R
assume L . v <> 0. R ; ::_thesis: contradiction
then v in { u where u is Vector of V : L . u <> 0. R } ;
hence contradiction by A1; ::_thesis: verum
end;
hence L . x = L9 . x by A3; ::_thesis: verum
end;
hence L = L9 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines ZeroLC RMOD_4:def_4_:_
for R being Ring
for V being RightMod of R
for b3 being Linear_Combination of V holds
( b3 = ZeroLC V iff Carrier b3 = {} );
theorem Th18: :: RMOD_4:18
for R being Ring
for V being RightMod of R
for v being Vector of V holds (ZeroLC V) . v = 0. R
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v being Vector of V holds (ZeroLC V) . v = 0. R
let V be RightMod of R; ::_thesis: for v being Vector of V holds (ZeroLC V) . v = 0. R
let v be Vector of V; ::_thesis: (ZeroLC V) . v = 0. R
( Carrier (ZeroLC V) = {} & not v in {} ) by Def4;
hence (ZeroLC V) . v = 0. R ; ::_thesis: verum
end;
definition
let R be Ring;
let V be RightMod of R;
let A be Subset of V;
mode Linear_Combination of A -> Linear_Combination of V means :Def5: :: RMOD_4:def 5
Carrier it c= A;
existence
ex b1 being Linear_Combination of V st Carrier b1 c= A
proof
take L = ZeroLC V; ::_thesis: Carrier L c= A
Carrier L = {} by Def4;
hence Carrier L c= A by XBOOLE_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Linear_Combination RMOD_4:def_5_:_
for R being Ring
for V being RightMod of R
for A being Subset of V
for b4 being Linear_Combination of V holds
( b4 is Linear_Combination of A iff Carrier b4 c= A );
theorem Th19: :: RMOD_4:19
for R being Ring
for V being RightMod of R
for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B
proof
let R be Ring; ::_thesis: for V being RightMod of R
for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B
let V be RightMod of R; ::_thesis: for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B
let A, B be Subset of V; ::_thesis: for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B
let l be Linear_Combination of A; ::_thesis: ( A c= B implies l is Linear_Combination of B )
assume A1: A c= B ; ::_thesis: l is Linear_Combination of B
Carrier l c= A by Def5;
then Carrier l c= B by A1, XBOOLE_1:1;
hence l is Linear_Combination of B by Def5; ::_thesis: verum
end;
theorem Th20: :: RMOD_4:20
for R being Ring
for V being RightMod of R
for A being Subset of V holds ZeroLC V is Linear_Combination of A
proof
let R be Ring; ::_thesis: for V being RightMod of R
for A being Subset of V holds ZeroLC V is Linear_Combination of A
let V be RightMod of R; ::_thesis: for A being Subset of V holds ZeroLC V is Linear_Combination of A
let A be Subset of V; ::_thesis: ZeroLC V is Linear_Combination of A
( Carrier (ZeroLC V) = {} & {} c= A ) by Def4, XBOOLE_1:2;
hence ZeroLC V is Linear_Combination of A by Def5; ::_thesis: verum
end;
theorem Th21: :: RMOD_4:21
for R being Ring
for V being RightMod of R
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V
proof
let R be Ring; ::_thesis: for V being RightMod of R
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V
let V be RightMod of R; ::_thesis: for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V
let l be Linear_Combination of {} the carrier of V; ::_thesis: l = ZeroLC V
Carrier l c= {} by Def5;
then Carrier l = {} ;
hence l = ZeroLC V by Def4; ::_thesis: verum
end;
theorem :: RMOD_4:22
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds L is Linear_Combination of Carrier L by Def5;
definition
let R be Ring;
let V be RightMod of R;
let F be FinSequence of V;
let f be Function of V,R;
funcf (#) F -> FinSequence of V means :Def6: :: RMOD_4:def 6
( len it = len F & ( for i being Nat st i in dom it holds
it . i = (F /. i) * (f . (F /. i)) ) );
existence
ex b1 being FinSequence of V st
( len b1 = len F & ( for i being Nat st i in dom b1 holds
b1 . i = (F /. i) * (f . (F /. i)) ) )
proof
deffunc H1( Nat) -> Element of the carrier of V = (F /. $1) * (f . (F /. $1));
consider G being FinSequence such that
A1: len G = len F and
A2: for n being Nat st n in dom G holds
G . n = H1(n) from FINSEQ_1:sch_2();
rng G c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in the carrier of V )
assume x in rng G ; ::_thesis: x in the carrier of V
then consider y being set such that
A3: y in dom G and
A4: G . y = x by FUNCT_1:def_3;
y in Seg (len F) by A1, A3, FINSEQ_1:def_3;
then reconsider y = y as Element of NAT ;
G . y = (F /. y) * (f . (F /. y)) by A2, A3;
hence x in the carrier of V by A4; ::_thesis: verum
end;
then reconsider G = G as FinSequence of V by FINSEQ_1:def_4;
take G ; ::_thesis: ( len G = len F & ( for i being Nat st i in dom G holds
G . i = (F /. i) * (f . (F /. i)) ) )
thus ( len G = len F & ( for i being Nat st i in dom G holds
G . i = (F /. i) * (f . (F /. i)) ) ) by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of V st len b1 = len F & ( for i being Nat st i in dom b1 holds
b1 . i = (F /. i) * (f . (F /. i)) ) & len b2 = len F & ( for i being Nat st i in dom b2 holds
b2 . i = (F /. i) * (f . (F /. i)) ) holds
b1 = b2
proof
let H1, H2 be FinSequence of V; ::_thesis: ( len H1 = len F & ( for i being Nat st i in dom H1 holds
H1 . i = (F /. i) * (f . (F /. i)) ) & len H2 = len F & ( for i being Nat st i in dom H2 holds
H2 . i = (F /. i) * (f . (F /. i)) ) implies H1 = H2 )
assume that
A5: len H1 = len F and
A6: for i being Nat st i in dom H1 holds
H1 . i = (F /. i) * (f . (F /. i)) and
A7: len H2 = len F and
A8: for i being Nat st i in dom H2 holds
H2 . i = (F /. i) * (f . (F /. i)) ; ::_thesis: H1 = H2
now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_H1_holds_
H1_._k_=_H2_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len H1 implies H1 . k = H2 . k )
assume ( 1 <= k & k <= len H1 ) ; ::_thesis: H1 . k = H2 . k
then A9: k in Seg (len H1) by FINSEQ_1:1;
then k in dom H1 by FINSEQ_1:def_3;
then A10: H1 . k = (F /. k) * (f . (F /. k)) by A6;
k in dom H2 by A5, A7, A9, FINSEQ_1:def_3;
hence H1 . k = H2 . k by A8, A10; ::_thesis: verum
end;
hence H1 = H2 by A5, A7, FINSEQ_1:14; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines (#) RMOD_4:def_6_:_
for R being Ring
for V being RightMod of R
for F being FinSequence of V
for f being Function of V,R
for b5 being FinSequence of V holds
( b5 = f (#) F iff ( len b5 = len F & ( for i being Nat st i in dom b5 holds
b5 . i = (F /. i) * (f . (F /. i)) ) ) );
theorem Th23: :: RMOD_4:23
for R being Ring
for V being RightMod of R
for i being Nat
for v being Vector of V
for F being FinSequence of V
for f being Function of V,R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for i being Nat
for v being Vector of V
for F being FinSequence of V
for f being Function of V,R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)
let V be RightMod of R; ::_thesis: for i being Nat
for v being Vector of V
for F being FinSequence of V
for f being Function of V,R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)
let i be Nat; ::_thesis: for v being Vector of V
for F being FinSequence of V
for f being Function of V,R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)
let v be Vector of V; ::_thesis: for F being FinSequence of V
for f being Function of V,R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)
let F be FinSequence of V; ::_thesis: for f being Function of V,R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)
let f be Function of V,R; ::_thesis: ( i in dom F & v = F . i implies (f (#) F) . i = v * (f . v) )
assume that
A1: i in dom F and
A2: v = F . i ; ::_thesis: (f (#) F) . i = v * (f . v)
A3: F /. i = F . i by A1, PARTFUN1:def_6;
len (f (#) F) = len F by Def6;
then i in dom (f (#) F) by A1, FINSEQ_3:29;
hence (f (#) F) . i = v * (f . v) by A2, A3, Def6; ::_thesis: verum
end;
theorem :: RMOD_4:24
for R being Ring
for V being RightMod of R
for f being Function of V,R holds f (#) (<*> the carrier of V) = <*> the carrier of V
proof
let R be Ring; ::_thesis: for V being RightMod of R
for f being Function of V,R holds f (#) (<*> the carrier of V) = <*> the carrier of V
let V be RightMod of R; ::_thesis: for f being Function of V,R holds f (#) (<*> the carrier of V) = <*> the carrier of V
let f be Function of V,R; ::_thesis: f (#) (<*> the carrier of V) = <*> the carrier of V
len (f (#) (<*> the carrier of V)) = len (<*> the carrier of V) by Def6
.= 0 ;
hence f (#) (<*> the carrier of V) = <*> the carrier of V ; ::_thesis: verum
end;
theorem Th25: :: RMOD_4:25
for R being Ring
for V being RightMod of R
for v being Vector of V
for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*>
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v being Vector of V
for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*>
let V be RightMod of R; ::_thesis: for v being Vector of V
for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*>
let v be Vector of V; ::_thesis: for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*>
let f be Function of V,R; ::_thesis: f (#) <*v*> = <*(v * (f . v))*>
A1: 1 in {1} by TARSKI:def_1;
A2: len (f (#) <*v*>) = len <*v*> by Def6
.= 1 by FINSEQ_1:40 ;
then dom (f (#) <*v*>) = {1} by FINSEQ_1:2, FINSEQ_1:def_3;
then (f (#) <*v*>) . 1 = (<*v*> /. 1) * (f . (<*v*> /. 1)) by A1, Def6
.= v * (f . (<*v*> /. 1)) by FINSEQ_4:16
.= v * (f . v) by FINSEQ_4:16 ;
hence f (#) <*v*> = <*(v * (f . v))*> by A2, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th26: :: RMOD_4:26
for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V
for f being Function of V,R holds f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*>
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v1, v2 being Vector of V
for f being Function of V,R holds f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*>
let V be RightMod of R; ::_thesis: for v1, v2 being Vector of V
for f being Function of V,R holds f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*>
let v1, v2 be Vector of V; ::_thesis: for f being Function of V,R holds f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*>
let f be Function of V,R; ::_thesis: f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*>
A1: len (f (#) <*v1,v2*>) = len <*v1,v2*> by Def6
.= 2 by FINSEQ_1:44 ;
then A2: dom (f (#) <*v1,v2*>) = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3;
2 in {1,2} by TARSKI:def_2;
then A3: (f (#) <*v1,v2*>) . 2 = (<*v1,v2*> /. 2) * (f . (<*v1,v2*> /. 2)) by A2, Def6
.= v2 * (f . (<*v1,v2*> /. 2)) by FINSEQ_4:17
.= v2 * (f . v2) by FINSEQ_4:17 ;
1 in {1,2} by TARSKI:def_2;
then (f (#) <*v1,v2*>) . 1 = (<*v1,v2*> /. 1) * (f . (<*v1,v2*> /. 1)) by A2, Def6
.= v1 * (f . (<*v1,v2*> /. 1)) by FINSEQ_4:17
.= v1 * (f . v1) by FINSEQ_4:17 ;
hence f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*> by A1, A3, FINSEQ_1:44; ::_thesis: verum
end;
theorem :: RMOD_4:27
for R being Ring
for V being RightMod of R
for v1, v2, v3 being Vector of V
for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*>
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v1, v2, v3 being Vector of V
for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*>
let V be RightMod of R; ::_thesis: for v1, v2, v3 being Vector of V
for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*>
let v1, v2, v3 be Vector of V; ::_thesis: for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*>
let f be Function of V,R; ::_thesis: f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*>
A1: len (f (#) <*v1,v2,v3*>) = len <*v1,v2,v3*> by Def6
.= 3 by FINSEQ_1:45 ;
then A2: dom (f (#) <*v1,v2,v3*>) = {1,2,3} by FINSEQ_1:def_3, FINSEQ_3:1;
3 in {1,2,3} by ENUMSET1:def_1;
then A3: (f (#) <*v1,v2,v3*>) . 3 = (<*v1,v2,v3*> /. 3) * (f . (<*v1,v2,v3*> /. 3)) by A2, Def6
.= v3 * (f . (<*v1,v2,v3*> /. 3)) by FINSEQ_4:18
.= v3 * (f . v3) by FINSEQ_4:18 ;
2 in {1,2,3} by ENUMSET1:def_1;
then A4: (f (#) <*v1,v2,v3*>) . 2 = (<*v1,v2,v3*> /. 2) * (f . (<*v1,v2,v3*> /. 2)) by A2, Def6
.= v2 * (f . (<*v1,v2,v3*> /. 2)) by FINSEQ_4:18
.= v2 * (f . v2) by FINSEQ_4:18 ;
1 in {1,2,3} by ENUMSET1:def_1;
then (f (#) <*v1,v2,v3*>) . 1 = (<*v1,v2,v3*> /. 1) * (f . (<*v1,v2,v3*> /. 1)) by A2, Def6
.= v1 * (f . (<*v1,v2,v3*> /. 1)) by FINSEQ_4:18
.= v1 * (f . v1) by FINSEQ_4:18 ;
hence f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*> by A1, A4, A3, FINSEQ_1:45; ::_thesis: verum
end;
theorem Th28: :: RMOD_4:28
for R being Ring
for V being RightMod of R
for F, G being FinSequence of V
for f being Function of V,R holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for F, G being FinSequence of V
for f being Function of V,R holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
let V be RightMod of R; ::_thesis: for F, G being FinSequence of V
for f being Function of V,R holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
let F, G be FinSequence of V; ::_thesis: for f being Function of V,R holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
let f be Function of V,R; ::_thesis: f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
set H = (f (#) F) ^ (f (#) G);
set I = F ^ G;
A1: len F = len (f (#) F) by Def6;
A2: len ((f (#) F) ^ (f (#) G)) = (len (f (#) F)) + (len (f (#) G)) by FINSEQ_1:22
.= (len F) + (len (f (#) G)) by Def6
.= (len F) + (len G) by Def6
.= len (F ^ G) by FINSEQ_1:22 ;
A3: len G = len (f (#) G) by Def6;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_((f_(#)_F)_^_(f_(#)_G))_holds_
((f_(#)_F)_^_(f_(#)_G))_._k_=_((F_^_G)_/._k)_*_(f_._((F_^_G)_/._k))
let k be Nat; ::_thesis: ( k in dom ((f (#) F) ^ (f (#) G)) implies ((f (#) F) ^ (f (#) G)) . k = ((F ^ G) /. k) * (f . ((F ^ G) /. k)) )
assume A4: k in dom ((f (#) F) ^ (f (#) G)) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = ((F ^ G) /. k) * (f . ((F ^ G) /. k))
now__::_thesis:_((f_(#)_F)_^_(f_(#)_G))_._k_=_((F_^_G)_/._k)_*_(f_._((F_^_G)_/._k))
percases ( k in dom (f (#) F) or ex n being Nat st
( n in dom (f (#) G) & k = (len (f (#) F)) + n ) ) by A4, FINSEQ_1:25;
supposeA5: k in dom (f (#) F) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = ((F ^ G) /. k) * (f . ((F ^ G) /. k))
then A6: k in dom F by A1, FINSEQ_3:29;
then A7: k in dom (F ^ G) by FINSEQ_3:22;
A8: F /. k = F . k by A6, PARTFUN1:def_6
.= (F ^ G) . k by A6, FINSEQ_1:def_7
.= (F ^ G) /. k by A7, PARTFUN1:def_6 ;
thus ((f (#) F) ^ (f (#) G)) . k = (f (#) F) . k by A5, FINSEQ_1:def_7
.= ((F ^ G) /. k) * (f . ((F ^ G) /. k)) by A5, A8, Def6 ; ::_thesis: verum
end;
supposeA9: ex n being Nat st
( n in dom (f (#) G) & k = (len (f (#) F)) + n ) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = ((F ^ G) /. k) * (f . ((F ^ G) /. k))
A10: k in dom (F ^ G) by A2, A4, FINSEQ_3:29;
consider n being Nat such that
A11: n in dom (f (#) G) and
A12: k = (len (f (#) F)) + n by A9;
A13: n in dom G by A3, A11, FINSEQ_3:29;
then A14: G /. n = G . n by PARTFUN1:def_6
.= (F ^ G) . k by A1, A12, A13, FINSEQ_1:def_7
.= (F ^ G) /. k by A10, PARTFUN1:def_6 ;
thus ((f (#) F) ^ (f (#) G)) . k = (f (#) G) . n by A11, A12, FINSEQ_1:def_7
.= ((F ^ G) /. k) * (f . ((F ^ G) /. k)) by A11, A14, Def6 ; ::_thesis: verum
end;
end;
end;
hence ((f (#) F) ^ (f (#) G)) . k = ((F ^ G) /. k) * (f . ((F ^ G) /. k)) ; ::_thesis: verum
end;
hence f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by A2, Def6; ::_thesis: verum
end;
definition
let R be Ring;
let V be RightMod of R;
let L be Linear_Combination of V;
func Sum L -> Vector of V means :Def7: :: RMOD_4:def 7
ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) );
existence
ex b1 being Vector of V ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & b1 = Sum (L (#) F) )
proof
consider F being FinSequence such that
A1: rng F = Carrier L and
A2: F is one-to-one by FINSEQ_4:58;
reconsider F = F as FinSequence of V by A1, FINSEQ_1:def_4;
take Sum (L (#) F) ; ::_thesis: ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) )
take F ; ::_thesis: ( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) )
thus ( F is one-to-one & rng F = Carrier L ) by A1, A2; ::_thesis: Sum (L (#) F) = Sum (L (#) F)
thus Sum (L (#) F) = Sum (L (#) F) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Vector of V st ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & b1 = Sum (L (#) F) ) & ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & b2 = Sum (L (#) F) ) holds
b1 = b2
proof
let v1, v2 be Vector of V; ::_thesis: ( ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & v1 = Sum (L (#) F) ) & ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & v2 = Sum (L (#) F) ) implies v1 = v2 )
given F1 being FinSequence of V such that A3: F1 is one-to-one and
A4: rng F1 = Carrier L and
A5: v1 = Sum (L (#) F1) ; ::_thesis: ( for F being FinSequence of V holds
( not F is one-to-one or not rng F = Carrier L or not v2 = Sum (L (#) F) ) or v1 = v2 )
given F2 being FinSequence of V such that A6: F2 is one-to-one and
A7: rng F2 = Carrier L and
A8: v2 = Sum (L (#) F2) ; ::_thesis: v1 = v2
defpred S1[ set , set ] means {$2} = F1 " {(F2 . $1)};
A9: len F1 = len F2 by A3, A4, A6, A7, FINSEQ_1:48;
A10: dom F1 = Seg (len F1) by FINSEQ_1:def_3;
A11: dom F2 = Seg (len F2) by FINSEQ_1:def_3;
A12: for x being set st x in dom F1 holds
ex y being set st
( y in dom F1 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in dom F1 implies ex y being set st
( y in dom F1 & S1[x,y] ) )
assume x in dom F1 ; ::_thesis: ex y being set st
( y in dom F1 & S1[x,y] )
then F2 . x in rng F1 by A4, A7, A9, A10, A11, FUNCT_1:def_3;
then consider y being set such that
A13: F1 " {(F2 . x)} = {y} by A3, FUNCT_1:74;
take y ; ::_thesis: ( y in dom F1 & S1[x,y] )
y in F1 " {(F2 . x)} by A13, TARSKI:def_1;
hence y in dom F1 by FUNCT_1:def_7; ::_thesis: S1[x,y]
thus S1[x,y] by A13; ::_thesis: verum
end;
consider f being Function of (dom F1),(dom F1) such that
A14: for x being set st x in dom F1 holds
S1[x,f . x] from FUNCT_2:sch_1(A12);
A15: rng f = dom F1
proof
thus rng f c= dom F1 by RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: dom F1 c= rng f
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom F1 or y in rng f )
assume A16: y in dom F1 ; ::_thesis: y in rng f
then F1 . y in rng F2 by A4, A7, FUNCT_1:def_3;
then consider x being set such that
A17: x in dom F2 and
A18: F2 . x = F1 . y by FUNCT_1:def_3;
F1 " {(F2 . x)} = F1 " (Im (F1,y)) by A16, A18, FUNCT_1:59;
then F1 " {(F2 . x)} c= {y} by A3, FUNCT_1:82;
then {(f . x)} c= {y} by A9, A10, A11, A14, A17;
then A19: f . x = y by ZFMISC_1:18;
x in dom f by A9, A10, A11, A17, FUNCT_2:def_1;
hence y in rng f by A19, FUNCT_1:def_3; ::_thesis: verum
end;
set G1 = L (#) F1;
A20: len (L (#) F1) = len F1 by Def6;
A21: ( dom F1 = {} implies dom F1 = {} ) ;
A22: f is one-to-one
proof
let y1, y2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not y1 in dom f or not y2 in dom f or not f . y1 = f . y2 or y1 = y2 )
assume that
A23: y1 in dom f and
A24: y2 in dom f and
A25: f . y1 = f . y2 ; ::_thesis: y1 = y2
A26: y2 in dom F1 by A21, A24, FUNCT_2:def_1;
then A27: F1 " {(F2 . y2)} = {(f . y2)} by A14;
A28: y1 in dom F1 by A21, A23, FUNCT_2:def_1;
then F2 . y1 in rng F1 by A4, A7, A9, A10, A11, FUNCT_1:def_3;
then A29: {(F2 . y1)} c= rng F1 by ZFMISC_1:31;
F2 . y2 in rng F1 by A4, A7, A9, A10, A11, A26, FUNCT_1:def_3;
then A30: {(F2 . y2)} c= rng F1 by ZFMISC_1:31;
F1 " {(F2 . y1)} = {(f . y1)} by A14, A28;
then {(F2 . y1)} = {(F2 . y2)} by A25, A27, A29, A30, FUNCT_1:91;
then A31: F2 . y1 = F2 . y2 by ZFMISC_1:3;
( y1 in dom F2 & y2 in dom F2 ) by A9, A10, A11, A21, A23, A24, FUNCT_2:def_1;
hence y1 = y2 by A6, A31, FUNCT_1:def_4; ::_thesis: verum
end;
set G2 = L (#) F2;
A32: dom (L (#) F2) = Seg (len (L (#) F2)) by FINSEQ_1:def_3;
reconsider f = f as Permutation of (dom F1) by A15, A22, FUNCT_2:57;
( dom F1 = Seg (len F1) & dom (L (#) F1) = Seg (len (L (#) F1)) ) by FINSEQ_1:def_3;
then reconsider f = f as Permutation of (dom (L (#) F1)) by A20;
A33: len (L (#) F2) = len F2 by Def6;
A34: dom (L (#) F1) = Seg (len (L (#) F1)) by FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(L_(#)_F2)_holds_
(L_(#)_F2)_._i_=_(L_(#)_F1)_._(f_._i)
let i be Element of NAT ; ::_thesis: ( i in dom (L (#) F2) implies (L (#) F2) . i = (L (#) F1) . (f . i) )
assume A35: i in dom (L (#) F2) ; ::_thesis: (L (#) F2) . i = (L (#) F1) . (f . i)
then A36: ( (L (#) F2) . i = (F2 /. i) * (L . (F2 /. i)) & F2 . i = F2 /. i ) by A33, A11, A32, Def6, PARTFUN1:def_6;
i in dom F2 by A33, A35, FINSEQ_3:29;
then reconsider u = F2 . i as Vector of V by FINSEQ_2:11;
i in dom f by A9, A20, A33, A34, A32, A35, FUNCT_2:def_1;
then A37: f . i in dom F1 by A15, FUNCT_1:def_3;
then reconsider m = f . i as Element of NAT by A10;
reconsider v = F1 . m as Vector of V by A37, FINSEQ_2:11;
{(F1 . (f . i))} = Im (F1,(f . i)) by A37, FUNCT_1:59
.= F1 .: (F1 " {(F2 . i)}) by A9, A33, A10, A32, A14, A35 ;
then A38: u = v by FUNCT_1:75, ZFMISC_1:18;
F1 . m = F1 /. m by A37, PARTFUN1:def_6;
hence (L (#) F2) . i = (L (#) F1) . (f . i) by A20, A10, A34, A37, A38, A36, Def6; ::_thesis: verum
end;
hence v1 = v2 by A3, A4, A5, A6, A7, A8, A20, A33, FINSEQ_1:48, RLVECT_2:6; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines Sum RMOD_4:def_7_:_
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V
for b4 being Vector of V holds
( b4 = Sum L iff ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & b4 = Sum (L (#) F) ) );
Lm3: for R being Ring
for V being RightMod of R holds Sum (ZeroLC V) = 0. V
proof
let R be Ring; ::_thesis: for V being RightMod of R holds Sum (ZeroLC V) = 0. V
let V be RightMod of R; ::_thesis: Sum (ZeroLC V) = 0. V
consider F being FinSequence of V such that
F is one-to-one and
A1: rng F = Carrier (ZeroLC V) and
A2: Sum (ZeroLC V) = Sum ((ZeroLC V) (#) F) by Def7;
Carrier (ZeroLC V) = {} by Def4;
then F = {} by A1, RELAT_1:41;
then len F = 0 ;
then len ((ZeroLC V) (#) F) = 0 by Def6;
hence Sum (ZeroLC V) = 0. V by A2, RLVECT_1:75; ::_thesis: verum
end;
theorem Th29: :: RMOD_4:29
for R being Ring
for V being RightMod of R
for A being Subset of V st 0. R <> 1_ R holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
proof
let R be Ring; ::_thesis: for V being RightMod of R
for A being Subset of V st 0. R <> 1_ R holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
let V be RightMod of R; ::_thesis: for A being Subset of V st 0. R <> 1_ R holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
let A be Subset of V; ::_thesis: ( 0. R <> 1_ R implies ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) )
assume A1: 0. R <> 1_ R ; ::_thesis: ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
thus ( A <> {} & A is linearly-closed implies for l being Linear_Combination of A holds Sum l in A ) ::_thesis: ( ( for l being Linear_Combination of A holds Sum l in A ) implies ( A <> {} & A is linearly-closed ) )
proof
defpred S1[ Nat] means for l being Linear_Combination of A st card (Carrier l) = $1 holds
Sum l in A;
assume that
A2: A <> {} and
A3: A is linearly-closed ; ::_thesis: for l being Linear_Combination of A holds Sum l in A
now__::_thesis:_for_l_being_Linear_Combination_of_A_st_card_(Carrier_l)_=_0_holds_
Sum_l_in_A
let l be Linear_Combination of A; ::_thesis: ( card (Carrier l) = 0 implies Sum l in A )
assume card (Carrier l) = 0 ; ::_thesis: Sum l in A
then Carrier l = {} ;
then l = ZeroLC V by Def4;
then Sum l = 0. V by Lm3;
hence Sum l in A by A2, A3, RMOD_2:1; ::_thesis: verum
end;
then A4: S1[ 0 ] ;
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_l_being_Linear_Combination_of_A_st_card_(Carrier_l)_=_k_holds_
Sum_l_in_A_)_holds_
for_l_being_Linear_Combination_of_A_st_card_(Carrier_l)_=_k_+_1_holds_
Sum_l_in_A
let k be Element of NAT ; ::_thesis: ( ( for l being Linear_Combination of A st card (Carrier l) = k holds
Sum l in A ) implies for l being Linear_Combination of A st card (Carrier l) = k + 1 holds
Sum l in A )
assume A5: for l being Linear_Combination of A st card (Carrier l) = k holds
Sum l in A ; ::_thesis: for l being Linear_Combination of A st card (Carrier l) = k + 1 holds
Sum l in A
let l be Linear_Combination of A; ::_thesis: ( card (Carrier l) = k + 1 implies Sum l in A )
deffunc H1( Element of V) -> Element of the carrier of R = l . $1;
consider F being FinSequence of V such that
A6: F is one-to-one and
A7: rng F = Carrier l and
A8: Sum l = Sum (l (#) F) by Def7;
reconsider G = F | (Seg k) as FinSequence of V by FINSEQ_1:18;
assume A9: card (Carrier l) = k + 1 ; ::_thesis: Sum l in A
then A10: len F = k + 1 by A6, A7, FINSEQ_4:62;
then A11: len (l (#) F) = k + 1 by Def6;
A12: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A13: k + 1 in dom F by A10, FINSEQ_1:def_3;
k + 1 in dom F by A10, A12, FINSEQ_1:def_3;
then reconsider v = F . (k + 1) as Vector of V by FINSEQ_2:11;
consider f being Function of V,R such that
A14: f . v = 0. R and
A15: for u being Element of V st u <> v holds
f . u = H1(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
A16: v in Carrier l by A7, A13, FUNCT_1:def_3;
now__::_thesis:_for_u_being_Vector_of_V_st_not_u_in_Carrier_l_holds_
f_._u_=_0._R
let u be Vector of V; ::_thesis: ( not u in Carrier l implies f . u = 0. R )
assume A17: not u in Carrier l ; ::_thesis: f . u = 0. R
hence f . u = l . u by A16, A15
.= 0. R by A17 ;
::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def2;
A18: A \ {v} c= A by XBOOLE_1:36;
A19: Carrier l c= A by Def5;
then A20: v * (l . v) in A by A3, A16, RMOD_2:def_1;
A21: Carrier f = (Carrier l) \ {v}
proof
thus Carrier f c= (Carrier l) \ {v} :: according to XBOOLE_0:def_10 ::_thesis: (Carrier l) \ {v} c= Carrier f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in (Carrier l) \ {v} )
assume x in Carrier f ; ::_thesis: x in (Carrier l) \ {v}
then consider u being Vector of V such that
A22: u = x and
A23: f . u <> 0. R ;
f . u = l . u by A14, A15, A23;
then A24: x in Carrier l by A22, A23;
not x in {v} by A14, A22, A23, TARSKI:def_1;
hence x in (Carrier l) \ {v} by A24, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Carrier l) \ {v} or x in Carrier f )
assume A25: x in (Carrier l) \ {v} ; ::_thesis: x in Carrier f
then x in Carrier l by XBOOLE_0:def_5;
then consider u being Vector of V such that
A26: x = u and
A27: l . u <> 0. R ;
not x in {v} by A25, XBOOLE_0:def_5;
then x <> v by TARSKI:def_1;
then l . u = f . u by A15, A26;
hence x in Carrier f by A26, A27; ::_thesis: verum
end;
then Carrier f c= A \ {v} by A19, XBOOLE_1:33;
then Carrier f c= A by A18, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by Def5;
A28: len G = k by A10, FINSEQ_3:53;
then A29: len (f (#) G) = k by Def6;
A30: rng G = Carrier f
proof
thus rng G c= Carrier f :: according to XBOOLE_0:def_10 ::_thesis: Carrier f c= rng G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in Carrier f )
assume x in rng G ; ::_thesis: x in Carrier f
then consider y being set such that
A31: y in dom G and
A32: G . y = x by FUNCT_1:def_3;
reconsider y = y as Nat by A31, FINSEQ_3:23;
A33: ( dom G c= dom F & G . y = F . y ) by A31, FUNCT_1:47, RELAT_1:60;
now__::_thesis:_not_x_=_v
assume x = v ; ::_thesis: contradiction
then A34: k + 1 = y by A6, A13, A31, A32, A33, FUNCT_1:def_4;
y <= k by A28, A31, FINSEQ_3:25;
hence contradiction by A34, XREAL_1:29; ::_thesis: verum
end;
then A35: not x in {v} by TARSKI:def_1;
x in rng F by A31, A32, A33, FUNCT_1:def_3;
hence x in Carrier f by A7, A21, A35, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in rng G )
assume A36: x in Carrier f ; ::_thesis: x in rng G
then x in rng F by A7, A21, XBOOLE_0:def_5;
then consider y being set such that
A37: y in dom F and
A38: F . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A37, FINSEQ_3:23;
now__::_thesis:_y_in_Seg_k
assume not y in Seg k ; ::_thesis: contradiction
then y in (dom F) \ (Seg k) by A37, XBOOLE_0:def_5;
then y in (Seg (k + 1)) \ (Seg k) by A10, FINSEQ_1:def_3;
then y in {(k + 1)} by FINSEQ_3:15;
then y = k + 1 by TARSKI:def_1;
then not v in {v} by A21, A36, A38, XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
then y in (dom F) /\ (Seg k) by A37, XBOOLE_0:def_4;
then A39: y in dom G by RELAT_1:61;
then G . y = F . y by FUNCT_1:47;
hence x in rng G by A38, A39, FUNCT_1:def_3; ::_thesis: verum
end;
(Seg (k + 1)) /\ (Seg k) = Seg k by FINSEQ_1:7, NAT_1:12
.= dom (f (#) G) by A29, FINSEQ_1:def_3 ;
then A40: dom (f (#) G) = (dom (l (#) F)) /\ (Seg k) by A11, FINSEQ_1:def_3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_(#)_G)_holds_
(f_(#)_G)_._x_=_(l_(#)_F)_._x
let x be set ; ::_thesis: ( x in dom (f (#) G) implies (f (#) G) . x = (l (#) F) . x )
A41: rng F c= the carrier of V by FINSEQ_1:def_4;
assume A42: x in dom (f (#) G) ; ::_thesis: (f (#) G) . x = (l (#) F) . x
then reconsider n = x as Nat by FINSEQ_3:23;
n in dom (l (#) F) by A40, A42, XBOOLE_0:def_4;
then A43: n in dom F by A10, A11, FINSEQ_3:29;
then F . n in rng F by FUNCT_1:def_3;
then reconsider w = F . n as Vector of V by A41;
A44: n in dom G by A28, A29, A42, FINSEQ_3:29;
then A45: G . n in rng G by FUNCT_1:def_3;
rng G c= the carrier of V by FINSEQ_1:def_4;
then reconsider u = G . n as Vector of V by A45;
not u in {v} by A21, A30, A45, XBOOLE_0:def_5;
then A46: u <> v by TARSKI:def_1;
A47: (f (#) G) . n = u * (f . u) by A44, Th23
.= u * (l . u) by A15, A46 ;
w = u by A44, FUNCT_1:47;
hence (f (#) G) . x = (l (#) F) . x by A47, A43, Th23; ::_thesis: verum
end;
then f (#) G = (l (#) F) | (Seg k) by A40, FUNCT_1:46;
then A48: f (#) G = (l (#) F) | (dom (f (#) G)) by A29, FINSEQ_1:def_3;
v in rng F by A13, FUNCT_1:def_3;
then {v} c= Carrier l by A7, ZFMISC_1:31;
then card (Carrier f) = (k + 1) - (card {v}) by A9, A21, CARD_2:44
.= (k + 1) - 1 by CARD_1:30
.= k by XCMPLX_1:26 ;
then A49: Sum f in A by A5;
G is one-to-one by A6, FUNCT_1:52;
then A50: Sum (f (#) G) = Sum f by A30, Def7;
(l (#) F) . (len F) = v * (l . v) by A10, A13, Th23;
then Sum (l (#) F) = (Sum (f (#) G)) + (v * (l . v)) by A10, A11, A29, A48, RLVECT_1:38;
hence Sum l in A by A3, A8, A20, A50, A49, RMOD_2:def_1; ::_thesis: verum
end;
then A51: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
let l be Linear_Combination of A; ::_thesis: Sum l in A
A52: card (Carrier l) = card (Carrier l) ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A51);
hence Sum l in A by A52; ::_thesis: verum
end;
assume A53: for l being Linear_Combination of A holds Sum l in A ; ::_thesis: ( A <> {} & A is linearly-closed )
hence A <> {} ; ::_thesis: A is linearly-closed
( ZeroLC V is Linear_Combination of A & Sum (ZeroLC V) = 0. V ) by Lm3, Th20;
then A54: 0. V in A by A53;
A55: for a being Scalar of R
for v being Vector of V st v in A holds
v * a in A
proof
let a be Scalar of R; ::_thesis: for v being Vector of V st v in A holds
v * a in A
let v be Vector of V; ::_thesis: ( v in A implies v * a in A )
assume A56: v in A ; ::_thesis: v * a in A
now__::_thesis:_v_*_a_in_A
percases ( a = 0. R or a <> 0. R ) ;
suppose a = 0. R ; ::_thesis: v * a in A
hence v * a in A by A54, VECTSP_2:32; ::_thesis: verum
end;
supposeA57: a <> 0. R ; ::_thesis: v * a in A
deffunc H1( Element of V) -> Element of the carrier of R = 0. R;
consider f being Function of V,R such that
A58: f . v = a and
A59: for u being Element of V st u <> v holds
f . u = H1(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
now__::_thesis:_for_u_being_Vector_of_V_st_not_u_in_{v}_holds_
f_._u_=_0._R
let u be Vector of V; ::_thesis: ( not u in {v} implies f . u = 0. R )
assume not u in {v} ; ::_thesis: f . u = 0. R
then u <> v by TARSKI:def_1;
hence f . u = 0. R by A59; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def2;
A60: Carrier f = {v}
proof
thus Carrier f c= {v} :: according to XBOOLE_0:def_10 ::_thesis: {v} c= Carrier f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume x in Carrier f ; ::_thesis: x in {v}
then consider u being Vector of V such that
A61: x = u and
A62: f . u <> 0. R ;
u = v by A59, A62;
hence x in {v} by A61, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in Carrier f )
assume x in {v} ; ::_thesis: x in Carrier f
then x = v by TARSKI:def_1;
hence x in Carrier f by A57, A58; ::_thesis: verum
end;
{v} c= A by A56, ZFMISC_1:31;
then reconsider f = f as Linear_Combination of A by A60, Def5;
consider F being FinSequence of V such that
A63: ( F is one-to-one & rng F = Carrier f ) and
A64: Sum (f (#) F) = Sum f by Def7;
F = <*v*> by A60, A63, FINSEQ_3:97;
then f (#) F = <*(v * (f . v))*> by Th25;
then Sum f = v * a by A58, A64, RLVECT_1:44;
hence v * a in A by A53; ::_thesis: verum
end;
end;
end;
hence v * a in A ; ::_thesis: verum
end;
thus for v, u being Vector of V st v in A & u in A holds
v + u in A :: according to RMOD_2:def_1 ::_thesis: for b1 being Element of the carrier of R
for b2 being Element of the carrier of V holds
( not b2 in A or b2 * b1 in A )
proof
let v, u be Vector of V; ::_thesis: ( v in A & u in A implies v + u in A )
assume that
A65: v in A and
A66: u in A ; ::_thesis: v + u in A
now__::_thesis:_v_+_u_in_A
percases ( u = v or v <> u ) ;
suppose u = v ; ::_thesis: v + u in A
then v + u = (v * (1_ R)) + v by VECTSP_2:def_9
.= (v * (1_ R)) + (v * (1_ R)) by VECTSP_2:def_9
.= v * ((1_ R) + (1_ R)) by VECTSP_2:def_9 ;
hence v + u in A by A55, A65; ::_thesis: verum
end;
supposeA67: v <> u ; ::_thesis: v + u in A
deffunc H1( Element of V) -> Element of the carrier of R = 0. R;
consider f being Function of V,R such that
A68: ( f . v = 1_ R & f . u = 1_ R ) and
A69: for w being Element of V st w <> v & w <> u holds
f . w = H1(w) from FUNCT_2:sch_7(A67);
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
now__::_thesis:_for_w_being_Vector_of_V_st_not_w_in_{v,u}_holds_
f_._w_=_0._R
let w be Vector of V; ::_thesis: ( not w in {v,u} implies f . w = 0. R )
assume not w in {v,u} ; ::_thesis: f . w = 0. R
then ( w <> v & w <> u ) by TARSKI:def_2;
hence f . w = 0. R by A69; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def2;
A70: Carrier f = {v,u}
proof
thus Carrier f c= {v,u} :: according to XBOOLE_0:def_10 ::_thesis: {v,u} c= Carrier f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v,u} )
assume x in Carrier f ; ::_thesis: x in {v,u}
then ex w being Vector of V st
( x = w & f . w <> 0. R ) ;
then ( x = v or x = u ) by A69;
hence x in {v,u} by TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v,u} or x in Carrier f )
assume x in {v,u} ; ::_thesis: x in Carrier f
then ( x = v or x = u ) by TARSKI:def_2;
hence x in Carrier f by A1, A68; ::_thesis: verum
end;
then A71: Carrier f c= A by A65, A66, ZFMISC_1:32;
A72: ( u * (1_ R) = u & v * (1_ R) = v ) by VECTSP_2:def_9;
reconsider f = f as Linear_Combination of A by A71, Def5;
consider F being FinSequence of V such that
A73: ( F is one-to-one & rng F = Carrier f ) and
A74: Sum (f (#) F) = Sum f by Def7;
( F = <*v,u*> or F = <*u,v*> ) by A67, A70, A73, FINSEQ_3:99;
then ( f (#) F = <*(v * (1_ R)),(u * (1_ R))*> or f (#) F = <*(u * (1_ R)),(v * (1_ R))*> ) by A68, Th26;
then Sum f = v + u by A74, A72, RLVECT_1:45;
hence v + u in A by A53; ::_thesis: verum
end;
end;
end;
hence v + u in A ; ::_thesis: verum
end;
thus for b1 being Element of the carrier of R
for b2 being Element of the carrier of V holds
( not b2 in A or b2 * b1 in A ) by A55; ::_thesis: verum
end;
theorem :: RMOD_4:30
for R being Ring
for V being RightMod of R holds Sum (ZeroLC V) = 0. V by Lm3;
theorem Th31: :: RMOD_4:31
for R being Ring
for V being RightMod of R
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V
proof
let R be Ring; ::_thesis: for V being RightMod of R
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V
let V be RightMod of R; ::_thesis: for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V
let l be Linear_Combination of {} the carrier of V; ::_thesis: Sum l = 0. V
l = ZeroLC V by Th21;
hence Sum l = 0. V by Lm3; ::_thesis: verum
end;
theorem Th32: :: RMOD_4:32
for R being Ring
for V being RightMod of R
for v being Vector of V
for l being Linear_Combination of {v} holds Sum l = v * (l . v)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v being Vector of V
for l being Linear_Combination of {v} holds Sum l = v * (l . v)
let V be RightMod of R; ::_thesis: for v being Vector of V
for l being Linear_Combination of {v} holds Sum l = v * (l . v)
let v be Vector of V; ::_thesis: for l being Linear_Combination of {v} holds Sum l = v * (l . v)
let l be Linear_Combination of {v}; ::_thesis: Sum l = v * (l . v)
A1: Carrier l c= {v} by Def5;
now__::_thesis:_Sum_l_=_v_*_(l_._v)
percases ( Carrier l = {} or Carrier l = {v} ) by A1, ZFMISC_1:33;
suppose Carrier l = {} ; ::_thesis: Sum l = v * (l . v)
then A2: l = ZeroLC V by Def4;
hence Sum l = 0. V by Lm3
.= v * (0. R) by VECTSP_2:32
.= v * (l . v) by A2, Th18 ;
::_thesis: verum
end;
suppose Carrier l = {v} ; ::_thesis: Sum l = v * (l . v)
then consider F being FinSequence of V such that
A3: ( F is one-to-one & rng F = {v} ) and
A4: Sum l = Sum (l (#) F) by Def7;
F = <*v*> by A3, FINSEQ_3:97;
then l (#) F = <*(v * (l . v))*> by Th25;
hence Sum l = v * (l . v) by A4, RLVECT_1:44; ::_thesis: verum
end;
end;
end;
hence Sum l = v * (l . v) ; ::_thesis: verum
end;
theorem Th33: :: RMOD_4:33
for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v1, v2 being Vector of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
let V be RightMod of R; ::_thesis: for v1, v2 being Vector of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
let v1, v2 be Vector of V; ::_thesis: ( v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) )
assume A1: v1 <> v2 ; ::_thesis: for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
let l be Linear_Combination of {v1,v2}; ::_thesis: Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
A2: Carrier l c= {v1,v2} by Def5;
now__::_thesis:_Sum_l_=_(v1_*_(l_._v1))_+_(v2_*_(l_._v2))
percases ( Carrier l = {} or Carrier l = {v1} or Carrier l = {v2} or Carrier l = {v1,v2} ) by A2, ZFMISC_1:36;
suppose Carrier l = {} ; ::_thesis: Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
then A3: l = ZeroLC V by Def4;
hence Sum l = 0. V by Lm3
.= (0. V) + (0. V) by RLVECT_1:def_4
.= (v1 * (0. R)) + (0. V) by VECTSP_2:32
.= (v1 * (0. R)) + (v2 * (0. R)) by VECTSP_2:32
.= (v1 * (l . v1)) + (v2 * (0. R)) by A3, Th18
.= (v1 * (l . v1)) + (v2 * (l . v2)) by A3, Th18 ;
::_thesis: verum
end;
supposeA4: Carrier l = {v1} ; ::_thesis: Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
then reconsider L = l as Linear_Combination of {v1} by Def5;
A5: not v2 in Carrier l by A1, A4, TARSKI:def_1;
thus Sum l = Sum L
.= v1 * (l . v1) by Th32
.= (v1 * (l . v1)) + (0. V) by RLVECT_1:def_4
.= (v1 * (l . v1)) + (v2 * (0. R)) by VECTSP_2:32
.= (v1 * (l . v1)) + (v2 * (l . v2)) by A5 ; ::_thesis: verum
end;
supposeA6: Carrier l = {v2} ; ::_thesis: Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
then reconsider L = l as Linear_Combination of {v2} by Def5;
A7: not v1 in Carrier l by A1, A6, TARSKI:def_1;
thus Sum l = Sum L
.= v2 * (l . v2) by Th32
.= (0. V) + (v2 * (l . v2)) by RLVECT_1:def_4
.= (v1 * (0. R)) + (v2 * (l . v2)) by VECTSP_2:32
.= (v1 * (l . v1)) + (v2 * (l . v2)) by A7 ; ::_thesis: verum
end;
suppose Carrier l = {v1,v2} ; ::_thesis: Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
then consider F being FinSequence of V such that
A8: ( F is one-to-one & rng F = {v1,v2} ) and
A9: Sum l = Sum (l (#) F) by Def7;
( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A8, FINSEQ_3:99;
then ( l (#) F = <*(v1 * (l . v1)),(v2 * (l . v2))*> or l (#) F = <*(v2 * (l . v2)),(v1 * (l . v1))*> ) by Th26;
hence Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) by A9, RLVECT_1:45; ::_thesis: verum
end;
end;
end;
hence Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) ; ::_thesis: verum
end;
theorem :: RMOD_4:34
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V
proof
let R be Ring; ::_thesis: for V being RightMod of R
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V
let V be RightMod of R; ::_thesis: for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V
let L be Linear_Combination of V; ::_thesis: ( Carrier L = {} implies Sum L = 0. V )
assume Carrier L = {} ; ::_thesis: Sum L = 0. V
then L = ZeroLC V by Def4;
hence Sum L = 0. V by Lm3; ::_thesis: verum
end;
theorem Th35: :: RMOD_4:35
for R being Ring
for V being RightMod of R
for v being Vector of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = v * (L . v)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v being Vector of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = v * (L . v)
let V be RightMod of R; ::_thesis: for v being Vector of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = v * (L . v)
let v be Vector of V; ::_thesis: for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = v * (L . v)
let L be Linear_Combination of V; ::_thesis: ( Carrier L = {v} implies Sum L = v * (L . v) )
assume Carrier L = {v} ; ::_thesis: Sum L = v * (L . v)
then L is Linear_Combination of {v} by Def5;
hence Sum L = v * (L . v) by Th32; ::_thesis: verum
end;
theorem :: RMOD_4:36
for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V
for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = (v1 * (L . v1)) + (v2 * (L . v2))
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v1, v2 being Vector of V
for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = (v1 * (L . v1)) + (v2 * (L . v2))
let V be RightMod of R; ::_thesis: for v1, v2 being Vector of V
for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = (v1 * (L . v1)) + (v2 * (L . v2))
let v1, v2 be Vector of V; ::_thesis: for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = (v1 * (L . v1)) + (v2 * (L . v2))
let L be Linear_Combination of V; ::_thesis: ( Carrier L = {v1,v2} & v1 <> v2 implies Sum L = (v1 * (L . v1)) + (v2 * (L . v2)) )
assume that
A1: Carrier L = {v1,v2} and
A2: v1 <> v2 ; ::_thesis: Sum L = (v1 * (L . v1)) + (v2 * (L . v2))
L is Linear_Combination of {v1,v2} by A1, Def5;
hence Sum L = (v1 * (L . v1)) + (v2 * (L . v2)) by A2, Th33; ::_thesis: verum
end;
definition
let R be Ring;
let V be RightMod of R;
let L1, L2 be Linear_Combination of V;
:: original: =
redefine predL1 = L2 means :: RMOD_4:def 8
for v being Vector of V holds L1 . v = L2 . v;
compatibility
( L1 = L2 iff for v being Vector of V holds L1 . v = L2 . v ) by FUNCT_2:63;
end;
:: deftheorem defines = RMOD_4:def_8_:_
for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds
( L1 = L2 iff for v being Vector of V holds L1 . v = L2 . v );
definition
let R be Ring;
let V be RightMod of R;
let L1, L2 be Linear_Combination of V;
funcL1 + L2 -> Linear_Combination of V means :Def9: :: RMOD_4:def 9
for v being Vector of V holds it . v = (L1 . v) + (L2 . v);
existence
ex b1 being Linear_Combination of V st
for v being Vector of V holds b1 . v = (L1 . v) + (L2 . v)
proof
deffunc H1( Element of V) -> Element of the carrier of R = (L1 . $1) + (L2 . $1);
consider f being Function of V,R such that
A1: for v being Element of V holds f . v = H1(v) from FUNCT_2:sch_4();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
now__::_thesis:_for_v_being_Vector_of_V_st_not_v_in_(Carrier_L1)_\/_(Carrier_L2)_holds_
f_._v_=_0._R
let v be Vector of V; ::_thesis: ( not v in (Carrier L1) \/ (Carrier L2) implies f . v = 0. R )
assume A2: not v in (Carrier L1) \/ (Carrier L2) ; ::_thesis: f . v = 0. R
then not v in Carrier L2 by XBOOLE_0:def_3;
then A3: L2 . v = 0. R ;
not v in Carrier L1 by A2, XBOOLE_0:def_3;
then L1 . v = 0. R ;
hence f . v = (0. R) + (0. R) by A1, A3
.= 0. R by RLVECT_1:4 ;
::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def2;
take f ; ::_thesis: for v being Vector of V holds f . v = (L1 . v) + (L2 . v)
let v be Vector of V; ::_thesis: f . v = (L1 . v) + (L2 . v)
thus f . v = (L1 . v) + (L2 . v) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Linear_Combination of V st ( for v being Vector of V holds b1 . v = (L1 . v) + (L2 . v) ) & ( for v being Vector of V holds b2 . v = (L1 . v) + (L2 . v) ) holds
b1 = b2
proof
let M, N be Linear_Combination of V; ::_thesis: ( ( for v being Vector of V holds M . v = (L1 . v) + (L2 . v) ) & ( for v being Vector of V holds N . v = (L1 . v) + (L2 . v) ) implies M = N )
assume A4: for v being Vector of V holds M . v = (L1 . v) + (L2 . v) ; ::_thesis: ( ex v being Vector of V st not N . v = (L1 . v) + (L2 . v) or M = N )
assume A5: for v being Vector of V holds N . v = (L1 . v) + (L2 . v) ; ::_thesis: M = N
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: M . v = N . v
thus M . v = (L1 . v) + (L2 . v) by A4
.= N . v by A5 ; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines + RMOD_4:def_9_:_
for R being Ring
for V being RightMod of R
for L1, L2, b5 being Linear_Combination of V holds
( b5 = L1 + L2 iff for v being Vector of V holds b5 . v = (L1 . v) + (L2 . v) );
theorem Th37: :: RMOD_4:37
for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
let V be RightMod of R; ::_thesis: for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
let L1, L2 be Linear_Combination of V; ::_thesis: Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier (L1 + L2) or x in (Carrier L1) \/ (Carrier L2) )
assume x in Carrier (L1 + L2) ; ::_thesis: x in (Carrier L1) \/ (Carrier L2)
then consider u being Vector of V such that
A1: x = u and
A2: (L1 + L2) . u <> 0. R ;
(L1 + L2) . u = (L1 . u) + (L2 . u) by Def9;
then ( L1 . u <> 0. R or L2 . u <> 0. R ) by A2, RLVECT_1:4;
then ( x in { v1 where v1 is Vector of V : L1 . v1 <> 0. R } or x in { v2 where v2 is Vector of V : L2 . v2 <> 0. R } ) by A1;
hence x in (Carrier L1) \/ (Carrier L2) by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th38: :: RMOD_4:38
for R being Ring
for V being RightMod of R
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 + L2 is Linear_Combination of A
proof
let R be Ring; ::_thesis: for V being RightMod of R
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 + L2 is Linear_Combination of A
let V be RightMod of R; ::_thesis: for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 + L2 is Linear_Combination of A
let A be Subset of V; ::_thesis: for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 + L2 is Linear_Combination of A
let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 is Linear_Combination of A & L2 is Linear_Combination of A implies L1 + L2 is Linear_Combination of A )
assume ( L1 is Linear_Combination of A & L2 is Linear_Combination of A ) ; ::_thesis: L1 + L2 is Linear_Combination of A
then ( Carrier L1 c= A & Carrier L2 c= A ) by Def5;
then A1: (Carrier L1) \/ (Carrier L2) c= A by XBOOLE_1:8;
Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) by Th37;
hence Carrier (L1 + L2) c= A by A1, XBOOLE_1:1; :: according to RMOD_4:def_5 ::_thesis: verum
end;
theorem Th39: :: RMOD_4:39
for R being comRing
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1
proof
let R be comRing; ::_thesis: for V being RightMod of R
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1
let V be RightMod of R; ::_thesis: for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1
let L1, L2 be Linear_Combination of V; ::_thesis: L1 + L2 = L2 + L1
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L1 + L2) . v = (L2 + L1) . v
thus (L1 + L2) . v = (L2 . v) + (L1 . v) by Def9
.= (L2 + L1) . v by Def9 ; ::_thesis: verum
end;
theorem :: RMOD_4:40
for R being Ring
for V being RightMod of R
for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3
proof
let R be Ring; ::_thesis: for V being RightMod of R
for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3
let V be RightMod of R; ::_thesis: for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3
let L1, L2, L3 be Linear_Combination of V; ::_thesis: L1 + (L2 + L3) = (L1 + L2) + L3
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L1 + (L2 + L3)) . v = ((L1 + L2) + L3) . v
thus (L1 + (L2 + L3)) . v = (L1 . v) + ((L2 + L3) . v) by Def9
.= (L1 . v) + ((L2 . v) + (L3 . v)) by Def9
.= ((L1 . v) + (L2 . v)) + (L3 . v) by RLVECT_1:def_3
.= ((L1 + L2) . v) + (L3 . v) by Def9
.= ((L1 + L2) + L3) . v by Def9 ; ::_thesis: verum
end;
theorem :: RMOD_4:41
for R being comRing
for V being RightMod of R
for L being Linear_Combination of V holds
( L + (ZeroLC V) = L & (ZeroLC V) + L = L )
proof
let R be comRing; ::_thesis: for V being RightMod of R
for L being Linear_Combination of V holds
( L + (ZeroLC V) = L & (ZeroLC V) + L = L )
let V be RightMod of R; ::_thesis: for L being Linear_Combination of V holds
( L + (ZeroLC V) = L & (ZeroLC V) + L = L )
let L be Linear_Combination of V; ::_thesis: ( L + (ZeroLC V) = L & (ZeroLC V) + L = L )
thus L + (ZeroLC V) = L ::_thesis: (ZeroLC V) + L = L
proof
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L + (ZeroLC V)) . v = L . v
thus (L + (ZeroLC V)) . v = (L . v) + ((ZeroLC V) . v) by Def9
.= (L . v) + (0. R) by Th18
.= L . v by RLVECT_1:4 ; ::_thesis: verum
end;
hence (ZeroLC V) + L = L by Th39; ::_thesis: verum
end;
definition
let R be Ring;
let V be RightMod of R;
let a be Scalar of R;
let L be Linear_Combination of V;
funcL * a -> Linear_Combination of V means :Def10: :: RMOD_4:def 10
for v being Vector of V holds it . v = (L . v) * a;
existence
ex b1 being Linear_Combination of V st
for v being Vector of V holds b1 . v = (L . v) * a
proof
deffunc H1( Element of V) -> Element of the carrier of R = (L . $1) * a;
consider f being Function of V,R such that
A1: for v being Element of V holds f . v = H1(v) from FUNCT_2:sch_4();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
now__::_thesis:_for_v_being_Vector_of_V_st_not_v_in_Carrier_L_holds_
f_._v_=_0._R
let v be Vector of V; ::_thesis: ( not v in Carrier L implies f . v = 0. R )
assume not v in Carrier L ; ::_thesis: f . v = 0. R
then L . v = 0. R ;
hence f . v = (0. R) * a by A1
.= 0. R by VECTSP_1:7 ;
::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def2;
take f ; ::_thesis: for v being Vector of V holds f . v = (L . v) * a
let v be Vector of V; ::_thesis: f . v = (L . v) * a
thus f . v = (L . v) * a by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Linear_Combination of V st ( for v being Vector of V holds b1 . v = (L . v) * a ) & ( for v being Vector of V holds b2 . v = (L . v) * a ) holds
b1 = b2
proof
let L1, L2 be Linear_Combination of V; ::_thesis: ( ( for v being Vector of V holds L1 . v = (L . v) * a ) & ( for v being Vector of V holds L2 . v = (L . v) * a ) implies L1 = L2 )
assume A2: for v being Vector of V holds L1 . v = (L . v) * a ; ::_thesis: ( ex v being Vector of V st not L2 . v = (L . v) * a or L1 = L2 )
assume A3: for v being Vector of V holds L2 . v = (L . v) * a ; ::_thesis: L1 = L2
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: L1 . v = L2 . v
thus L1 . v = (L . v) * a by A2
.= L2 . v by A3 ; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines * RMOD_4:def_10_:_
for R being Ring
for V being RightMod of R
for a being Scalar of R
for L, b5 being Linear_Combination of V holds
( b5 = L * a iff for v being Vector of V holds b5 . v = (L . v) * a );
theorem Th42: :: RMOD_4:42
for R being Ring
for V being RightMod of R
for a being Scalar of R
for L being Linear_Combination of V holds Carrier (L * a) c= Carrier L
proof
let R be Ring; ::_thesis: for V being RightMod of R
for a being Scalar of R
for L being Linear_Combination of V holds Carrier (L * a) c= Carrier L
let V be RightMod of R; ::_thesis: for a being Scalar of R
for L being Linear_Combination of V holds Carrier (L * a) c= Carrier L
let a be Scalar of R; ::_thesis: for L being Linear_Combination of V holds Carrier (L * a) c= Carrier L
let L be Linear_Combination of V; ::_thesis: Carrier (L * a) c= Carrier L
set T = { u where u is Vector of V : (L * a) . u <> 0. R } ;
set S = { v where v is Vector of V : L . v <> 0. R } ;
{ u where u is Vector of V : (L * a) . u <> 0. R } c= { v where v is Vector of V : L . v <> 0. R }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Vector of V : (L * a) . u <> 0. R } or x in { v where v is Vector of V : L . v <> 0. R } )
assume x in { u where u is Vector of V : (L * a) . u <> 0. R } ; ::_thesis: x in { v where v is Vector of V : L . v <> 0. R }
then consider u being Vector of V such that
A1: x = u and
A2: (L * a) . u <> 0. R ;
(L * a) . u = (L . u) * a by Def10;
then L . u <> 0. R by A2, VECTSP_1:7;
hence x in { v where v is Vector of V : L . v <> 0. R } by A1; ::_thesis: verum
end;
hence Carrier (L * a) c= Carrier L ; ::_thesis: verum
end;
theorem Th43: :: RMOD_4:43
for RR being domRing
for VV being RightMod of RR
for LL being Linear_Combination of VV
for aa being Scalar of RR st aa <> 0. RR holds
Carrier (LL * aa) = Carrier LL
proof
let RR be domRing; ::_thesis: for VV being RightMod of RR
for LL being Linear_Combination of VV
for aa being Scalar of RR st aa <> 0. RR holds
Carrier (LL * aa) = Carrier LL
let VV be RightMod of RR; ::_thesis: for LL being Linear_Combination of VV
for aa being Scalar of RR st aa <> 0. RR holds
Carrier (LL * aa) = Carrier LL
let LL be Linear_Combination of VV; ::_thesis: for aa being Scalar of RR st aa <> 0. RR holds
Carrier (LL * aa) = Carrier LL
let aa be Scalar of RR; ::_thesis: ( aa <> 0. RR implies Carrier (LL * aa) = Carrier LL )
set T = { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } ;
set S = { vv where vv is Vector of VV : LL . vv <> 0. RR } ;
assume A1: aa <> 0. RR ; ::_thesis: Carrier (LL * aa) = Carrier LL
{ uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } = { vv where vv is Vector of VV : LL . vv <> 0. RR }
proof
thus { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } c= { vv where vv is Vector of VV : LL . vv <> 0. RR } :: according to XBOOLE_0:def_10 ::_thesis: { vv where vv is Vector of VV : LL . vv <> 0. RR } c= { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } or x in { vv where vv is Vector of VV : LL . vv <> 0. RR } )
assume x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } ; ::_thesis: x in { vv where vv is Vector of VV : LL . vv <> 0. RR }
then consider uu being Vector of VV such that
A2: x = uu and
A3: (LL * aa) . uu <> 0. RR ;
(LL * aa) . uu = (LL . uu) * aa by Def10;
then LL . uu <> 0. RR by A3, VECTSP_1:6;
hence x in { vv where vv is Vector of VV : LL . vv <> 0. RR } by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { vv where vv is Vector of VV : LL . vv <> 0. RR } or x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } )
assume x in { vv where vv is Vector of VV : LL . vv <> 0. RR } ; ::_thesis: x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR }
then consider vv being Vector of VV such that
A4: x = vv and
A5: LL . vv <> 0. RR ;
(LL * aa) . vv = (LL . vv) * aa by Def10;
then (LL * aa) . vv <> 0. RR by A1, A5, VECTSP_2:def_1;
hence x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } by A4; ::_thesis: verum
end;
hence Carrier (LL * aa) = Carrier LL ; ::_thesis: verum
end;
theorem Th44: :: RMOD_4:44
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds L * (0. R) = ZeroLC V
proof
let R be Ring; ::_thesis: for V being RightMod of R
for L being Linear_Combination of V holds L * (0. R) = ZeroLC V
let V be RightMod of R; ::_thesis: for L being Linear_Combination of V holds L * (0. R) = ZeroLC V
let L be Linear_Combination of V; ::_thesis: L * (0. R) = ZeroLC V
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L * (0. R)) . v = (ZeroLC V) . v
thus (L * (0. R)) . v = (L . v) * (0. R) by Def10
.= 0. R by VECTSP_1:6
.= (ZeroLC V) . v by Th18 ; ::_thesis: verum
end;
theorem Th45: :: RMOD_4:45
for R being Ring
for V being RightMod of R
for a being Scalar of R
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
L * a is Linear_Combination of A
proof
let R be Ring; ::_thesis: for V being RightMod of R
for a being Scalar of R
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
L * a is Linear_Combination of A
let V be RightMod of R; ::_thesis: for a being Scalar of R
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
L * a is Linear_Combination of A
let a be Scalar of R; ::_thesis: for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
L * a is Linear_Combination of A
let A be Subset of V; ::_thesis: for L being Linear_Combination of V st L is Linear_Combination of A holds
L * a is Linear_Combination of A
let L be Linear_Combination of V; ::_thesis: ( L is Linear_Combination of A implies L * a is Linear_Combination of A )
assume L is Linear_Combination of A ; ::_thesis: L * a is Linear_Combination of A
then A1: Carrier L c= A by Def5;
Carrier (L * a) c= Carrier L by Th42;
then Carrier (L * a) c= A by A1, XBOOLE_1:1;
hence L * a is Linear_Combination of A by Def5; ::_thesis: verum
end;
theorem :: RMOD_4:46
for R being Ring
for V being RightMod of R
for a, b being Scalar of R
for L being Linear_Combination of V holds L * (a + b) = (L * a) + (L * b)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for a, b being Scalar of R
for L being Linear_Combination of V holds L * (a + b) = (L * a) + (L * b)
let V be RightMod of R; ::_thesis: for a, b being Scalar of R
for L being Linear_Combination of V holds L * (a + b) = (L * a) + (L * b)
let a, b be Scalar of R; ::_thesis: for L being Linear_Combination of V holds L * (a + b) = (L * a) + (L * b)
let L be Linear_Combination of V; ::_thesis: L * (a + b) = (L * a) + (L * b)
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L * (a + b)) . v = ((L * a) + (L * b)) . v
thus (L * (a + b)) . v = (L . v) * (a + b) by Def10
.= ((L . v) * a) + ((L . v) * b) by VECTSP_1:def_7
.= ((L * a) . v) + ((L . v) * b) by Def10
.= ((L * a) . v) + ((L * b) . v) by Def10
.= ((L * a) + (L * b)) . v by Def9 ; ::_thesis: verum
end;
theorem :: RMOD_4:47
for R being Ring
for V being RightMod of R
for a being Scalar of R
for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for a being Scalar of R
for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a)
let V be RightMod of R; ::_thesis: for a being Scalar of R
for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a)
let a be Scalar of R; ::_thesis: for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a)
let L1, L2 be Linear_Combination of V; ::_thesis: (L1 + L2) * a = (L1 * a) + (L2 * a)
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: ((L1 + L2) * a) . v = ((L1 * a) + (L2 * a)) . v
thus ((L1 + L2) * a) . v = ((L1 + L2) . v) * a by Def10
.= ((L1 . v) + (L2 . v)) * a by Def9
.= ((L1 . v) * a) + ((L2 . v) * a) by VECTSP_1:def_7
.= ((L1 * a) . v) + ((L2 . v) * a) by Def10
.= ((L1 * a) . v) + ((L2 * a) . v) by Def10
.= ((L1 * a) + (L2 * a)) . v by Def9 ; ::_thesis: verum
end;
theorem Th48: :: RMOD_4:48
for R being Ring
for V being RightMod of R
for b, a being Scalar of R
for L being Linear_Combination of V holds (L * b) * a = L * (b * a)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for b, a being Scalar of R
for L being Linear_Combination of V holds (L * b) * a = L * (b * a)
let V be RightMod of R; ::_thesis: for b, a being Scalar of R
for L being Linear_Combination of V holds (L * b) * a = L * (b * a)
let b, a be Scalar of R; ::_thesis: for L being Linear_Combination of V holds (L * b) * a = L * (b * a)
let L be Linear_Combination of V; ::_thesis: (L * b) * a = L * (b * a)
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: ((L * b) * a) . v = (L * (b * a)) . v
thus ((L * b) * a) . v = ((L * b) . v) * a by Def10
.= ((L . v) * b) * a by Def10
.= (L . v) * (b * a) by GROUP_1:def_3
.= (L * (b * a)) . v by Def10 ; ::_thesis: verum
end;
theorem :: RMOD_4:49
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds L * (1_ R) = L
proof
let R be Ring; ::_thesis: for V being RightMod of R
for L being Linear_Combination of V holds L * (1_ R) = L
let V be RightMod of R; ::_thesis: for L being Linear_Combination of V holds L * (1_ R) = L
let L be Linear_Combination of V; ::_thesis: L * (1_ R) = L
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L * (1_ R)) . v = L . v
thus (L * (1_ R)) . v = (L . v) * (1_ R) by Def10
.= L . v by VECTSP_1:def_4 ; ::_thesis: verum
end;
definition
let R be Ring;
let V be RightMod of R;
let L be Linear_Combination of V;
func - L -> Linear_Combination of V equals :: RMOD_4:def 11
L * (- (1_ R));
correctness
coherence
L * (- (1_ R)) is Linear_Combination of V;
;
involutiveness
for b1, b2 being Linear_Combination of V st b1 = b2 * (- (1_ R)) holds
b2 = b1 * (- (1_ R))
proof
let L, L9 be Linear_Combination of V; ::_thesis: ( L = L9 * (- (1_ R)) implies L9 = L * (- (1_ R)) )
assume A1: L = L9 * (- (1_ R)) ; ::_thesis: L9 = L * (- (1_ R))
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: L9 . v = (L * (- (1_ R))) . v
thus L9 . v = (L9 . v) * (1_ R) by VECTSP_1:def_4
.= (L9 . v) * ((1_ R) * (1_ R)) by VECTSP_1:def_4
.= (L9 . v) * ((- (1_ R)) * (- (1_ R))) by VECTSP_1:10
.= (L9 * ((- (1_ R)) * (- (1_ R)))) . v by Def10
.= (L * (- (1_ R))) . v by A1, Th48 ; ::_thesis: verum
end;
end;
:: deftheorem defines - RMOD_4:def_11_:_
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds - L = L * (- (1_ R));
theorem Th50: :: RMOD_4:50
for R being Ring
for V being RightMod of R
for v being Vector of V
for L being Linear_Combination of V holds (- L) . v = - (L . v)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v being Vector of V
for L being Linear_Combination of V holds (- L) . v = - (L . v)
let V be RightMod of R; ::_thesis: for v being Vector of V
for L being Linear_Combination of V holds (- L) . v = - (L . v)
let v be Vector of V; ::_thesis: for L being Linear_Combination of V holds (- L) . v = - (L . v)
let L be Linear_Combination of V; ::_thesis: (- L) . v = - (L . v)
thus (- L) . v = (L . v) * (- (1_ R)) by Def10
.= - (L . v) by VECTSP_2:28 ; ::_thesis: verum
end;
theorem :: RMOD_4:51
for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1
proof
let R be Ring; ::_thesis: for V being RightMod of R
for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1
let V be RightMod of R; ::_thesis: for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1
let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 + L2 = ZeroLC V implies L2 = - L1 )
assume A1: L1 + L2 = ZeroLC V ; ::_thesis: L2 = - L1
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: L2 . v = (- L1) . v
(L1 . v) + (L2 . v) = (ZeroLC V) . v by A1, Def9
.= 0. R by Th18 ;
hence L2 . v = - (L1 . v) by RLVECT_1:6
.= (- L1) . v by Th50 ;
::_thesis: verum
end;
theorem Th52: :: RMOD_4:52
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds Carrier (- L) = Carrier L
proof
let R be Ring; ::_thesis: for V being RightMod of R
for L being Linear_Combination of V holds Carrier (- L) = Carrier L
let V be RightMod of R; ::_thesis: for L being Linear_Combination of V holds Carrier (- L) = Carrier L
let L be Linear_Combination of V; ::_thesis: Carrier (- L) = Carrier L
set a = - (1_ R);
Carrier (L * (- (1_ R))) = Carrier L
proof
set S = { v where v is Vector of V : L . v <> 0. R } ;
set T = { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } ;
{ u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } = { v where v is Vector of V : L . v <> 0. R }
proof
thus { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } c= { v where v is Vector of V : L . v <> 0. R } :: according to XBOOLE_0:def_10 ::_thesis: { v where v is Vector of V : L . v <> 0. R } c= { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } or x in { v where v is Vector of V : L . v <> 0. R } )
assume x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } ; ::_thesis: x in { v where v is Vector of V : L . v <> 0. R }
then consider u being Vector of V such that
A1: x = u and
A2: (L * (- (1_ R))) . u <> 0. R ;
(L * (- (1_ R))) . u = (L . u) * (- (1_ R)) by Def10;
then L . u <> 0. R by A2, VECTSP_1:7;
hence x in { v where v is Vector of V : L . v <> 0. R } by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Vector of V : L . v <> 0. R } or x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } )
assume x in { v where v is Vector of V : L . v <> 0. R } ; ::_thesis: x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R }
then consider v being Vector of V such that
A3: x = v and
A4: L . v <> 0. R ;
(L * (- (1_ R))) . v = (L . v) * (- (1_ R)) by Def10
.= - (L . v) by VECTSP_2:28 ;
then (L * (- (1_ R))) . v <> 0. R by A4, VECTSP_2:3;
hence x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } by A3; ::_thesis: verum
end;
hence Carrier (L * (- (1_ R))) = Carrier L ; ::_thesis: verum
end;
hence Carrier (- L) = Carrier L ; ::_thesis: verum
end;
theorem :: RMOD_4:53
for R being Ring
for V being RightMod of R
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
- L is Linear_Combination of A by Th45;
definition
let R be Ring;
let V be RightMod of R;
let L1, L2 be Linear_Combination of V;
funcL1 - L2 -> Linear_Combination of V equals :: RMOD_4:def 12
L1 + (- L2);
correctness
coherence
L1 + (- L2) is Linear_Combination of V;
;
end;
:: deftheorem defines - RMOD_4:def_12_:_
for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);
theorem Th54: :: RMOD_4:54
for R being Ring
for V being RightMod of R
for v being Vector of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v being Vector of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
let V be RightMod of R; ::_thesis: for v being Vector of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
let v be Vector of V; ::_thesis: for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
let L1, L2 be Linear_Combination of V; ::_thesis: (L1 - L2) . v = (L1 . v) - (L2 . v)
thus (L1 - L2) . v = (L1 . v) + ((- L2) . v) by Def9
.= (L1 . v) + (- (L2 . v)) by Th50
.= (L1 . v) - (L2 . v) by RLVECT_1:def_11 ; ::_thesis: verum
end;
theorem :: RMOD_4:55
for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
let V be RightMod of R; ::_thesis: for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
let L1, L2 be Linear_Combination of V; ::_thesis: Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier (- L2)) by Th37;
hence Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) by Th52; ::_thesis: verum
end;
theorem :: RMOD_4:56
for R being Ring
for V being RightMod of R
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 - L2 is Linear_Combination of A
proof
let R be Ring; ::_thesis: for V being RightMod of R
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 - L2 is Linear_Combination of A
let V be RightMod of R; ::_thesis: for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 - L2 is Linear_Combination of A
let A be Subset of V; ::_thesis: for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 - L2 is Linear_Combination of A
let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 is Linear_Combination of A & L2 is Linear_Combination of A implies L1 - L2 is Linear_Combination of A )
assume that
A1: L1 is Linear_Combination of A and
A2: L2 is Linear_Combination of A ; ::_thesis: L1 - L2 is Linear_Combination of A
- L2 is Linear_Combination of A by A2, Th45;
hence L1 - L2 is Linear_Combination of A by A1, Th38; ::_thesis: verum
end;
theorem :: RMOD_4:57
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds L - L = ZeroLC V
proof
let R be Ring; ::_thesis: for V being RightMod of R
for L being Linear_Combination of V holds L - L = ZeroLC V
let V be RightMod of R; ::_thesis: for L being Linear_Combination of V holds L - L = ZeroLC V
let L be Linear_Combination of V; ::_thesis: L - L = ZeroLC V
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L - L) . v = (ZeroLC V) . v
thus (L - L) . v = (L . v) - (L . v) by Th54
.= 0. R by RLVECT_1:15
.= (ZeroLC V) . v by Th18 ; ::_thesis: verum
end;
theorem Th58: :: RMOD_4:58
for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
let V be RightMod of R; ::_thesis: for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
let L1, L2 be Linear_Combination of V; ::_thesis: Sum (L1 + L2) = (Sum L1) + (Sum L2)
set A = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2);
set C1 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1);
consider p being FinSequence such that
A1: rng p = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of V by A1, FINSEQ_1:def_4;
A3: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier L1) \/ ((Carrier (L1 + L2)) \/ (Carrier L2)) by XBOOLE_1:4;
set C3 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2));
consider r being FinSequence such that
A4: rng r = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) and
A5: r is one-to-one by FINSEQ_4:58;
reconsider r = r as FinSequence of V by A4, FINSEQ_1:def_4;
A6: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier (L1 + L2)) \/ ((Carrier L1) \/ (Carrier L2)) by XBOOLE_1:4;
set C2 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2);
consider q being FinSequence such that
A7: rng q = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) and
A8: q is one-to-one by FINSEQ_4:58;
reconsider q = q as FinSequence of V by A7, FINSEQ_1:def_4;
consider F being FinSequence of V such that
A9: F is one-to-one and
A10: rng F = Carrier (L1 + L2) and
A11: Sum ((L1 + L2) (#) F) = Sum (L1 + L2) by Def7;
set FF = F ^ r;
consider G being FinSequence of V such that
A12: G is one-to-one and
A13: rng G = Carrier L1 and
A14: Sum (L1 (#) G) = Sum L1 by Def7;
rng (F ^ r) = (rng F) \/ (rng r) by FINSEQ_1:31;
then rng (F ^ r) = (Carrier (L1 + L2)) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A10, A4, XBOOLE_1:39;
then A15: rng (F ^ r) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A6, XBOOLE_1:7, XBOOLE_1:12;
set GG = G ^ p;
rng (G ^ p) = (rng G) \/ (rng p) by FINSEQ_1:31;
then rng (G ^ p) = (Carrier L1) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A13, A1, XBOOLE_1:39;
then A16: rng (G ^ p) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A3, XBOOLE_1:7, XBOOLE_1:12;
rng F misses rng r
proof
set x = the Element of (rng F) /\ (rng r);
assume not rng F misses rng r ; ::_thesis: contradiction
then (rng F) /\ (rng r) <> {} by XBOOLE_0:def_7;
then ( the Element of (rng F) /\ (rng r) in Carrier (L1 + L2) & the Element of (rng F) /\ (rng r) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) ) by A10, A4, XBOOLE_0:def_4;
hence contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
then A17: F ^ r is one-to-one by A9, A5, FINSEQ_3:91;
rng G misses rng p
proof
set x = the Element of (rng G) /\ (rng p);
assume not rng G misses rng p ; ::_thesis: contradiction
then (rng G) /\ (rng p) <> {} by XBOOLE_0:def_7;
then ( the Element of (rng G) /\ (rng p) in Carrier L1 & the Element of (rng G) /\ (rng p) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) ) by A13, A1, XBOOLE_0:def_4;
hence contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
then A18: G ^ p is one-to-one by A12, A2, FINSEQ_3:91;
then A19: len (G ^ p) = len (F ^ r) by A17, A16, A15, FINSEQ_1:48;
deffunc H1( Nat) -> set = (F ^ r) <- ((G ^ p) . $1);
consider P being FinSequence such that
A20: len P = len (F ^ r) and
A21: for k being Nat st k in dom P holds
P . k = H1(k) from FINSEQ_1:sch_2();
A22: dom P = Seg (len (F ^ r)) by A20, FINSEQ_1:def_3;
A23: now__::_thesis:_for_x_being_set_st_x_in_dom_(G_^_p)_holds_
(G_^_p)_._x_=_(F_^_r)_._(P_._x)
let x be set ; ::_thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (F ^ r) . (P . x) )
assume A24: x in dom (G ^ p) ; ::_thesis: (G ^ p) . x = (F ^ r) . (P . x)
then reconsider n = x as Nat by FINSEQ_3:23;
(G ^ p) . n in rng (F ^ r) by A16, A15, A24, FUNCT_1:def_3;
then A25: F ^ r just_once_values (G ^ p) . n by A17, FINSEQ_4:8;
n in Seg (len (F ^ r)) by A19, A24, FINSEQ_1:def_3;
then (F ^ r) . (P . n) = (F ^ r) . ((F ^ r) <- ((G ^ p) . n)) by A21, A22
.= (G ^ p) . n by A25, FINSEQ_4:def_3 ;
hence (G ^ p) . x = (F ^ r) . (P . x) ; ::_thesis: verum
end;
A26: dom (G ^ p) = dom (F ^ r) by A19, FINSEQ_3:29;
A27: rng P c= dom (F ^ r)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P or x in dom (F ^ r) )
assume x in rng P ; ::_thesis: x in dom (F ^ r)
then consider y being set such that
A28: y in dom P and
A29: P . y = x by FUNCT_1:def_3;
reconsider y = y as Nat by A28, FINSEQ_3:23;
y in dom (F ^ r) by A20, A28, FINSEQ_3:29;
then (G ^ p) . y in rng (F ^ r) by A16, A15, A26, FUNCT_1:def_3;
then A30: F ^ r just_once_values (G ^ p) . y by A17, FINSEQ_4:8;
P . y = (F ^ r) <- ((G ^ p) . y) by A21, A28;
hence x in dom (F ^ r) by A29, A30, FINSEQ_4:def_3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_(G_^_p)_implies_(_x_in_dom_P_&_P_._x_in_dom_(F_^_r)_)_)_&_(_x_in_dom_P_&_P_._x_in_dom_(F_^_r)_implies_x_in_dom_(G_^_p)_)_)
let x be set ; ::_thesis: ( ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) & ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) ) )
thus ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) ::_thesis: ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) )
proof
assume x in dom (G ^ p) ; ::_thesis: ( x in dom P & P . x in dom (F ^ r) )
hence x in dom P by A19, A20, FINSEQ_3:29; ::_thesis: P . x in dom (F ^ r)
then P . x in rng P by FUNCT_1:def_3;
hence P . x in dom (F ^ r) by A27; ::_thesis: verum
end;
assume that
A31: x in dom P and
P . x in dom (F ^ r) ; ::_thesis: x in dom (G ^ p)
x in Seg (len P) by A31, FINSEQ_1:def_3;
hence x in dom (G ^ p) by A19, A20, FINSEQ_1:def_3; ::_thesis: verum
end;
then A32: G ^ p = (F ^ r) * P by A23, FUNCT_1:10;
dom (F ^ r) c= rng P
proof
set f = ((F ^ r) ") * (G ^ p);
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (F ^ r) or x in rng P )
assume A33: x in dom (F ^ r) ; ::_thesis: x in rng P
dom ((F ^ r) ") = rng (G ^ p) by A17, A16, A15, FUNCT_1:33;
then A34: rng (((F ^ r) ") * (G ^ p)) = rng ((F ^ r) ") by RELAT_1:28
.= dom (F ^ r) by A17, FUNCT_1:33 ;
((F ^ r) ") * (G ^ p) = (((F ^ r) ") * (F ^ r)) * P by A32, RELAT_1:36
.= (id (dom (F ^ r))) * P by A17, FUNCT_1:39
.= P by A27, RELAT_1:53 ;
hence x in rng P by A33, A34; ::_thesis: verum
end;
then A35: dom (F ^ r) = rng P by A27, XBOOLE_0:def_10;
A36: len r = len ((L1 + L2) (#) r) by Def6;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_r_holds_
((L1_+_L2)_(#)_r)_._k_=_(r_/._k)_*_(0._R)
let k be Nat; ::_thesis: ( k in dom r implies ((L1 + L2) (#) r) . k = (r /. k) * (0. R) )
assume A37: k in dom r ; ::_thesis: ((L1 + L2) (#) r) . k = (r /. k) * (0. R)
then r /. k = r . k by PARTFUN1:def_6;
then r /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) by A4, A37, FUNCT_1:def_3;
then A38: not r /. k in Carrier (L1 + L2) by XBOOLE_0:def_5;
k in dom ((L1 + L2) (#) r) by A36, A37, FINSEQ_3:29;
then ((L1 + L2) (#) r) . k = (r /. k) * ((L1 + L2) . (r /. k)) by Def6;
hence ((L1 + L2) (#) r) . k = (r /. k) * (0. R) by A38; ::_thesis: verum
end;
then A39: Sum ((L1 + L2) (#) r) = (Sum r) * (0. R) by A36, Lm2
.= 0. V by VECTSP_2:32 ;
A40: len p = len (L1 (#) p) by Def6;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_holds_
(L1_(#)_p)_._k_=_(p_/._k)_*_(0._R)
let k be Nat; ::_thesis: ( k in dom p implies (L1 (#) p) . k = (p /. k) * (0. R) )
assume A41: k in dom p ; ::_thesis: (L1 (#) p) . k = (p /. k) * (0. R)
then p /. k = p . k by PARTFUN1:def_6;
then p /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) by A1, A41, FUNCT_1:def_3;
then A42: not p /. k in Carrier L1 by XBOOLE_0:def_5;
k in dom (L1 (#) p) by A40, A41, FINSEQ_3:29;
then (L1 (#) p) . k = (p /. k) * (L1 . (p /. k)) by Def6;
hence (L1 (#) p) . k = (p /. k) * (0. R) by A42; ::_thesis: verum
end;
then A43: Sum (L1 (#) p) = (Sum p) * (0. R) by A40, Lm2
.= 0. V by VECTSP_2:32 ;
set f = (L1 + L2) (#) (F ^ r);
consider H being FinSequence of V such that
A44: H is one-to-one and
A45: rng H = Carrier L2 and
A46: Sum (L2 (#) H) = Sum L2 by Def7;
set HH = H ^ q;
rng H misses rng q
proof
set x = the Element of (rng H) /\ (rng q);
assume not rng H misses rng q ; ::_thesis: contradiction
then (rng H) /\ (rng q) <> {} by XBOOLE_0:def_7;
then ( the Element of (rng H) /\ (rng q) in Carrier L2 & the Element of (rng H) /\ (rng q) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) ) by A45, A7, XBOOLE_0:def_4;
hence contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
then A47: H ^ q is one-to-one by A44, A8, FINSEQ_3:91;
A48: len q = len (L2 (#) q) by Def6;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_q_holds_
(L2_(#)_q)_._k_=_(q_/._k)_*_(0._R)
let k be Nat; ::_thesis: ( k in dom q implies (L2 (#) q) . k = (q /. k) * (0. R) )
assume A49: k in dom q ; ::_thesis: (L2 (#) q) . k = (q /. k) * (0. R)
then q /. k = q . k by PARTFUN1:def_6;
then q /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) by A7, A49, FUNCT_1:def_3;
then A50: not q /. k in Carrier L2 by XBOOLE_0:def_5;
k in dom (L2 (#) q) by A48, A49, FINSEQ_3:29;
then (L2 (#) q) . k = (q /. k) * (L2 . (q /. k)) by Def6;
hence (L2 (#) q) . k = (q /. k) * (0. R) by A50; ::_thesis: verum
end;
then A51: Sum (L2 (#) q) = (Sum q) * (0. R) by A48, Lm2
.= 0. V by VECTSP_2:32 ;
set g = L1 (#) (G ^ p);
A52: len (L1 (#) (G ^ p)) = len (G ^ p) by Def6;
then A53: Seg (len (G ^ p)) = dom (L1 (#) (G ^ p)) by FINSEQ_1:def_3;
rng (H ^ q) = (rng H) \/ (rng q) by FINSEQ_1:31;
then rng (H ^ q) = (Carrier L2) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A45, A7, XBOOLE_1:39;
then A54: rng (H ^ q) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by XBOOLE_1:7, XBOOLE_1:12;
then A55: len (G ^ p) = len (H ^ q) by A47, A18, A16, FINSEQ_1:48;
deffunc H2( Nat) -> set = (H ^ q) <- ((G ^ p) . $1);
consider R being FinSequence such that
A56: len R = len (H ^ q) and
A57: for k being Nat st k in dom R holds
R . k = H2(k) from FINSEQ_1:sch_2();
A58: dom R = Seg (len (H ^ q)) by A56, FINSEQ_1:def_3;
A59: now__::_thesis:_for_x_being_set_st_x_in_dom_(G_^_p)_holds_
(G_^_p)_._x_=_(H_^_q)_._(R_._x)
let x be set ; ::_thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (H ^ q) . (R . x) )
assume A60: x in dom (G ^ p) ; ::_thesis: (G ^ p) . x = (H ^ q) . (R . x)
then reconsider n = x as Nat by FINSEQ_3:23;
(G ^ p) . n in rng (H ^ q) by A16, A54, A60, FUNCT_1:def_3;
then A61: H ^ q just_once_values (G ^ p) . n by A47, FINSEQ_4:8;
n in Seg (len (H ^ q)) by A55, A60, FINSEQ_1:def_3;
then (H ^ q) . (R . n) = (H ^ q) . ((H ^ q) <- ((G ^ p) . n)) by A57, A58
.= (G ^ p) . n by A61, FINSEQ_4:def_3 ;
hence (G ^ p) . x = (H ^ q) . (R . x) ; ::_thesis: verum
end;
A62: dom (G ^ p) = dom (H ^ q) by A55, FINSEQ_3:29;
A63: rng R c= dom (H ^ q)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng R or x in dom (H ^ q) )
assume x in rng R ; ::_thesis: x in dom (H ^ q)
then consider y being set such that
A64: y in dom R and
A65: R . y = x by FUNCT_1:def_3;
reconsider y = y as Nat by A64, FINSEQ_3:23;
y in dom (H ^ q) by A56, A64, FINSEQ_3:29;
then (G ^ p) . y in rng (H ^ q) by A16, A54, A62, FUNCT_1:def_3;
then A66: H ^ q just_once_values (G ^ p) . y by A47, FINSEQ_4:8;
R . y = (H ^ q) <- ((G ^ p) . y) by A57, A64;
hence x in dom (H ^ q) by A65, A66, FINSEQ_4:def_3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_(G_^_p)_implies_(_x_in_dom_R_&_R_._x_in_dom_(H_^_q)_)_)_&_(_x_in_dom_R_&_R_._x_in_dom_(H_^_q)_implies_x_in_dom_(G_^_p)_)_)
let x be set ; ::_thesis: ( ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) & ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) ) )
thus ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) ::_thesis: ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) )
proof
assume x in dom (G ^ p) ; ::_thesis: ( x in dom R & R . x in dom (H ^ q) )
then x in Seg (len R) by A55, A56, FINSEQ_1:def_3;
hence x in dom R by FINSEQ_1:def_3; ::_thesis: R . x in dom (H ^ q)
then R . x in rng R by FUNCT_1:def_3;
hence R . x in dom (H ^ q) by A63; ::_thesis: verum
end;
assume that
A67: x in dom R and
R . x in dom (H ^ q) ; ::_thesis: x in dom (G ^ p)
x in Seg (len R) by A67, FINSEQ_1:def_3;
hence x in dom (G ^ p) by A55, A56, FINSEQ_1:def_3; ::_thesis: verum
end;
then A68: G ^ p = (H ^ q) * R by A59, FUNCT_1:10;
dom (H ^ q) c= rng R
proof
set f = ((H ^ q) ") * (G ^ p);
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (H ^ q) or x in rng R )
assume A69: x in dom (H ^ q) ; ::_thesis: x in rng R
dom ((H ^ q) ") = rng (G ^ p) by A47, A16, A54, FUNCT_1:33;
then A70: rng (((H ^ q) ") * (G ^ p)) = rng ((H ^ q) ") by RELAT_1:28
.= dom (H ^ q) by A47, FUNCT_1:33 ;
((H ^ q) ") * (G ^ p) = (((H ^ q) ") * (H ^ q)) * R by A68, RELAT_1:36
.= (id (dom (H ^ q))) * R by A47, FUNCT_1:39
.= R by A63, RELAT_1:53 ;
hence x in rng R by A69, A70; ::_thesis: verum
end;
then A71: dom (H ^ q) = rng R by A63, XBOOLE_0:def_10;
A72: Sum (L1 (#) (G ^ p)) = Sum ((L1 (#) G) ^ (L1 (#) p)) by Th28
.= (Sum (L1 (#) G)) + (0. V) by A43, RLVECT_1:41
.= Sum (L1 (#) G) by RLVECT_1:def_4 ;
set h = L2 (#) (H ^ q);
A73: Sum (L2 (#) (H ^ q)) = Sum ((L2 (#) H) ^ (L2 (#) q)) by Th28
.= (Sum (L2 (#) H)) + (0. V) by A51, RLVECT_1:41
.= Sum (L2 (#) H) by RLVECT_1:def_4 ;
A74: Sum ((L1 + L2) (#) (F ^ r)) = Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Th28
.= (Sum ((L1 + L2) (#) F)) + (0. V) by A39, RLVECT_1:41
.= Sum ((L1 + L2) (#) F) by RLVECT_1:def_4 ;
A75: dom P = dom (F ^ r) by A20, FINSEQ_3:29;
then A76: P is one-to-one by A35, FINSEQ_4:60;
A77: dom R = dom (H ^ q) by A56, FINSEQ_3:29;
then A78: R is one-to-one by A71, FINSEQ_4:60;
reconsider R = R as Function of (dom (H ^ q)),(dom (H ^ q)) by A63, A77, FUNCT_2:2;
A79: len (L2 (#) (H ^ q)) = len (H ^ q) by Def6;
then A80: dom (L2 (#) (H ^ q)) = dom (H ^ q) by FINSEQ_3:29;
then reconsider R = R as Function of (dom (L2 (#) (H ^ q))),(dom (L2 (#) (H ^ q))) ;
reconsider Hp = (L2 (#) (H ^ q)) * R as FinSequence of V by FINSEQ_2:47;
reconsider R = R as Permutation of (dom (L2 (#) (H ^ q))) by A71, A78, A80, FUNCT_2:57;
A81: Hp = (L2 (#) (H ^ q)) * R ;
then A82: len Hp = len (G ^ p) by A55, A79, FINSEQ_2:44;
reconsider P = P as Function of (dom (F ^ r)),(dom (F ^ r)) by A27, A75, FUNCT_2:2;
A83: len ((L1 + L2) (#) (F ^ r)) = len (F ^ r) by Def6;
then A84: dom ((L1 + L2) (#) (F ^ r)) = dom (F ^ r) by FINSEQ_3:29;
then reconsider P = P as Function of (dom ((L1 + L2) (#) (F ^ r))),(dom ((L1 + L2) (#) (F ^ r))) ;
reconsider Fp = ((L1 + L2) (#) (F ^ r)) * P as FinSequence of V by FINSEQ_2:47;
reconsider P = P as Permutation of (dom ((L1 + L2) (#) (F ^ r))) by A35, A76, A84, FUNCT_2:57;
A85: Fp = ((L1 + L2) (#) (F ^ r)) * P ;
then A86: Sum Fp = Sum ((L1 + L2) (#) (F ^ r)) by RLVECT_2:7;
deffunc H3( Nat) -> Element of the carrier of V = ((L1 (#) (G ^ p)) /. $1) + (Hp /. $1);
consider I being FinSequence such that
A87: len I = len (G ^ p) and
A88: for k being Nat st k in dom I holds
I . k = H3(k) from FINSEQ_1:sch_2();
A89: dom I = Seg (len (G ^ p)) by A87, FINSEQ_1:def_3;
then A90: for k being Element of NAT st k in Seg (len (G ^ p)) holds
I . k = H3(k) by A88;
rng I c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng I or x in the carrier of V )
assume x in rng I ; ::_thesis: x in the carrier of V
then consider y being set such that
A91: y in dom I and
A92: I . y = x by FUNCT_1:def_3;
reconsider y = y as Nat by A91, FINSEQ_3:23;
I . y = ((L1 (#) (G ^ p)) /. y) + (Hp /. y) by A88, A91;
hence x in the carrier of V by A92; ::_thesis: verum
end;
then reconsider I = I as FinSequence of V by FINSEQ_1:def_4;
A93: len Fp = len I by A19, A83, A85, A87, FINSEQ_2:44;
A94: now__::_thesis:_for_x_being_set_st_x_in_Seg_(len_I)_holds_
I_._x_=_Fp_._x
let x be set ; ::_thesis: ( x in Seg (len I) implies I . x = Fp . x )
assume A95: x in Seg (len I) ; ::_thesis: I . x = Fp . x
then reconsider k = x as Element of NAT ;
A96: x in dom (H ^ q) by A55, A87, A95, FINSEQ_1:def_3;
then R . k in dom R by A71, A77, FUNCT_1:def_3;
then reconsider j = R . k as Nat by FINSEQ_3:23;
A97: x in dom (G ^ p) by A87, A95, FINSEQ_1:def_3;
then A98: (H ^ q) . j = (G ^ p) . k by A59
.= (G ^ p) /. k by A97, PARTFUN1:def_6 ;
P . k in dom P by A26, A62, A35, A75, A96, FUNCT_1:def_3;
then reconsider l = P . k as Nat by FINSEQ_3:23;
set v = (G ^ p) /. k;
A99: x in dom Fp by A93, A95, FINSEQ_1:def_3;
A100: (F ^ r) . l = (G ^ p) . k by A23, A97
.= (G ^ p) /. k by A97, PARTFUN1:def_6 ;
P . k in dom (F ^ r) by A26, A62, A35, A75, A96, FUNCT_1:def_3;
then A101: ((L1 + L2) (#) (F ^ r)) . l = ((G ^ p) /. k) * ((L1 + L2) . ((G ^ p) /. k)) by A100, Th23
.= ((G ^ p) /. k) * ((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k))) by Def9
.= (((G ^ p) /. k) * (L1 . ((G ^ p) /. k))) + (((G ^ p) /. k) * (L2 . ((G ^ p) /. k))) by VECTSP_2:def_9 ;
A102: x in dom Hp by A87, A82, A95, FINSEQ_1:def_3;
then A103: Hp /. k = ((L2 (#) (H ^ q)) * R) . k by PARTFUN1:def_6
.= (L2 (#) (H ^ q)) . (R . k) by A102, FUNCT_1:12 ;
R . k in dom (H ^ q) by A71, A77, A96, FUNCT_1:def_3;
then A104: (L2 (#) (H ^ q)) . j = ((G ^ p) /. k) * (L2 . ((G ^ p) /. k)) by A98, Th23;
A105: x in dom (L1 (#) (G ^ p)) by A87, A52, A95, FINSEQ_1:def_3;
then (L1 (#) (G ^ p)) /. k = (L1 (#) (G ^ p)) . k by PARTFUN1:def_6
.= ((G ^ p) /. k) * (L1 . ((G ^ p) /. k)) by A105, Def6 ;
hence I . x = (((G ^ p) /. k) * (L1 . ((G ^ p) /. k))) + (((G ^ p) /. k) * (L2 . ((G ^ p) /. k))) by A87, A88, A89, A95, A103, A104
.= Fp . x by A99, A101, FUNCT_1:12 ;
::_thesis: verum
end;
( dom I = Seg (len I) & dom Fp = Seg (len I) ) by A93, FINSEQ_1:def_3;
then A106: I = Fp by A94, FUNCT_1:2;
Sum Hp = Sum (L2 (#) (H ^ q)) by A81, RLVECT_2:7;
hence Sum (L1 + L2) = (Sum L1) + (Sum L2) by A11, A14, A46, A72, A73, A74, A86, A87, A90, A82, A52, A106, A53, RLVECT_2:2; ::_thesis: verum
end;
theorem Th59: :: RMOD_4:59
for R being domRing
for V being RightMod of R
for L being Linear_Combination of V
for a being Scalar of R holds Sum (L * a) = (Sum L) * a
proof
let R be domRing; ::_thesis: for V being RightMod of R
for L being Linear_Combination of V
for a being Scalar of R holds Sum (L * a) = (Sum L) * a
let V be RightMod of R; ::_thesis: for L being Linear_Combination of V
for a being Scalar of R holds Sum (L * a) = (Sum L) * a
let L be Linear_Combination of V; ::_thesis: for a being Scalar of R holds Sum (L * a) = (Sum L) * a
let a be Scalar of R; ::_thesis: Sum (L * a) = (Sum L) * a
percases ( a <> 0. R or a = 0. R ) ;
supposeA1: a <> 0. R ; ::_thesis: Sum (L * a) = (Sum L) * a
set l = L * a;
A2: Carrier (L * a) = Carrier L by A1, Th43;
consider G being FinSequence of V such that
A3: G is one-to-one and
A4: rng G = Carrier L and
A5: Sum L = Sum (L (#) G) by Def7;
set g = L (#) G;
consider F being FinSequence of V such that
A6: F is one-to-one and
A7: rng F = Carrier (L * a) and
A8: Sum (L * a) = Sum ((L * a) (#) F) by Def7;
A9: len G = len F by A1, A6, A7, A3, A4, Th43, FINSEQ_1:48;
set f = (L * a) (#) F;
deffunc H1( Nat) -> set = F <- (G . $1);
consider P being FinSequence such that
A10: len P = len F and
A11: for k being Nat st k in dom P holds
P . k = H1(k) from FINSEQ_1:sch_2();
A12: dom P = Seg (len F) by A10, FINSEQ_1:def_3;
A13: now__::_thesis:_for_x_being_set_st_x_in_dom_G_holds_
G_._x_=_F_._(P_._x)
let x be set ; ::_thesis: ( x in dom G implies G . x = F . (P . x) )
assume A14: x in dom G ; ::_thesis: G . x = F . (P . x)
then reconsider n = x as Nat by FINSEQ_3:23;
G . n in rng F by A7, A4, A2, A14, FUNCT_1:def_3;
then A15: F just_once_values G . n by A6, FINSEQ_4:8;
n in Seg (len F) by A9, A14, FINSEQ_1:def_3;
then F . (P . n) = F . (F <- (G . n)) by A11, A12
.= G . n by A15, FINSEQ_4:def_3 ;
hence G . x = F . (P . x) ; ::_thesis: verum
end;
A16: rng P c= dom F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P or x in dom F )
assume x in rng P ; ::_thesis: x in dom F
then consider y being set such that
A17: y in dom P and
A18: P . y = x by FUNCT_1:def_3;
reconsider y = y as Nat by A17, FINSEQ_3:23;
y in dom G by A10, A9, A17, FINSEQ_3:29;
then G . y in rng F by A7, A4, A2, FUNCT_1:def_3;
then A19: F just_once_values G . y by A6, FINSEQ_4:8;
P . y = F <- (G . y) by A11, A17;
hence x in dom F by A18, A19, FINSEQ_4:def_3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_G_implies_(_x_in_dom_P_&_P_._x_in_dom_F_)_)_&_(_x_in_dom_P_&_P_._x_in_dom_F_implies_x_in_dom_G_)_)
let x be set ; ::_thesis: ( ( x in dom G implies ( x in dom P & P . x in dom F ) ) & ( x in dom P & P . x in dom F implies x in dom G ) )
thus ( x in dom G implies ( x in dom P & P . x in dom F ) ) ::_thesis: ( x in dom P & P . x in dom F implies x in dom G )
proof
assume x in dom G ; ::_thesis: ( x in dom P & P . x in dom F )
then x in Seg (len P) by A10, A9, FINSEQ_1:def_3;
hence x in dom P by FINSEQ_1:def_3; ::_thesis: P . x in dom F
then P . x in rng P by FUNCT_1:def_3;
hence P . x in dom F by A16; ::_thesis: verum
end;
assume that
A20: x in dom P and
P . x in dom F ; ::_thesis: x in dom G
x in Seg (len P) by A20, FINSEQ_1:def_3;
hence x in dom G by A10, A9, FINSEQ_1:def_3; ::_thesis: verum
end;
then A21: G = F * P by A13, FUNCT_1:10;
dom F c= rng P
proof
set f = (F ") * G;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom F or x in rng P )
assume A22: x in dom F ; ::_thesis: x in rng P
dom (F ") = rng G by A6, A7, A4, A2, FUNCT_1:33;
then A23: rng ((F ") * G) = rng (F ") by RELAT_1:28
.= dom F by A6, FUNCT_1:33 ;
(F ") * G = ((F ") * F) * P by A21, RELAT_1:36
.= (id (dom F)) * P by A6, FUNCT_1:39
.= P by A16, RELAT_1:53 ;
hence x in rng P by A22, A23; ::_thesis: verum
end;
then A24: dom F = rng P by A16, XBOOLE_0:def_10;
A25: dom P = dom F by A10, FINSEQ_3:29;
then A26: P is one-to-one by A24, FINSEQ_4:60;
reconsider P = P as Function of (dom F),(dom F) by A16, A25, FUNCT_2:2;
A27: len ((L * a) (#) F) = len F by Def6;
then A28: dom ((L * a) (#) F) = dom F by FINSEQ_3:29;
then reconsider P = P as Function of (dom ((L * a) (#) F)),(dom ((L * a) (#) F)) ;
reconsider Fp = ((L * a) (#) F) * P as FinSequence of V by FINSEQ_2:47;
reconsider P = P as Permutation of (dom ((L * a) (#) F)) by A24, A26, A28, FUNCT_2:57;
A29: Fp = ((L * a) (#) F) * P ;
then A30: len Fp = len ((L * a) (#) F) by FINSEQ_2:44;
then A31: len Fp = len (L (#) G) by A9, A27, Def6;
A32: now__::_thesis:_for_k_being_Nat
for_v_being_Vector_of_V_st_k_in_dom_Fp_&_v_=_(L_(#)_G)_._k_holds_
Fp_._k_=_v_*_a
let k be Nat; ::_thesis: for v being Vector of V st k in dom Fp & v = (L (#) G) . k holds
Fp . k = v * a
let v be Vector of V; ::_thesis: ( k in dom Fp & v = (L (#) G) . k implies Fp . k = v * a )
assume that
A33: k in dom Fp and
A34: v = (L (#) G) . k ; ::_thesis: Fp . k = v * a
A35: k in Seg (len (L (#) G)) by A31, A33, FINSEQ_1:def_3;
then A36: k in dom P by A10, A27, A30, A31, FINSEQ_1:def_3;
A37: k in dom G by A9, A27, A30, A31, A35, FINSEQ_1:def_3;
then G . k in rng G by FUNCT_1:def_3;
then F just_once_values G . k by A6, A7, A4, A2, FINSEQ_4:8;
then A38: F <- (G . k) in dom F by FINSEQ_4:def_3;
then reconsider i = F <- (G . k) as Nat by FINSEQ_3:23;
A39: G /. k = G . k by A37, PARTFUN1:def_6
.= F . (P . k) by A21, A36, FUNCT_1:13
.= F . i by A11, A12, A27, A30, A31, A35
.= F /. i by A38, PARTFUN1:def_6 ;
A40: k in dom (L (#) G) by A35, FINSEQ_1:def_3;
i in Seg (len ((L * a) (#) F)) by A27, A38, FINSEQ_1:def_3;
then A41: i in dom ((L * a) (#) F) by FINSEQ_1:def_3;
thus Fp . k = ((L * a) (#) F) . (P . k) by A36, FUNCT_1:13
.= ((L * a) (#) F) . (F <- (G . k)) by A11, A12, A27, A30, A31, A35
.= (F /. i) * ((L * a) . (F /. i)) by A41, Def6
.= (F /. i) * ((L . (F /. i)) * a) by Def10
.= ((F /. i) * (L . (F /. i))) * a by VECTSP_2:def_9
.= v * a by A34, A40, A39, Def6 ; ::_thesis: verum
end;
Sum Fp = Sum ((L * a) (#) F) by A29, RLVECT_2:7;
hence Sum (L * a) = (Sum L) * a by A8, A5, A31, A32, Th1; ::_thesis: verum
end;
supposeA42: a = 0. R ; ::_thesis: Sum (L * a) = (Sum L) * a
hence Sum (L * a) = Sum (ZeroLC V) by Th44
.= 0. V by Lm3
.= (Sum L) * a by A42, VECTSP_2:32 ;
::_thesis: verum
end;
end;
end;
theorem Th60: :: RMOD_4:60
for R being domRing
for V being RightMod of R
for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
proof
let R be domRing; ::_thesis: for V being RightMod of R
for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
let V be RightMod of R; ::_thesis: for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
let L be Linear_Combination of V; ::_thesis: Sum (- L) = - (Sum L)
thus Sum (- L) = (Sum L) * (- (1_ R)) by Th59
.= - (Sum L) by VECTSP_2:32 ; ::_thesis: verum
end;
theorem :: RMOD_4:61
for R being domRing
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)
proof
let R be domRing; ::_thesis: for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)
let V be RightMod of R; ::_thesis: for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)
let L1, L2 be Linear_Combination of V; ::_thesis: Sum (L1 - L2) = (Sum L1) - (Sum L2)
thus Sum (L1 - L2) = (Sum L1) + (Sum (- L2)) by Th58
.= (Sum L1) + (- (Sum L2)) by Th60
.= (Sum L1) - (Sum L2) by RLVECT_1:def_11 ; ::_thesis: verum
end;
begin
definition
let R be Ring;
let V be RightMod of R;
let IT be Subset of V;
attrIT is linearly-independent means :Def13: :: RMOD_4:def 13
for l being Linear_Combination of IT st Sum l = 0. V holds
Carrier l = {} ;
end;
:: deftheorem Def13 defines linearly-independent RMOD_4:def_13_:_
for R being Ring
for V being RightMod of R
for IT being Subset of V holds
( IT is linearly-independent iff for l being Linear_Combination of IT st Sum l = 0. V holds
Carrier l = {} );
notation
let R be Ring;
let V be RightMod of R;
let IT be Subset of V;
antonym linearly-dependent IT for linearly-independent ;
end;
theorem :: RMOD_4:62
for R being Ring
for V being RightMod of R
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
proof
let R be Ring; ::_thesis: for V being RightMod of R
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
let V be RightMod of R; ::_thesis: for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
let A, B be Subset of V; ::_thesis: ( A c= B & B is linearly-independent implies A is linearly-independent )
assume that
A1: A c= B and
A2: B is linearly-independent ; ::_thesis: A is linearly-independent
let l be Linear_Combination of A; :: according to RMOD_4:def_13 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
reconsider L = l as Linear_Combination of B by A1, Th19;
assume Sum l = 0. V ; ::_thesis: Carrier l = {}
then Carrier L = {} by A2, Def13;
hence Carrier l = {} ; ::_thesis: verum
end;
theorem Th63: :: RMOD_4:63
for R being Ring
for V being RightMod of R
for A being Subset of V st 0. R <> 1_ R & A is linearly-independent holds
not 0. V in A
proof
let R be Ring; ::_thesis: for V being RightMod of R
for A being Subset of V st 0. R <> 1_ R & A is linearly-independent holds
not 0. V in A
let V be RightMod of R; ::_thesis: for A being Subset of V st 0. R <> 1_ R & A is linearly-independent holds
not 0. V in A
let A be Subset of V; ::_thesis: ( 0. R <> 1_ R & A is linearly-independent implies not 0. V in A )
assume that
A1: 0. R <> 1_ R and
A2: A is linearly-independent and
A3: 0. V in A ; ::_thesis: contradiction
deffunc H1( Element of V) -> Element of the carrier of R = 0. R;
consider f being Function of the carrier of V, the carrier of R such that
A4: f . (0. V) = 1_ R and
A5: for v being Element of V st v <> 0. V holds
f . v = H1(v) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
ex T being finite Subset of V st
for v being Vector of V st not v in T holds
f . v = 0. R
proof
take T = {(0. V)}; ::_thesis: for v being Vector of V st not v in T holds
f . v = 0. R
let v be Vector of V; ::_thesis: ( not v in T implies f . v = 0. R )
assume not v in T ; ::_thesis: f . v = 0. R
then v <> 0. V by TARSKI:def_1;
hence f . v = 0. R by A5; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def2;
A6: Carrier f = {(0. V)}
proof
thus Carrier f c= {(0. V)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. V)} c= Carrier f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {(0. V)} )
assume x in Carrier f ; ::_thesis: x in {(0. V)}
then consider v being Vector of V such that
A7: v = x and
A8: f . v <> 0. R ;
v = 0. V by A5, A8;
hence x in {(0. V)} by A7, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. V)} or x in Carrier f )
assume x in {(0. V)} ; ::_thesis: x in Carrier f
then x = 0. V by TARSKI:def_1;
hence x in Carrier f by A1, A4; ::_thesis: verum
end;
then Carrier f c= A by A3, ZFMISC_1:31;
then reconsider f = f as Linear_Combination of A by Def5;
Sum f = (0. V) * (f . (0. V)) by A6, Th35
.= 0. V by VECTSP_2:32 ;
hence contradiction by A2, A6, Def13; ::_thesis: verum
end;
theorem :: RMOD_4:64
for R being Ring
for V being RightMod of R holds {} the carrier of V is linearly-independent
proof
let R be Ring; ::_thesis: for V being RightMod of R holds {} the carrier of V is linearly-independent
let V be RightMod of R; ::_thesis: {} the carrier of V is linearly-independent
let l be Linear_Combination of {} the carrier of V; :: according to RMOD_4:def_13 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
Carrier l c= {} by Def5;
hence ( Sum l = 0. V implies Carrier l = {} ) ; ::_thesis: verum
end;
theorem Th65: :: RMOD_4:65
for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V st 0. R <> 1_ R & {v1,v2} is linearly-independent holds
( v1 <> 0. V & v2 <> 0. V )
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v1, v2 being Vector of V st 0. R <> 1_ R & {v1,v2} is linearly-independent holds
( v1 <> 0. V & v2 <> 0. V )
let V be RightMod of R; ::_thesis: for v1, v2 being Vector of V st 0. R <> 1_ R & {v1,v2} is linearly-independent holds
( v1 <> 0. V & v2 <> 0. V )
let v1, v2 be Vector of V; ::_thesis: ( 0. R <> 1_ R & {v1,v2} is linearly-independent implies ( v1 <> 0. V & v2 <> 0. V ) )
A1: ( v1 in {v1,v2} & v2 in {v1,v2} ) by TARSKI:def_2;
assume ( 0. R <> 1_ R & {v1,v2} is linearly-independent ) ; ::_thesis: ( v1 <> 0. V & v2 <> 0. V )
hence ( v1 <> 0. V & v2 <> 0. V ) by A1, Th63; ::_thesis: verum
end;
theorem :: RMOD_4:66
for R being Ring
for V being RightMod of R
for v being Vector of V st 0. R <> 1_ R holds
( {v,(0. V)} is linearly-dependent & {(0. V),v} is linearly-dependent ) by Th65;
definition
let R be domRing;
let V be RightMod of R;
let A be Subset of V;
func Lin A -> strict Submodule of V means :Def14: :: RMOD_4:def 14
the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ;
existence
ex b1 being strict Submodule of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum }
proof
set A1 = { (Sum l) where l is Linear_Combination of A : verum } ;
reconsider l = ZeroLC V as Linear_Combination of A by Th20;
{ (Sum l) where l is Linear_Combination of A : verum } c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Sum l) where l is Linear_Combination of A : verum } or x in the carrier of V )
assume x in { (Sum l) where l is Linear_Combination of A : verum } ; ::_thesis: x in the carrier of V
then ex l being Linear_Combination of A st x = Sum l ;
hence x in the carrier of V ; ::_thesis: verum
end;
then reconsider A1 = { (Sum l) where l is Linear_Combination of A : verum } as Subset of V ;
A1: A1 is linearly-closed
proof
thus for v, u being Vector of V st v in A1 & u in A1 holds
v + u in A1 :: according to RMOD_2:def_1 ::_thesis: for b1 being Element of the carrier of R
for b2 being Element of the carrier of V holds
( not b2 in A1 or b2 * b1 in A1 )
proof
let v, u be Vector of V; ::_thesis: ( v in A1 & u in A1 implies v + u in A1 )
assume that
A2: v in A1 and
A3: u in A1 ; ::_thesis: v + u in A1
consider l1 being Linear_Combination of A such that
A4: v = Sum l1 by A2;
consider l2 being Linear_Combination of A such that
A5: u = Sum l2 by A3;
reconsider f = l1 + l2 as Linear_Combination of A by Th38;
v + u = Sum f by A4, A5, Th58;
hence v + u in A1 ; ::_thesis: verum
end;
let a be Scalar of R; ::_thesis: for b1 being Element of the carrier of V holds
( not b1 in A1 or b1 * a in A1 )
let v be Vector of V; ::_thesis: ( not v in A1 or v * a in A1 )
assume v in A1 ; ::_thesis: v * a in A1
then consider l being Linear_Combination of A such that
A6: v = Sum l ;
reconsider f = l * a as Linear_Combination of A by Th45;
v * a = Sum f by A6, Th59;
hence v * a in A1 ; ::_thesis: verum
end;
Sum l = 0. V by Lm3;
then 0. V in A1 ;
hence ex b1 being strict Submodule of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } by A1, RMOD_2:34; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Submodule of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } & the carrier of b2 = { (Sum l) where l is Linear_Combination of A : verum } holds
b1 = b2 by RMOD_2:29;
end;
:: deftheorem Def14 defines Lin RMOD_4:def_14_:_
for R being domRing
for V being RightMod of R
for A being Subset of V
for b4 being strict Submodule of V holds
( b4 = Lin A iff the carrier of b4 = { (Sum l) where l is Linear_Combination of A : verum } );
theorem Th67: :: RMOD_4:67
for x being set
for R being domRing
for V being RightMod of R
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
proof
let x be set ; ::_thesis: for R being domRing
for V being RightMod of R
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let R be domRing; ::_thesis: for V being RightMod of R
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let V be RightMod of R; ::_thesis: for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let A be Subset of V; ::_thesis: ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
thus ( x in Lin A implies ex l being Linear_Combination of A st x = Sum l ) ::_thesis: ( ex l being Linear_Combination of A st x = Sum l implies x in Lin A )
proof
assume x in Lin A ; ::_thesis: ex l being Linear_Combination of A st x = Sum l
then x in the carrier of (Lin A) by STRUCT_0:def_5;
then x in { (Sum l) where l is Linear_Combination of A : verum } by Def14;
hence ex l being Linear_Combination of A st x = Sum l ; ::_thesis: verum
end;
given k being Linear_Combination of A such that A1: x = Sum k ; ::_thesis: x in Lin A
x in { (Sum l) where l is Linear_Combination of A : verum } by A1;
then x in the carrier of (Lin A) by Def14;
hence x in Lin A by STRUCT_0:def_5; ::_thesis: verum
end;
theorem Th68: :: RMOD_4:68
for x being set
for R being domRing
for V being RightMod of R
for A being Subset of V st x in A holds
x in Lin A
proof
let x be set ; ::_thesis: for R being domRing
for V being RightMod of R
for A being Subset of V st x in A holds
x in Lin A
let R be domRing; ::_thesis: for V being RightMod of R
for A being Subset of V st x in A holds
x in Lin A
let V be RightMod of R; ::_thesis: for A being Subset of V st x in A holds
x in Lin A
let A be Subset of V; ::_thesis: ( x in A implies x in Lin A )
deffunc H1( Element of V) -> Element of the carrier of R = 0. R;
assume A1: x in A ; ::_thesis: x in Lin A
then reconsider v = x as Vector of V ;
consider f being Function of the carrier of V, the carrier of R such that
A2: f . v = 1_ R and
A3: for u being Vector of V st u <> v holds
f . u = H1(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
ex T being finite Subset of V st
for u being Vector of V st not u in T holds
f . u = 0. R
proof
take T = {v}; ::_thesis: for u being Vector of V st not u in T holds
f . u = 0. R
let u be Vector of V; ::_thesis: ( not u in T implies f . u = 0. R )
assume not u in T ; ::_thesis: f . u = 0. R
then u <> v by TARSKI:def_1;
hence f . u = 0. R by A3; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def2;
A4: Carrier f c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume x in Carrier f ; ::_thesis: x in {v}
then consider u being Vector of V such that
A5: x = u and
A6: f . u <> 0. R ;
u = v by A3, A6;
hence x in {v} by A5, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v} by Def5;
A7: Sum f = v * (1_ R) by A2, Th32
.= v by VECTSP_2:def_9 ;
{v} c= A by A1, ZFMISC_1:31;
then Carrier f c= A by A4, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by Def5;
Sum f = v by A7;
hence x in Lin A by Th67; ::_thesis: verum
end;
theorem :: RMOD_4:69
for R being domRing
for V being RightMod of R holds Lin ({} the carrier of V) = (0). V
proof
let R be domRing; ::_thesis: for V being RightMod of R holds Lin ({} the carrier of V) = (0). V
let V be RightMod of R; ::_thesis: Lin ({} the carrier of V) = (0). V
set A = Lin ({} the carrier of V);
now__::_thesis:_for_v_being_Vector_of_V_holds_
(_(_v_in_Lin_({}_the_carrier_of_V)_implies_v_in_(0)._V_)_&_(_v_in_(0)._V_implies_v_in_Lin_({}_the_carrier_of_V)_)_)
let v be Vector of V; ::_thesis: ( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) )
thus ( v in Lin ({} the carrier of V) implies v in (0). V ) ::_thesis: ( v in (0). V implies v in Lin ({} the carrier of V) )
proof
assume v in Lin ({} the carrier of V) ; ::_thesis: v in (0). V
then A1: v in the carrier of (Lin ({} the carrier of V)) by STRUCT_0:def_5;
the carrier of (Lin ({} the carrier of V)) = { (Sum l0) where l0 is Linear_Combination of {} the carrier of V : verum } by Def14;
then ex l0 being Linear_Combination of {} the carrier of V st v = Sum l0 by A1;
then v = 0. V by Th31;
hence v in (0). V by RMOD_2:35; ::_thesis: verum
end;
assume v in (0). V ; ::_thesis: v in Lin ({} the carrier of V)
then v = 0. V by RMOD_2:35;
hence v in Lin ({} the carrier of V) by RMOD_2:17; ::_thesis: verum
end;
hence Lin ({} the carrier of V) = (0). V by RMOD_2:30; ::_thesis: verum
end;
theorem :: RMOD_4:70
for R being domRing
for V being RightMod of R
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
proof
let R be domRing; ::_thesis: for V being RightMod of R
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
let V be RightMod of R; ::_thesis: for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
let A be Subset of V; ::_thesis: ( not Lin A = (0). V or A = {} or A = {(0. V)} )
assume that
A1: Lin A = (0). V and
A2: A <> {} ; ::_thesis: A = {(0. V)}
thus A c= {(0. V)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. V)} c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in {(0. V)} )
assume x in A ; ::_thesis: x in {(0. V)}
then x in Lin A by Th68;
then x = 0. V by A1, RMOD_2:35;
hence x in {(0. V)} by TARSKI:def_1; ::_thesis: verum
end;
set y = the Element of A;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. V)} or x in A )
assume x in {(0. V)} ; ::_thesis: x in A
then A3: x = 0. V by TARSKI:def_1;
( the Element of A in A & the Element of A in Lin A ) by A2, Th68;
hence x in A by A1, A3, RMOD_2:35; ::_thesis: verum
end;
theorem Th71: :: RMOD_4:71
for R being domRing
for V being RightMod of R
for A being Subset of V
for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds
Lin A = W
proof
let R be domRing; ::_thesis: for V being RightMod of R
for A being Subset of V
for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds
Lin A = W
let V be RightMod of R; ::_thesis: for A being Subset of V
for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds
Lin A = W
let A be Subset of V; ::_thesis: for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds
Lin A = W
let W be strict Submodule of V; ::_thesis: ( 0. R <> 1_ R & A = the carrier of W implies Lin A = W )
assume that
A1: 0. R <> 1_ R and
A2: A = the carrier of W ; ::_thesis: Lin A = W
now__::_thesis:_for_v_being_Vector_of_V_holds_
(_(_v_in_Lin_A_implies_v_in_W_)_&_(_v_in_W_implies_v_in_Lin_A_)_)
let v be Vector of V; ::_thesis: ( ( v in Lin A implies v in W ) & ( v in W implies v in Lin A ) )
thus ( v in Lin A implies v in W ) ::_thesis: ( v in W implies v in Lin A )
proof
assume v in Lin A ; ::_thesis: v in W
then A3: ex l being Linear_Combination of A st v = Sum l by Th67;
A is linearly-closed by A2, RMOD_2:33;
then v in the carrier of W by A1, A2, A3, Th29;
hence v in W by STRUCT_0:def_5; ::_thesis: verum
end;
( v in W iff v in the carrier of W ) by STRUCT_0:def_5;
hence ( v in W implies v in Lin A ) by A2, Th68; ::_thesis: verum
end;
hence Lin A = W by RMOD_2:30; ::_thesis: verum
end;
theorem :: RMOD_4:72
for R being domRing
for V being strict RightMod of R
for A being Subset of V st 0. R <> 1_ R & A = the carrier of V holds
Lin A = V
proof
let R be domRing; ::_thesis: for V being strict RightMod of R
for A being Subset of V st 0. R <> 1_ R & A = the carrier of V holds
Lin A = V
let V be strict RightMod of R; ::_thesis: for A being Subset of V st 0. R <> 1_ R & A = the carrier of V holds
Lin A = V
let A be Subset of V; ::_thesis: ( 0. R <> 1_ R & A = the carrier of V implies Lin A = V )
assume A1: 0. R <> 1_ R ; ::_thesis: ( not A = the carrier of V or Lin A = V )
assume A2: A = the carrier of V ; ::_thesis: Lin A = V
(Omega). V = V ;
hence Lin A = V by A1, A2, Th71; ::_thesis: verum
end;
theorem Th73: :: RMOD_4:73
for R being domRing
for V being RightMod of R
for A, B being Subset of V st A c= B holds
Lin A is Submodule of Lin B
proof
let R be domRing; ::_thesis: for V being RightMod of R
for A, B being Subset of V st A c= B holds
Lin A is Submodule of Lin B
let V be RightMod of R; ::_thesis: for A, B being Subset of V st A c= B holds
Lin A is Submodule of Lin B
let A, B be Subset of V; ::_thesis: ( A c= B implies Lin A is Submodule of Lin B )
assume A1: A c= B ; ::_thesis: Lin A is Submodule of Lin B
now__::_thesis:_for_v_being_Vector_of_V_st_v_in_Lin_A_holds_
v_in_Lin_B
let v be Vector of V; ::_thesis: ( v in Lin A implies v in Lin B )
assume v in Lin A ; ::_thesis: v in Lin B
then consider l being Linear_Combination of A such that
A2: v = Sum l by Th67;
reconsider l = l as Linear_Combination of B by A1, Th19;
Sum l = v by A2;
hence v in Lin B by Th67; ::_thesis: verum
end;
hence Lin A is Submodule of Lin B by RMOD_2:28; ::_thesis: verum
end;
theorem :: RMOD_4:74
for R being domRing
for V being strict RightMod of R
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
proof
let R be domRing; ::_thesis: for V being strict RightMod of R
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let V be strict RightMod of R; ::_thesis: for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let A, B be Subset of V; ::_thesis: ( Lin A = V & A c= B implies Lin B = V )
assume ( Lin A = V & A c= B ) ; ::_thesis: Lin B = V
then V is Submodule of Lin B by Th73;
hence Lin B = V by RMOD_2:25; ::_thesis: verum
end;
theorem :: RMOD_4:75
for R being domRing
for V being RightMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
proof
let R be domRing; ::_thesis: for V being RightMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
let V be RightMod of R; ::_thesis: for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
let A, B be Subset of V; ::_thesis: Lin (A \/ B) = (Lin A) + (Lin B)
now__::_thesis:_for_v_being_Vector_of_V_st_v_in_Lin_(A_\/_B)_holds_
v_in_(Lin_A)_+_(Lin_B)
deffunc H1( set ) -> Element of the carrier of R = 0. R;
let v be Vector of V; ::_thesis: ( v in Lin (A \/ B) implies v in (Lin A) + (Lin B) )
assume v in Lin (A \/ B) ; ::_thesis: v in (Lin A) + (Lin B)
then consider l being Linear_Combination of A \/ B such that
A1: v = Sum l by Th67;
deffunc H2( set ) -> set = l . $1;
set D = (Carrier l) \ A;
set C = (Carrier l) /\ A;
defpred S1[ set ] means $1 in (Carrier l) /\ A;
defpred S2[ set ] means $1 in (Carrier l) \ A;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_
(_(_x_in_(Carrier_l)_/\_A_implies_l_._x_in_the_carrier_of_R_)_&_(_not_x_in_(Carrier_l)_/\_A_implies_0._R_in_the_carrier_of_R_)_)
let x be set ; ::_thesis: ( x in the carrier of V implies ( ( x in (Carrier l) /\ A implies l . x in the carrier of R ) & ( not x in (Carrier l) /\ A implies 0. R in the carrier of R ) ) )
assume x in the carrier of V ; ::_thesis: ( ( x in (Carrier l) /\ A implies l . x in the carrier of R ) & ( not x in (Carrier l) /\ A implies 0. R in the carrier of R ) )
then reconsider v = x as Vector of V ;
for f being Function of the carrier of V, the carrier of R holds f . v in the carrier of R ;
hence ( x in (Carrier l) /\ A implies l . x in the carrier of R ) ; ::_thesis: ( not x in (Carrier l) /\ A implies 0. R in the carrier of R )
assume not x in (Carrier l) /\ A ; ::_thesis: 0. R in the carrier of R
thus 0. R in the carrier of R ; ::_thesis: verum
end;
then A2: for x being set st x in the carrier of V holds
( ( S1[x] implies H2(x) in the carrier of R ) & ( not S1[x] implies H1(x) in the carrier of R ) ) ;
consider f being Function of the carrier of V, the carrier of R such that
A3: for x being set st x in the carrier of V holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FUNCT_2:sch_5(A2);
reconsider C = (Carrier l) /\ A as finite Subset of V ;
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
for u being Vector of V st not u in C holds
f . u = 0. R by A3;
then reconsider f = f as Linear_Combination of V by Def2;
A4: Carrier f c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in C )
assume x in Carrier f ; ::_thesis: x in C
then A5: ex u being Vector of V st
( x = u & f . u <> 0. R ) ;
assume not x in C ; ::_thesis: contradiction
hence contradiction by A3, A5; ::_thesis: verum
end;
C c= A by XBOOLE_1:17;
then Carrier f c= A by A4, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by Def5;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_
(_(_x_in_(Carrier_l)_\_A_implies_l_._x_in_the_carrier_of_R_)_&_(_not_x_in_(Carrier_l)_\_A_implies_0._R_in_the_carrier_of_R_)_)
let x be set ; ::_thesis: ( x in the carrier of V implies ( ( x in (Carrier l) \ A implies l . x in the carrier of R ) & ( not x in (Carrier l) \ A implies 0. R in the carrier of R ) ) )
assume x in the carrier of V ; ::_thesis: ( ( x in (Carrier l) \ A implies l . x in the carrier of R ) & ( not x in (Carrier l) \ A implies 0. R in the carrier of R ) )
then reconsider v = x as Vector of V ;
for g being Function of the carrier of V, the carrier of R holds g . v in the carrier of R ;
hence ( x in (Carrier l) \ A implies l . x in the carrier of R ) ; ::_thesis: ( not x in (Carrier l) \ A implies 0. R in the carrier of R )
assume not x in (Carrier l) \ A ; ::_thesis: 0. R in the carrier of R
thus 0. R in the carrier of R ; ::_thesis: verum
end;
then A6: for x being set st x in the carrier of V holds
( ( S2[x] implies H2(x) in the carrier of R ) & ( not S2[x] implies H1(x) in the carrier of R ) ) ;
consider g being Function of the carrier of V, the carrier of R such that
A7: for x being set st x in the carrier of V holds
( ( S2[x] implies g . x = H2(x) ) & ( not S2[x] implies g . x = H1(x) ) ) from FUNCT_2:sch_5(A6);
reconsider D = (Carrier l) \ A as finite Subset of V ;
reconsider g = g as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
for u being Vector of V st not u in D holds
g . u = 0. R by A7;
then reconsider g = g as Linear_Combination of V by Def2;
A8: D c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in B )
assume x in D ; ::_thesis: x in B
then A9: ( x in Carrier l & not x in A ) by XBOOLE_0:def_5;
Carrier l c= A \/ B by Def5;
hence x in B by A9, XBOOLE_0:def_3; ::_thesis: verum
end;
Carrier g c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in D )
assume x in Carrier g ; ::_thesis: x in D
then A10: ex u being Vector of V st
( x = u & g . u <> 0. R ) ;
assume not x in D ; ::_thesis: contradiction
hence contradiction by A7, A10; ::_thesis: verum
end;
then Carrier g c= B by A8, XBOOLE_1:1;
then reconsider g = g as Linear_Combination of B by Def5;
l = f + g
proof
let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: l . v = (f + g) . v
now__::_thesis:_(f_+_g)_._v_=_l_._v
percases ( v in C or not v in C ) ;
supposeA11: v in C ; ::_thesis: (f + g) . v = l . v
A12: now__::_thesis:_not_v_in_D
assume v in D ; ::_thesis: contradiction
then not v in A by XBOOLE_0:def_5;
hence contradiction by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
thus (f + g) . v = (f . v) + (g . v) by Def9
.= (l . v) + (g . v) by A3, A11
.= (l . v) + (0. R) by A7, A12
.= l . v by RLVECT_1:4 ; ::_thesis: verum
end;
supposeA13: not v in C ; ::_thesis: l . v = (f + g) . v
now__::_thesis:_(f_+_g)_._v_=_l_._v
percases ( v in Carrier l or not v in Carrier l ) ;
supposeA14: v in Carrier l ; ::_thesis: (f + g) . v = l . v
A15: now__::_thesis:_v_in_D
assume not v in D ; ::_thesis: contradiction
then ( not v in Carrier l or v in A ) by XBOOLE_0:def_5;
hence contradiction by A13, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
thus (f + g) . v = (f . v) + (g . v) by Def9
.= (0. R) + (g . v) by A3, A13
.= g . v by RLVECT_1:4
.= l . v by A7, A15 ; ::_thesis: verum
end;
supposeA16: not v in Carrier l ; ::_thesis: (f + g) . v = l . v
then A17: not v in D by XBOOLE_0:def_5;
A18: not v in C by A16, XBOOLE_0:def_4;
thus (f + g) . v = (f . v) + (g . v) by Def9
.= (0. R) + (g . v) by A3, A18
.= (0. R) + (0. R) by A7, A17
.= 0. R by RLVECT_1:4
.= l . v by A16 ; ::_thesis: verum
end;
end;
end;
hence l . v = (f + g) . v ; ::_thesis: verum
end;
end;
end;
hence l . v = (f + g) . v ; ::_thesis: verum
end;
then A19: v = (Sum f) + (Sum g) by A1, Th58;
( Sum f in Lin A & Sum g in Lin B ) by Th67;
hence v in (Lin A) + (Lin B) by A19, RMOD_3:1; ::_thesis: verum
end;
then A20: Lin (A \/ B) is Submodule of (Lin A) + (Lin B) by RMOD_2:28;
( Lin A is Submodule of Lin (A \/ B) & Lin B is Submodule of Lin (A \/ B) ) by Th73, XBOOLE_1:7;
then (Lin A) + (Lin B) is Submodule of Lin (A \/ B) by RMOD_3:35;
hence Lin (A \/ B) = (Lin A) + (Lin B) by A20, RMOD_2:25; ::_thesis: verum
end;
theorem :: RMOD_4:76
for R being domRing
for V being RightMod of R
for A, B being Subset of V holds Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B)
proof
let R be domRing; ::_thesis: for V being RightMod of R
for A, B being Subset of V holds Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B)
let V be RightMod of R; ::_thesis: for A, B being Subset of V holds Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B)
let A, B be Subset of V; ::_thesis: Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B)
( Lin (A /\ B) is Submodule of Lin A & Lin (A /\ B) is Submodule of Lin B ) by Th73, XBOOLE_1:17;
hence Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B) by RMOD_3:20; ::_thesis: verum
end;