:: RLVECT_2 semantic presentation
begin
definition
let S be 1-sorted ;
let x be set ;
assume A1: x in S ;
func vector (S,x) -> Element of S equals :Def1: :: RLVECT_2:def 1
x;
coherence
x is Element of S by A1, STRUCT_0:def_5;
end;
:: deftheorem Def1 defines vector RLVECT_2:def_1_:_
for S being 1-sorted
for x being set st x in S holds
vector (S,x) = x;
theorem :: RLVECT_2:1
for S being non empty 1-sorted
for v being Element of S holds vector (S,v) = v by Def1, RLVECT_1:1;
theorem Th2: :: RLVECT_2:2
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)
defpred S1[ Element of NAT ] means for F, G, H being FinSequence of the carrier of V st len F = $1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G);
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_F,_G,_H_being_FinSequence_of_the_carrier_of_V_st_len_F_=_k_&_len_F_=_len_G_&_len_F_=_len_H_&_(_for_k_being_Element_of_NAT_st_k_in_dom_F_holds_
H_._k_=_(F_/._k)_+_(G_/._k)_)_holds_
Sum_H_=_(Sum_F)_+_(Sum_G)_)_holds_
for_F,_G,_H_being_FinSequence_of_the_carrier_of_V_st_len_F_=_k_+_1_&_len_F_=_len_G_&_len_F_=_len_H_&_(_for_k_being_Element_of_NAT_st_k_in_dom_F_holds_
H_._k_=_(F_/._k)_+_(G_/._k)_)_holds_
Sum_H_=_(Sum_F)_+_(Sum_G)
let k be Element of NAT ; ::_thesis: ( ( for F, G, H being FinSequence of the carrier of V st len F = k & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G) ) implies for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G) )
assume A1: for F, G, H being FinSequence of the carrier of V st len F = k & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G) ; ::_thesis: for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)
let F, G, H be FinSequence of the carrier of V; ::_thesis: ( len F = k + 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) implies Sum H = (Sum F) + (Sum G) )
assume that
A2: len F = k + 1 and
A3: len F = len G and
A4: len F = len H and
A5: for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ; ::_thesis: Sum H = (Sum F) + (Sum G)
reconsider f = F | (Seg k), g = G | (Seg k), h = H | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18;
A6: len h = k by A2, A4, FINSEQ_3:53;
A7: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A8: k + 1 in dom G by A2, A3, FINSEQ_1:def_3;
then A9: G . (k + 1) in rng G by FUNCT_1:def_3;
k + 1 in dom H by A2, A4, A7, FINSEQ_1:def_3;
then A10: H . (k + 1) in rng H by FUNCT_1:def_3;
A11: k + 1 in dom F by A2, A7, FINSEQ_1:def_3;
then F . (k + 1) in rng F by FUNCT_1:def_3;
then reconsider v = F . (k + 1), u = G . (k + 1), w = H . (k + 1) as Element of V by A9, A10;
A12: w = (F /. (k + 1)) + (G /. (k + 1)) by A5, A11
.= v + (G /. (k + 1)) by A11, PARTFUN1:def_6
.= v + u by A8, PARTFUN1:def_6 ;
G = g ^ <*u*> by A2, A3, FINSEQ_3:55;
then A13: Sum G = (Sum g) + (Sum <*u*>) by RLVECT_1:41;
A14: Sum <*v*> = v by RLVECT_1:44;
A15: len f = k by A2, FINSEQ_3:53;
A16: len g = k by A2, A3, FINSEQ_3:53;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_f_holds_
h_._i_=_(f_/._i)_+_(g_/._i)
let i be Element of NAT ; ::_thesis: ( i in dom f implies h . i = (f /. i) + (g /. i) )
assume A17: i in dom f ; ::_thesis: h . i = (f /. i) + (g /. i)
then A18: F . i = f . i by FUNCT_1:47;
len f <= len F by A2, A15, NAT_1:12;
then A19: dom f c= dom F by FINSEQ_3:30;
then i in dom F by A17;
then i in dom G by A3, FINSEQ_3:29;
then A20: G /. i = G . i by PARTFUN1:def_6;
i in dom h by A15, A6, A17, FINSEQ_3:29;
then A21: H . i = h . i by FUNCT_1:47;
F /. i = F . i by A17, A19, PARTFUN1:def_6;
then A22: f /. i = F /. i by A17, A18, PARTFUN1:def_6;
A23: i in dom g by A15, A16, A17, FINSEQ_3:29;
then G . i = g . i by FUNCT_1:47;
then g /. i = G /. i by A23, A20, PARTFUN1:def_6;
hence h . i = (f /. i) + (g /. i) by A5, A17, A21, A19, A22; ::_thesis: verum
end;
then A24: Sum h = (Sum f) + (Sum g) by A1, A15, A16, A6;
F = f ^ <*v*> by A2, FINSEQ_3:55;
then A25: Sum F = (Sum f) + (Sum <*v*>) by RLVECT_1:41;
A26: Sum <*u*> = u by RLVECT_1:44;
H = h ^ <*w*> by A2, A4, FINSEQ_3:55;
hence Sum H = (Sum h) + (Sum <*w*>) by RLVECT_1:41
.= ((Sum f) + (Sum g)) + (v + u) by A24, A12, RLVECT_1:44
.= (((Sum f) + (Sum g)) + v) + u by RLVECT_1:def_3
.= ((Sum F) + (Sum g)) + u by A25, A14, RLVECT_1:def_3
.= (Sum F) + (Sum G) by A13, A26, RLVECT_1:def_3 ;
::_thesis: verum
end;
then A27: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A28: S1[ 0 ]
proof
let F, G, H be FinSequence of the carrier of V; ::_thesis: ( len F = 0 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) implies Sum H = (Sum F) + (Sum G) )
assume that
A29: len F = 0 and
A30: len F = len G and
A31: len F = len H ; ::_thesis: ( ex k being Element of NAT st
( k in dom F & not H . k = (F /. k) + (G /. k) ) or Sum H = (Sum F) + (Sum G) )
A32: Sum H = 0. V by A29, A31, RLVECT_1:75;
( Sum F = 0. V & Sum G = 0. V ) by A29, A30, RLVECT_1:75;
hence ( ex k being Element of NAT st
( k in dom F & not H . k = (F /. k) + (G /. k) ) or Sum H = (Sum F) + (Sum G) ) by A32, RLVECT_1:4; ::_thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A28, A27);
hence for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G) ; ::_thesis: verum
end;
theorem :: RLVECT_2:3
for V being RealLinearSpace
for a being Real
for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
proof
let V be RealLinearSpace; ::_thesis: for a being Real
for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
let a be Real; ::_thesis: for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
let F, G be FinSequence of V; ::_thesis: ( len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) implies Sum G = a * (Sum F) )
assume that
A1: len F = len G and
A2: for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ; ::_thesis: Sum G = a * (Sum F)
A3: ( dom F = Seg (len F) & dom G = Seg (len G) ) by FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_VECTOR_of_V_st_k_in_dom_G_&_v_=_F_._k_holds_
G_._k_=_a_*_v
let k be Element of NAT ; ::_thesis: for v being VECTOR of V st k in dom G & v = F . k holds
G . k = a * v
let v be VECTOR of V; ::_thesis: ( k in dom G & v = F . k implies G . k = a * v )
assume that
A4: k in dom G and
A5: v = F . k ; ::_thesis: G . k = a * v
v = F /. k by A1, A3, A4, A5, PARTFUN1:def_6;
hence G . k = a * v by A1, A2, A3, A4; ::_thesis: verum
end;
hence Sum G = a * (Sum F) by A1, RLVECT_1:39; ::_thesis: verum
end;
theorem Th4: :: RLVECT_2:4
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = - (F /. k) ) holds
Sum G = - (Sum F)
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = - (F /. k) ) holds
Sum G = - (Sum F)
let F, G be FinSequence of the carrier of V; ::_thesis: ( len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = - (F /. k) ) implies Sum G = - (Sum F) )
assume that
A1: len F = len G and
A2: for k being Element of NAT st k in dom F holds
G . k = - (F /. k) ; ::_thesis: Sum G = - (Sum F)
now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_Element_of_V_st_k_in_dom_G_&_v_=_F_._k_holds_
G_._k_=_-_v
let k be Element of NAT ; ::_thesis: for v being Element of V st k in dom G & v = F . k holds
G . k = - v
let v be Element of V; ::_thesis: ( k in dom G & v = F . k implies G . k = - v )
assume that
A3: k in dom G and
A4: v = F . k ; ::_thesis: G . k = - v
A5: ( dom G = Seg (len G) & dom F = Seg (len F) ) by FINSEQ_1:def_3;
then v = F /. k by A1, A3, A4, PARTFUN1:def_6;
hence G . k = - v by A1, A2, A3, A5; ::_thesis: verum
end;
hence Sum G = - (Sum F) by A1, RLVECT_1:40; ::_thesis: verum
end;
theorem :: RLVECT_2:5
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ) holds
Sum H = (Sum F) - (Sum G)
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ) holds
Sum H = (Sum F) - (Sum G)
let F, G, H be FinSequence of the carrier of V; ::_thesis: ( len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ) implies Sum H = (Sum F) - (Sum G) )
assume that
A1: len F = len G and
A2: len F = len H and
A3: for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ; ::_thesis: Sum H = (Sum F) - (Sum G)
deffunc H1( set ) -> Element of the carrier of V = - (G /. $1);
consider I being FinSequence such that
A4: len I = len G and
A5: for k being Nat st k in dom I holds
I . k = H1(k) from FINSEQ_1:sch_2();
dom I = Seg (len G) by A4, FINSEQ_1:def_3;
then A6: ( dom G = Seg (len G) & ( for k being Element of NAT st k in Seg (len G) holds
I . k = H1(k) ) ) by A5, FINSEQ_1:def_3;
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
A7: y in dom I and
A8: I . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A7;
x = - (G /. y) by A5, A7, A8;
then reconsider v = x as Element of V ;
v in V by RLVECT_1:1;
hence x in the carrier of V ; ::_thesis: verum
end;
then reconsider I = I as FinSequence of the carrier of V by FINSEQ_1:def_4;
A9: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_F_holds_
H_._k_=_(F_/._k)_+_(I_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom F implies H . k = (F /. k) + (I /. k) )
assume A10: k in dom F ; ::_thesis: H . k = (F /. k) + (I /. k)
A11: ( dom F = Seg (len F) & dom I = Seg (len I) ) by FINSEQ_1:def_3;
then A12: I . k = I /. k by A1, A4, A10, PARTFUN1:def_6;
thus H . k = (F /. k) - (G /. k) by A3, A10
.= (F /. k) + (I /. k) by A1, A4, A5, A11, A10, A12 ; ::_thesis: verum
end;
Sum I = - (Sum G) by A4, A6, Th4;
hence Sum H = (Sum F) - (Sum G) by A1, A2, A4, A9, Th2; ::_thesis: verum
end;
theorem Th6: :: RLVECT_2:6
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for F, G being FinSequence of the carrier of V
for f being Permutation of (dom F) st len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) holds
Sum F = Sum G
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for F, G being FinSequence of the carrier of V
for f being Permutation of (dom F) st len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) holds
Sum F = Sum G
let F, G be FinSequence of the carrier of V; ::_thesis: for f being Permutation of (dom F) st len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) holds
Sum F = Sum G
let f be Permutation of (dom F); ::_thesis: ( len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) implies Sum F = Sum G )
defpred S1[ Element of NAT ] means for H1, H2 being FinSequence of the carrier of V st len H1 = $1 & len H1 = len H2 holds
for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2;
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_H1,_H2_being_FinSequence_of_the_carrier_of_V_st_len_H1_=_k_&_len_H1_=_len_H2_holds_
for_f_being_Permutation_of_(dom_H1)_st_(_for_i_being_Element_of_NAT_st_i_in_dom_H2_holds_
H2_._i_=_H1_._(f_._i)_)_holds_
Sum_H1_=_Sum_H2_)_holds_
for_H1,_H2_being_FinSequence_of_the_carrier_of_V_st_len_H1_=_k_+_1_&_len_H1_=_len_H2_holds_
for_f_being_Permutation_of_(dom_H1)_st_(_for_i_being_Element_of_NAT_st_i_in_dom_H2_holds_
H2_._i_=_H1_._(f_._i)_)_holds_
Sum_H1_=_Sum_H2
let k be Element of NAT ; ::_thesis: ( ( for H1, H2 being FinSequence of the carrier of V st len H1 = k & len H1 = len H2 holds
for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2 ) implies for H1, H2 being FinSequence of the carrier of V st len H1 = k + 1 & len H1 = len H2 holds
for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2 )
assume A1: for H1, H2 being FinSequence of the carrier of V st len H1 = k & len H1 = len H2 holds
for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2 ; ::_thesis: for H1, H2 being FinSequence of the carrier of V st len H1 = k + 1 & len H1 = len H2 holds
for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2
let H1, H2 be FinSequence of the carrier of V; ::_thesis: ( len H1 = k + 1 & len H1 = len H2 implies for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2 )
assume that
A2: len H1 = k + 1 and
A3: len H1 = len H2 ; ::_thesis: for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2
reconsider p = H2 | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18;
let f be Permutation of (dom H1); ::_thesis: ( ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) implies Sum H1 = Sum H2 )
A4: dom H1 = Seg (k + 1) by A2, FINSEQ_1:def_3;
then A5: rng f = Seg (k + 1) by FUNCT_2:def_3;
A6: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_f_holds_
f_._n_is_Element_of_NAT
let n be Element of NAT ; ::_thesis: ( n in dom f implies f . n is Element of NAT )
assume n in dom f ; ::_thesis: f . n is Element of NAT
then f . n in Seg (k + 1) by A5, FUNCT_1:def_3;
hence f . n is Element of NAT ; ::_thesis: verum
end;
A7: dom H2 = Seg (k + 1) by A2, A3, FINSEQ_1:def_3;
then reconsider v = H2 . (k + 1) as Element of V by FINSEQ_1:4, FUNCT_1:102;
A8: dom p = Seg (len p) by FINSEQ_1:def_3;
( Seg (k + 1) = {} implies Seg (k + 1) = {} ) ;
then A9: dom f = Seg (k + 1) by A4, FUNCT_2:def_1;
A10: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A11: f . (k + 1) in Seg (k + 1) by A9, A5, FUNCT_1:def_3;
then reconsider n = f . (k + 1) as Element of NAT ;
A12: n <= k + 1 by A11, FINSEQ_1:1;
then consider m2 being Nat such that
A13: n + m2 = k + 1 by NAT_1:10;
defpred S2[ Nat, set ] means $2 = H1 . (n + $1);
1 <= n by A11, FINSEQ_1:1;
then consider m1 being Nat such that
A14: 1 + m1 = n by NAT_1:10;
reconsider m1 = m1, m2 = m2 as Element of NAT by ORDINAL1:def_12;
A15: for j being Nat st j in Seg m2 holds
ex x being set st S2[j,x] ;
consider q2 being FinSequence such that
A16: dom q2 = Seg m2 and
A17: for k being Nat st k in Seg m2 holds
S2[k,q2 . k] from FINSEQ_1:sch_1(A15);
rng q2 c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng q2 or x in the carrier of V )
assume x in rng q2 ; ::_thesis: x in the carrier of V
then consider y being set such that
A18: y in dom q2 and
A19: x = q2 . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A18;
1 <= y by A16, A18, FINSEQ_1:1;
then A20: 1 <= n + y by NAT_1:12;
y <= m2 by A16, A18, FINSEQ_1:1;
then n + y <= len H1 by A2, A13, XREAL_1:7;
then n + y in dom H1 by A20, FINSEQ_3:25;
then reconsider xx = H1 . (n + y) as Element of V by FUNCT_1:102;
xx in the carrier of V ;
hence x in the carrier of V by A16, A17, A18, A19; ::_thesis: verum
end;
then reconsider q2 = q2 as FinSequence of the carrier of V by FINSEQ_1:def_4;
reconsider q1 = H1 | (Seg m1) as FinSequence of the carrier of V by FINSEQ_1:18;
defpred S3[ set , set ] means ( ( f . $1 in dom q1 implies $2 = f . $1 ) & ( not f . $1 in dom q1 implies for l being Element of NAT st l = f . $1 holds
$2 = l - 1 ) );
A21: k <= k + 1 by NAT_1:12;
then A22: Seg k c= Seg (k + 1) by FINSEQ_1:5;
A23: for i being Nat st i in Seg k holds
ex y being set st S3[i,y]
proof
let i be Nat; ::_thesis: ( i in Seg k implies ex y being set st S3[i,y] )
assume A24: i in Seg k ; ::_thesis: ex y being set st S3[i,y]
now__::_thesis:_(_not_f_._i_in_dom_q1_implies_ex_y_being_Element_of_REAL_st_
(_(_f_._i_in_dom_q1_implies_y_=_f_._i_)_&_(_not_f_._i_in_dom_q1_implies_for_t_being_Element_of_NAT_st_t_=_f_._i_holds_
y_=_t_-_1_)_)_)
f . i in Seg (k + 1) by A9, A5, A22, A24, FUNCT_1:def_3;
then reconsider j = f . i as Element of NAT ;
assume A25: not f . i in dom q1 ; ::_thesis: ex y being Element of REAL st
( ( f . i in dom q1 implies y = f . i ) & ( not f . i in dom q1 implies for t being Element of NAT st t = f . i holds
y = t - 1 ) )
take y = j - 1; ::_thesis: ( ( f . i in dom q1 implies y = f . i ) & ( not f . i in dom q1 implies for t being Element of NAT st t = f . i holds
y = t - 1 ) )
thus ( f . i in dom q1 implies y = f . i ) by A25; ::_thesis: ( not f . i in dom q1 implies for t being Element of NAT st t = f . i holds
y = t - 1 )
assume not f . i in dom q1 ; ::_thesis: for t being Element of NAT st t = f . i holds
y = t - 1
let t be Element of NAT ; ::_thesis: ( t = f . i implies y = t - 1 )
assume t = f . i ; ::_thesis: y = t - 1
hence y = t - 1 ; ::_thesis: verum
end;
hence ex y being set st S3[i,y] ; ::_thesis: verum
end;
consider g being FinSequence such that
A26: dom g = Seg k and
A27: for i being Nat st i in Seg k holds
S3[i,g . i] from FINSEQ_1:sch_1(A23);
A28: dom p = Seg k by A2, A3, A21, FINSEQ_1:17;
m1 <= n by A14, NAT_1:11;
then A29: m1 <= k + 1 by A12, XXREAL_0:2;
then A30: dom q1 = Seg m1 by A2, FINSEQ_1:17;
A31: now__::_thesis:_for_i,_l_being_Element_of_NAT_st_l_=_f_._i_&_not_f_._i_in_dom_q1_&_i_in_dom_g_holds_
m1_+_2_<=_l
let i, l be Element of NAT ; ::_thesis: ( l = f . i & not f . i in dom q1 & i in dom g implies m1 + 2 <= l )
assume that
A32: l = f . i and
A33: not f . i in dom q1 and
A34: i in dom g ; ::_thesis: m1 + 2 <= l
A35: ( l < 1 or m1 < l ) by A30, A32, A33, FINSEQ_1:1;
A36: now__::_thesis:_not_m1_+_1_=_l
assume m1 + 1 = l ; ::_thesis: contradiction
then k + 1 = i by A10, A9, A14, A22, A26, A32, A34, FUNCT_1:def_4;
then k + 1 <= k + 0 by A26, A34, FINSEQ_1:1;
hence contradiction by XREAL_1:6; ::_thesis: verum
end;
f . i in rng f by A9, A22, A26, A34, FUNCT_1:def_3;
then m1 + 1 <= l by A4, A32, A35, FINSEQ_1:1, NAT_1:13;
then m1 + 1 < l by A36, XXREAL_0:1;
then (m1 + 1) + 1 <= l by NAT_1:13;
hence m1 + 2 <= l ; ::_thesis: verum
end;
A37: len q1 = m1 by A2, A29, FINSEQ_1:17;
A38: now__::_thesis:_for_j_being_Nat_st_j_in_dom_q2_holds_
H1_._((len_(q1_^_<*v*>))_+_j)_=_q2_._j
let j be Nat; ::_thesis: ( j in dom q2 implies H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j )
assume A39: j in dom q2 ; ::_thesis: H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j
len (q1 ^ <*v*>) = m1 + (len <*v*>) by A37, FINSEQ_1:22
.= n by A14, FINSEQ_1:39 ;
hence H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j by A16, A17, A39; ::_thesis: verum
end;
1 + k = 1 + (m1 + m2) by A14, A13;
then A40: m1 <= k by NAT_1:11;
A41: rng g c= dom p
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in dom p )
assume y in rng g ; ::_thesis: y in dom p
then consider x being set such that
A42: x in dom g and
A43: g . x = y by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A42;
now__::_thesis:_y_in_dom_p
percases ( f . x in dom q1 or not f . x in dom q1 ) ;
supposeA44: f . x in dom q1 ; ::_thesis: y in dom p
A45: dom q1 c= dom p by A40, A30, A28, FINSEQ_1:5;
f . x = g . x by A26, A27, A42, A44;
hence y in dom p by A43, A44, A45; ::_thesis: verum
end;
supposeA46: not f . x in dom q1 ; ::_thesis: y in dom p
reconsider j = f . x as Element of NAT by A9, A22, A6, A26, A42;
A47: f . x in Seg (k + 1) by A9, A5, A22, A26, A42, FUNCT_1:def_3;
( j < 1 or m1 < j ) by A30, A46, FINSEQ_1:1;
then reconsider l = j - 1 as Element of NAT by A47, FINSEQ_1:1, NAT_1:20;
j <= k + 1 by A47, FINSEQ_1:1;
then A48: l <= (k + 1) - 1 by XREAL_1:9;
m1 + 2 <= j by A31, A42, A46;
then A49: (m1 + 2) - 1 <= l by XREAL_1:9;
1 <= m1 + 1 by NAT_1:12;
then A50: 1 <= l by A49, XXREAL_0:2;
g . x = j - 1 by A26, A27, A42, A46;
hence y in dom p by A28, A43, A50, A48, FINSEQ_1:1; ::_thesis: verum
end;
end;
end;
hence y in dom p ; ::_thesis: verum
end;
set q = q1 ^ q2;
A51: len q2 = m2 by A16, FINSEQ_1:def_3;
then A52: len (q1 ^ q2) = m1 + m2 by A37, FINSEQ_1:22;
then A53: dom (q1 ^ q2) = Seg k by A14, A13, FINSEQ_1:def_3;
then reconsider g = g as Function of (dom (q1 ^ q2)),(dom (q1 ^ q2)) by A28, A26, A41, FUNCT_2:2;
A54: len p = k by A2, A3, A21, FINSEQ_1:17;
A55: rng g = dom (q1 ^ q2)
proof
thus rng g c= dom (q1 ^ q2) ; :: according to XBOOLE_0:def_10 ::_thesis: dom (q1 ^ q2) c= rng g
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom (q1 ^ q2) or y in rng g )
assume A56: y in dom (q1 ^ q2) ; ::_thesis: y in rng g
then reconsider j = y as Element of NAT ;
consider x being set such that
A57: x in dom f and
A58: f . x = y by A5, A22, A53, A56, FUNCT_1:def_3;
reconsider x = x as Element of NAT by A9, A57;
now__::_thesis:_y_in_rng_g
percases ( x in dom g or not x in dom g ) ;
supposeA59: x in dom g ; ::_thesis: y in rng g
now__::_thesis:_y_in_rng_g
percases ( f . x in dom q1 or not f . x in dom q1 ) ;
suppose f . x in dom q1 ; ::_thesis: y in rng g
then g . x = f . x by A26, A27, A59;
hence y in rng g by A58, A59, FUNCT_1:def_3; ::_thesis: verum
end;
supposeA60: not f . x in dom q1 ; ::_thesis: y in rng g
j <= k by A53, A56, FINSEQ_1:1;
then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:7;
then j + 1 in rng f by A5, FINSEQ_1:1;
then consider x1 being set such that
A61: x1 in dom f and
A62: f . x1 = j + 1 by FUNCT_1:def_3;
A63: now__::_thesis:_x1_in_dom_g
assume not x1 in dom g ; ::_thesis: contradiction
then x1 in (Seg (k + 1)) \ (Seg k) by A4, A26, A61, XBOOLE_0:def_5;
then x1 in {(k + 1)} by FINSEQ_3:15;
then A64: j + 1 = m1 + 1 by A14, A62, TARSKI:def_1;
1 <= j by A53, A56, FINSEQ_1:1;
hence contradiction by A30, A58, A60, A64, FINSEQ_1:1; ::_thesis: verum
end;
( j < 1 or m1 < j ) by A30, A58, A60, FINSEQ_1:1;
then not j + 1 <= m1 by A53, A56, FINSEQ_1:1, NAT_1:13;
then not f . x1 in dom q1 by A30, A62, FINSEQ_1:1;
then g . x1 = (j + 1) - 1 by A26, A27, A62, A63
.= y ;
hence y in rng g by A63, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
hence y in rng g ; ::_thesis: verum
end;
supposeA65: not x in dom g ; ::_thesis: y in rng g
j <= k by A53, A56, FINSEQ_1:1;
then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:7;
then j + 1 in rng f by A5, FINSEQ_1:1;
then consider x1 being set such that
A66: x1 in dom f and
A67: f . x1 = j + 1 by FUNCT_1:def_3;
x in (Seg (k + 1)) \ (Seg k) by A4, A26, A57, A65, XBOOLE_0:def_5;
then x in {(k + 1)} by FINSEQ_3:15;
then A68: x = k + 1 by TARSKI:def_1;
A69: now__::_thesis:_x1_in_dom_g
assume not x1 in dom g ; ::_thesis: contradiction
then x1 in (Seg (k + 1)) \ (Seg k) by A4, A26, A66, XBOOLE_0:def_5;
then x1 in {(k + 1)} by FINSEQ_3:15;
then j + 1 = j + 0 by A58, A68, A67, TARSKI:def_1;
hence contradiction ; ::_thesis: verum
end;
m1 <= j by A14, A58, A68, XREAL_1:29;
then not j + 1 <= m1 by NAT_1:13;
then not f . x1 in dom q1 by A30, A67, FINSEQ_1:1;
then g . x1 = (j + 1) - 1 by A26, A27, A67, A69
.= y ;
hence y in rng g by A69, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
hence y in rng g ; ::_thesis: verum
end;
assume A70: for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ; ::_thesis: Sum H1 = Sum H2
then A71: H2 . (k + 1) = H1 . (f . (k + 1)) by A7, FINSEQ_1:4;
A72: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(q1_^_<*v*>)_holds_
H1_._j_=_(q1_^_<*v*>)_._j
let j be Nat; ::_thesis: ( j in dom (q1 ^ <*v*>) implies H1 . j = (q1 ^ <*v*>) . j )
assume A73: j in dom (q1 ^ <*v*>) ; ::_thesis: H1 . j = (q1 ^ <*v*>) . j
A74: now__::_thesis:_(_j_in_Seg_m1_implies_H1_._j_=_(q1_^_<*v*>)_._j_)
assume j in Seg m1 ; ::_thesis: H1 . j = (q1 ^ <*v*>) . j
then A75: j in dom q1 by A2, A29, FINSEQ_1:17;
then q1 . j = H1 . j by FUNCT_1:47;
hence H1 . j = (q1 ^ <*v*>) . j by A75, FINSEQ_1:def_7; ::_thesis: verum
end;
A76: now__::_thesis:_(_j_in_{n}_implies_(q1_^_<*v*>)_._j_=_H1_._j_)
( 1 in Seg 1 & len <*v*> = 1 ) by FINSEQ_1:1, FINSEQ_1:39;
then 1 in dom <*v*> by FINSEQ_1:def_3;
then A77: (q1 ^ <*v*>) . ((len q1) + 1) = <*v*> . 1 by FINSEQ_1:def_7;
assume j in {n} ; ::_thesis: (q1 ^ <*v*>) . j = H1 . j
then j = n by TARSKI:def_1;
hence (q1 ^ <*v*>) . j = H1 . j by A71, A14, A37, A77, FINSEQ_1:40; ::_thesis: verum
end;
len (q1 ^ <*v*>) = m1 + (len <*v*>) by A37, FINSEQ_1:22
.= m1 + 1 by FINSEQ_1:40 ;
then j in Seg (m1 + 1) by A73, FINSEQ_1:def_3;
then j in (Seg m1) \/ {n} by A14, FINSEQ_1:9;
hence H1 . j = (q1 ^ <*v*>) . j by A74, A76, XBOOLE_0:def_3; ::_thesis: verum
end;
g is one-to-one
proof
let y1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not y1 in dom g or not b1 in dom g or not g . y1 = g . b1 or y1 = b1 )
let y2 be set ; ::_thesis: ( not y1 in dom g or not y2 in dom g or not g . y1 = g . y2 or y1 = y2 )
assume that
A78: y1 in dom g and
A79: y2 in dom g and
A80: g . y1 = g . y2 ; ::_thesis: y1 = y2
reconsider j1 = y1, j2 = y2 as Element of NAT by A26, A78, A79;
A81: f . y2 in Seg (k + 1) by A9, A5, A22, A26, A79, FUNCT_1:def_3;
A82: f . y1 in Seg (k + 1) by A9, A5, A22, A26, A78, FUNCT_1:def_3;
then reconsider a = f . y1, b = f . y2 as Element of NAT by A81;
now__::_thesis:_y1_=_y2
percases ( ( f . y1 in dom q1 & f . y2 in dom q1 ) or ( f . y1 in dom q1 & not f . y2 in dom q1 ) or ( not f . y1 in dom q1 & f . y2 in dom q1 ) or ( not f . y1 in dom q1 & not f . y2 in dom q1 ) ) ;
suppose ( f . y1 in dom q1 & f . y2 in dom q1 ) ; ::_thesis: y1 = y2
then ( g . j1 = f . y1 & g . j2 = f . y2 ) by A26, A27, A78, A79;
hence y1 = y2 by A9, A22, A26, A78, A79, A80, FUNCT_1:def_4; ::_thesis: verum
end;
supposeA83: ( f . y1 in dom q1 & not f . y2 in dom q1 ) ; ::_thesis: y1 = y2
then A84: a <= m1 by A30, FINSEQ_1:1;
( g . j1 = a & g . j2 = b - 1 ) by A26, A27, A78, A79, A83;
then A85: (b - 1) + 1 <= m1 + 1 by A80, A84, XREAL_1:6;
1 <= b by A81, FINSEQ_1:1;
then A86: b in Seg (m1 + 1) by A85, FINSEQ_1:1;
not b in Seg m1 by A2, A29, A83, FINSEQ_1:17;
then b in (Seg (m1 + 1)) \ (Seg m1) by A86, XBOOLE_0:def_5;
then b in {(m1 + 1)} by FINSEQ_3:15;
then b = m1 + 1 by TARSKI:def_1;
then y2 = k + 1 by A10, A9, A14, A22, A26, A79, FUNCT_1:def_4;
hence y1 = y2 by A26, A79, FINSEQ_3:8; ::_thesis: verum
end;
supposeA87: ( not f . y1 in dom q1 & f . y2 in dom q1 ) ; ::_thesis: y1 = y2
then A88: b <= m1 by A30, FINSEQ_1:1;
( g . j1 = a - 1 & g . j2 = b ) by A26, A27, A78, A79, A87;
then A89: (a - 1) + 1 <= m1 + 1 by A80, A88, XREAL_1:6;
1 <= a by A82, FINSEQ_1:1;
then A90: a in Seg (m1 + 1) by A89, FINSEQ_1:1;
not a in Seg m1 by A2, A29, A87, FINSEQ_1:17;
then a in (Seg (m1 + 1)) \ (Seg m1) by A90, XBOOLE_0:def_5;
then a in {(m1 + 1)} by FINSEQ_3:15;
then a = m1 + 1 by TARSKI:def_1;
then y1 = k + 1 by A10, A9, A14, A22, A26, A78, FUNCT_1:def_4;
hence y1 = y2 by A26, A78, FINSEQ_3:8; ::_thesis: verum
end;
supposeA91: ( not f . y1 in dom q1 & not f . y2 in dom q1 ) ; ::_thesis: y1 = y2
then g . j2 = b - 1 by A26, A27, A79;
then A92: g . y2 = b + (- 1) ;
g . j1 = a - 1 by A26, A27, A78, A91;
then g . j1 = a + (- 1) ;
then a = b by A80, A92, XCMPLX_1:2;
hence y1 = y2 by A9, A22, A26, A78, A79, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
hence y1 = y2 ; ::_thesis: verum
end;
then reconsider g = g as Permutation of (dom (q1 ^ q2)) by A55, FUNCT_2:57;
(len (q1 ^ <*v*>)) + (len q2) = ((len q1) + (len <*v*>)) + m2 by A51, FINSEQ_1:22
.= k + 1 by A14, A13, A37, FINSEQ_1:40 ;
then dom H1 = Seg ((len (q1 ^ <*v*>)) + (len q2)) by A2, FINSEQ_1:def_3;
then A93: H1 = (q1 ^ <*v*>) ^ q2 by A72, A38, FINSEQ_1:def_7;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_p_holds_
p_._i_=_(q1_^_q2)_._(g_._i)
let i be Element of NAT ; ::_thesis: ( i in dom p implies p . i = (q1 ^ q2) . (g . i) )
assume A94: i in dom p ; ::_thesis: p . i = (q1 ^ q2) . (g . i)
then f . i in rng f by A9, A22, A28, FUNCT_1:def_3;
then reconsider j = f . i as Element of NAT by A5;
now__::_thesis:_p_._i_=_(q1_^_q2)_._(g_._i)
percases ( f . i in dom q1 or not f . i in dom q1 ) ;
supposeA95: f . i in dom q1 ; ::_thesis: p . i = (q1 ^ q2) . (g . i)
then A96: ( f . i = g . i & H1 . j = q1 . j ) by A28, A27, A94, FUNCT_1:47;
( H2 . i = p . i & H2 . i = H1 . (f . i) ) by A70, A7, A22, A28, A94, FUNCT_1:47;
hence p . i = (q1 ^ q2) . (g . i) by A95, A96, FINSEQ_1:def_7; ::_thesis: verum
end;
supposeA97: not f . i in dom q1 ; ::_thesis: p . i = (q1 ^ q2) . (g . i)
then m1 + 2 <= j by A28, A26, A31, A94;
then A98: (m1 + 2) - 1 <= j - 1 by XREAL_1:9;
m1 < m1 + 1 by XREAL_1:29;
then A99: m1 < j - 1 by A98, XXREAL_0:2;
then m1 < j by XREAL_1:146, XXREAL_0:2;
then reconsider j1 = j - 1 as Element of NAT by NAT_1:20;
A100: not j1 in dom q1 by A30, A99, FINSEQ_1:1;
A101: g . i = j - 1 by A28, A27, A94, A97;
then j - 1 in dom (q1 ^ q2) by A28, A26, A55, A94, FUNCT_1:def_3;
then consider a being Nat such that
A102: a in dom q2 and
A103: j1 = (len q1) + a by A100, FINSEQ_1:25;
A104: len <*v*> = 1 by FINSEQ_1:39;
A105: ( H2 . i = p . i & H2 . i = H1 . (f . i) ) by A70, A7, A22, A28, A94, FUNCT_1:47;
A106: H1 = q1 ^ (<*v*> ^ q2) by A93, FINSEQ_1:32;
j in dom H1 by A4, A9, A5, A22, A28, A94, FUNCT_1:def_3;
then consider b being Nat such that
A107: b in dom (<*v*> ^ q2) and
A108: j = (len q1) + b by A97, A106, FINSEQ_1:25;
A109: H1 . j = (<*v*> ^ q2) . b by A106, A107, A108, FINSEQ_1:def_7;
A110: b = 1 + a by A103, A108;
(q1 ^ q2) . (j - 1) = q2 . a by A102, A103, FINSEQ_1:def_7;
hence p . i = (q1 ^ q2) . (g . i) by A101, A105, A102, A109, A110, A104, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
hence p . i = (q1 ^ q2) . (g . i) ; ::_thesis: verum
end;
then Sum p = Sum (q1 ^ q2) by A1, A14, A13, A54, A52;
then Sum H2 = (Sum (q1 ^ q2)) + (Sum <*v*>) by A2, A3, A54, A8, RLVECT_1:38, RLVECT_1:44
.= ((Sum q1) + (Sum q2)) + (Sum <*v*>) by RLVECT_1:41
.= (Sum q1) + ((Sum <*v*>) + (Sum q2)) by RLVECT_1:def_3
.= (Sum q1) + (Sum (<*v*> ^ q2)) by RLVECT_1:41
.= Sum (q1 ^ (<*v*> ^ q2)) by RLVECT_1:41
.= Sum H1 by A93, FINSEQ_1:32 ;
hence Sum H1 = Sum H2 ; ::_thesis: verum
end;
then A111: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A112: S1[ 0 ]
proof
let H1, H2 be FinSequence of the carrier of V; ::_thesis: ( len H1 = 0 & len H1 = len H2 implies for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2 )
assume that
A113: len H1 = 0 and
A114: len H1 = len H2 ; ::_thesis: for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2
Sum H1 = 0. V by A113, RLVECT_1:75;
hence for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2 by A113, A114, RLVECT_1:75; ::_thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A112, A111);
hence ( len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) implies Sum F = Sum G ) ; ::_thesis: verum
end;
theorem :: RLVECT_2:7
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for F, G being FinSequence of the carrier of V
for f being Permutation of (dom F) st G = F * f holds
Sum F = Sum G
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for F, G being FinSequence of the carrier of V
for f being Permutation of (dom F) st G = F * f holds
Sum F = Sum G
let F, G be FinSequence of the carrier of V; ::_thesis: for f being Permutation of (dom F) st G = F * f holds
Sum F = Sum G
let f be Permutation of (dom F); ::_thesis: ( G = F * f implies Sum F = Sum G )
assume G = F * f ; ::_thesis: Sum F = Sum G
then ( len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) ) by FINSEQ_2:44, FUNCT_1:12;
hence Sum F = Sum G by Th6; ::_thesis: verum
end;
definition
let V be non empty addLoopStr ;
let T be finite Subset of V;
assume A1: ( V is Abelian & V is add-associative & V is right_zeroed ) ;
func Sum T -> Element of V means :Def2: :: RLVECT_2:def 2
ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & it = Sum F );
existence
ex b1 being Element of V ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b1 = Sum F )
proof
consider p being FinSequence such that
A2: rng p = T and
A3: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of the carrier of V by A2, FINSEQ_1:def_4;
take Sum p ; ::_thesis: ex F being FinSequence of the carrier 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 A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of V st ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b1 = Sum F ) & ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b2 = Sum F ) holds
b1 = b2 by A1, RLVECT_1:42;
end;
:: deftheorem Def2 defines Sum RLVECT_2:def_2_:_
for V being non empty addLoopStr
for T being finite Subset of V st V is Abelian & V is add-associative & V is right_zeroed holds
for b3 being Element of V holds
( b3 = Sum T iff ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b3 = Sum F ) );
theorem Th8: :: RLVECT_2:8
for V being non empty Abelian add-associative right_zeroed addLoopStr holds Sum ({} V) = 0. V
proof
let V be non empty Abelian add-associative right_zeroed addLoopStr ; ::_thesis: Sum ({} V) = 0. V
Sum (<*> the carrier of V) = 0. V by RLVECT_1:43;
hence Sum ({} V) = 0. V by Def2, RELAT_1:38; ::_thesis: verum
end;
theorem :: RLVECT_2:9
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v being Element of V holds Sum {v} = v
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v being Element of V holds Sum {v} = v
let v be Element 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, Def2; ::_thesis: verum
end;
theorem :: RLVECT_2:10
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v1, v2 being Element of V st v1 <> v2 holds
Sum {v1,v2} = v1 + v2
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v1, v2 being Element of V st v1 <> v2 holds
Sum {v1,v2} = v1 + v2
let v1, v2 be Element 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, Def2; ::_thesis: verum
end;
theorem :: RLVECT_2:11
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v1, v2, v3 being Element of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds
Sum {v1,v2,v3} = (v1 + v2) + v3
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v1, v2, v3 being Element of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds
Sum {v1,v2,v3} = (v1 + v2) + v3
let v1, v2, v3 be Element 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, Def2; ::_thesis: verum
end;
theorem Th12: :: RLVECT_2:12
for V being non empty Abelian add-associative right_zeroed addLoopStr
for S, T being finite Subset of V st T misses S holds
Sum (T \/ S) = (Sum T) + (Sum S)
proof
let V be non empty Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for S, T being finite Subset of V st T misses S holds
Sum (T \/ S) = (Sum T) + (Sum S)
let S, T be finite Subset of V; ::_thesis: ( T misses S implies Sum (T \/ S) = (Sum T) + (Sum S) )
consider F being FinSequence of the carrier of V such that
A1: rng F = T \/ S and
A2: ( F is one-to-one & Sum (T \/ S) = Sum F ) by Def2;
consider G being FinSequence of the carrier of V such that
A3: rng G = T and
A4: G is one-to-one and
A5: Sum T = Sum G by Def2;
consider H being FinSequence of the carrier of V such that
A6: rng H = S and
A7: H is one-to-one and
A8: Sum S = Sum H by Def2;
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 Th13: :: RLVECT_2:13
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for S, T being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for S, T being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))
let S, T 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, Th12, XBOOLE_1:103
.= (((Sum (S \ T)) + (Sum (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by Th12, 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, Th12, XBOOLE_1:89
.= (Sum T) + (Sum S) by A2, Th12, XBOOLE_1:89 ;
hence Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) by RLSUB_2:61; ::_thesis: verum
end;
theorem :: RLVECT_2:14
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for S, T being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S))
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for S, T being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S))
let S, T 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 Th13;
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 Th15: :: RLVECT_2:15
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for S, T being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S)
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for S, T being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S)
let S, T 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 Th13;
then Sum (T \/ S) = ((Sum (T \ S)) + (Sum S)) - (0. V) by A1, Th8
.= (Sum (T \ S)) + (Sum S) by RLVECT_1:13 ;
hence Sum (T \ S) = (Sum (T \/ S)) - (Sum S) by RLSUB_2:61; ::_thesis: verum
end;
theorem Th16: :: RLVECT_2:16
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for S, T being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for S, T being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))
let S, T 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 Th15;
hence Sum (T \ S) = (Sum T) - (Sum (T /\ S)) by XBOOLE_1:22; ::_thesis: verum
end;
theorem :: RLVECT_2:17
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))
let S, T 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 Th16
.= (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 :: RLVECT_2:18
for V being non empty Abelian add-associative right_zeroed addLoopStr
for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \ S)) + (Sum (S \ T)) by Th12, XBOOLE_1:82;
definition
let V be non empty ZeroStr ;
mode Linear_Combination of V -> Element of Funcs ( the carrier of V,REAL) means :Def3: :: RLVECT_2:def 3
ex T being finite Subset of V st
for v being Element of V st not v in T holds
it . v = 0 ;
existence
ex b1 being Element of Funcs ( the carrier of V,REAL) ex T being finite Subset of V st
for v being Element of V st not v in T holds
b1 . v = 0
proof
reconsider f = the carrier of V --> 0 as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
take f ; ::_thesis: ex T being finite Subset of V st
for v being Element of V st not v in T holds
f . v = 0
take {} V ; ::_thesis: for v being Element of V st not v in {} V holds
f . v = 0
thus for v being Element of V st not v in {} V holds
f . v = 0 by FUNCOP_1:7; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Linear_Combination RLVECT_2:def_3_:_
for V being non empty ZeroStr
for b2 being Element of Funcs ( the carrier of V,REAL) holds
( b2 is Linear_Combination of V iff ex T being finite Subset of V st
for v being Element of V st not v in T holds
b2 . v = 0 );
notation
let V be non empty addLoopStr ;
let L be Element of Funcs ( the carrier of V,REAL);
synonym Carrier L for support V;
end;
Lm1: now__::_thesis:_for_V_being_non_empty_addLoopStr_
for_L_being_Element_of_Funcs_(_the_carrier_of_V,REAL)_holds_Carrier_c=_the_carrier_of_V
let V be non empty addLoopStr ; ::_thesis: for L being Element of Funcs ( the carrier of V,REAL) holds Carrier c= the carrier of V
let L be Element of Funcs ( the carrier of V,REAL); ::_thesis: Carrier c= the carrier of V
A1: support L c= dom L by PRE_POLY:37;
thus Carrier c= the carrier of V ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier or x in the carrier of V )
assume x in support L ; ::_thesis: x in the carrier of V
then x in dom L by A1;
hence x in the carrier of V ; ::_thesis: verum
end;
end;
definition
let V be non empty addLoopStr ;
let L be Element of Funcs ( the carrier of V,REAL);
:: original: Carrier
redefine func Carrier L -> Subset of V equals :: RLVECT_2:def 4
{ v where v is Element of V : L . v <> 0 } ;
coherence
Carrier is Subset of V by Lm1;
compatibility
for b1 being Subset of V holds
( b1 = Carrier iff b1 = { v where v is Element of V : L . v <> 0 } )
proof
let X be Subset of V; ::_thesis: ( X = Carrier iff X = { v where v is Element of V : L . v <> 0 } )
set A = Carrier ;
set B = { v where v is Element of V : L . v <> 0 } ;
thus ( X = Carrier implies X = { v where v is Element of V : L . v <> 0 } ) ::_thesis: ( X = { v where v is Element of V : L . v <> 0 } implies X = Carrier )
proof
assume A1: X = Carrier ; ::_thesis: X = { v where v is Element of V : L . v <> 0 }
thus X c= { v where v is Element of V : L . v <> 0 } :: according to XBOOLE_0:def_10 ::_thesis: { v where v is Element of V : L . v <> 0 } c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in { v where v is Element of V : L . v <> 0 } )
assume A2: x in X ; ::_thesis: x in { v where v is Element of V : L . v <> 0 }
then L . x <> 0 by A1, PRE_POLY:def_7;
hence x in { v where v is Element of V : L . v <> 0 } by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of V : L . v <> 0 } or x in X )
assume x in { v where v is Element of V : L . v <> 0 } ; ::_thesis: x in X
then ex v being Element of V st
( x = v & L . v <> 0 ) ;
hence x in X by A1, PRE_POLY:def_7; ::_thesis: verum
end;
assume A3: X = { v where v is Element of V : L . v <> 0 } ; ::_thesis: X = Carrier
thus X c= Carrier :: according to XBOOLE_0:def_10 ::_thesis: Carrier c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Carrier )
assume x in X ; ::_thesis: x in Carrier
then ex v being Element of V st
( x = v & L . v <> 0 ) by A3;
hence x in Carrier by PRE_POLY:def_7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier or x in X )
assume A4: x in Carrier ; ::_thesis: x in X
then A5: L . x <> 0 by PRE_POLY:def_7;
Carrier c= the carrier of V by Lm1;
hence x in X by A3, A4, A5; ::_thesis: verum
end;
end;
:: deftheorem defines Carrier RLVECT_2:def_4_:_
for V being non empty addLoopStr
for L being Element of Funcs ( the carrier of V,REAL) holds Carrier L = { v where v is Element of V : L . v <> 0 } ;
registration
let V be non empty addLoopStr ;
let L be Linear_Combination of V;
cluster Carrier -> finite ;
coherence
Carrier L is finite
proof
set A = Carrier L;
consider T being finite Subset of V such that
A1: for v being Element of V st not v in T holds
L . v = 0 by Def3;
Carrier L c= T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier L or x in T )
assume x in Carrier L ; ::_thesis: x in T
then ex v being Element of V st
( x = v & L . v <> 0 ) ;
hence x in T by A1; ::_thesis: verum
end;
hence Carrier L is finite ; ::_thesis: verum
end;
end;
theorem :: RLVECT_2:19
for V being non empty addLoopStr
for L being Linear_Combination of V
for v being Element of V holds
( L . v = 0 iff not v in Carrier L )
proof
let V be non empty addLoopStr ; ::_thesis: for L being Linear_Combination of V
for v being Element of V holds
( L . v = 0 iff not v in Carrier L )
let L be Linear_Combination of V; ::_thesis: for v being Element of V holds
( L . v = 0 iff not v in Carrier L )
let v be Element of V; ::_thesis: ( L . v = 0 iff not v in Carrier L )
thus ( L . v = 0 implies not v in Carrier L ) ::_thesis: ( not v in Carrier L implies L . v = 0 )
proof
assume A1: L . v = 0 ; ::_thesis: not v in Carrier L
assume v in Carrier L ; ::_thesis: contradiction
then ex u being Element of V st
( u = v & L . u <> 0 ) ;
hence contradiction by A1; ::_thesis: verum
end;
thus ( not v in Carrier L implies L . v = 0 ) ; ::_thesis: verum
end;
definition
let V be non empty addLoopStr ;
func ZeroLC V -> Linear_Combination of V means :Def5: :: RLVECT_2:def 5
Carrier it = {} ;
existence
ex b1 being Linear_Combination of V st Carrier b1 = {}
proof
reconsider f = the carrier of V --> 0 as Function of the carrier of V,REAL ;
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
f is Linear_Combination of V
proof
reconsider T = {} V as empty finite Subset of V ;
take T ; :: according to RLVECT_2:def_3 ::_thesis: for v being Element of V st not v in T holds
f . v = 0
thus for v being Element of V st not v in T holds
f . v = 0 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 Element of V : f . v <> 0 } ;
now__::_thesis:_not__{__v_where_v_is_Element_of_V_:_f_._v_<>_0__}__<>_{}
set x = the Element of { v where v is Element of V : f . v <> 0 } ;
assume { v where v is Element of V : f . v <> 0 } <> {} ; ::_thesis: contradiction
then the Element of { v where v is Element of V : f . v <> 0 } in { v where v is Element of V : f . v <> 0 } ;
then ex v being Element of V st
( the Element of { v where v is Element of V : f . v <> 0 } = v & f . v <> 0 ) ;
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
assume L9 . v <> 0 ; ::_thesis: contradiction
then v in { u where u is Element of V : L9 . u <> 0 } ;
hence contradiction by A2; ::_thesis: verum
end;
now__::_thesis:_not_L_._v_<>_0
assume L . v <> 0 ; ::_thesis: contradiction
then v in { u where u is Element of V : L . u <> 0 } ;
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 Def5 defines ZeroLC RLVECT_2:def_5_:_
for V being non empty addLoopStr
for b2 being Linear_Combination of V holds
( b2 = ZeroLC V iff Carrier b2 = {} );
theorem Th20: :: RLVECT_2:20
for V being non empty addLoopStr
for v being Element of V holds (ZeroLC V) . v = 0
proof
let V be non empty addLoopStr ; ::_thesis: for v being Element of V holds (ZeroLC V) . v = 0
let v be Element of V; ::_thesis: (ZeroLC V) . v = 0
( Carrier (ZeroLC V) = {} & not v in {} ) by Def5;
hence (ZeroLC V) . v = 0 ; ::_thesis: verum
end;
definition
let V be non empty addLoopStr ;
let A be Subset of V;
mode Linear_Combination of A -> Linear_Combination of V means :Def6: :: RLVECT_2:def 6
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 Def5;
hence Carrier L c= A by XBOOLE_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines Linear_Combination RLVECT_2:def_6_:_
for V being non empty addLoopStr
for A being Subset of V
for b3 being Linear_Combination of V holds
( b3 is Linear_Combination of A iff Carrier b3 c= A );
theorem :: RLVECT_2:21
for V being RealLinearSpace
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 V be RealLinearSpace; ::_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 Def6;
then Carrier l c= B by A1, XBOOLE_1:1;
hence l is Linear_Combination of B by Def6; ::_thesis: verum
end;
theorem Th22: :: RLVECT_2:22
for V being RealLinearSpace
for A being Subset of V holds ZeroLC V is Linear_Combination of A
proof
let V be RealLinearSpace; ::_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 Def5, XBOOLE_1:2;
hence ZeroLC V is Linear_Combination of A by Def6; ::_thesis: verum
end;
theorem Th23: :: RLVECT_2:23
for V being RealLinearSpace
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V
proof
let V be RealLinearSpace; ::_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 Def6;
then Carrier l = {} ;
hence l = ZeroLC V by Def5; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
let F be FinSequence of V;
let f be Function of the carrier of V,REAL;
funcf (#) F -> FinSequence of the carrier of V means :Def7: :: RLVECT_2:def 7
( len it = len F & ( for i being Element of NAT st i in dom it holds
it . i = (f . (F /. i)) * (F /. i) ) );
existence
ex b1 being FinSequence of the carrier of V st
( len b1 = len F & ( for i being Element of NAT st i in dom b1 holds
b1 . i = (f . (F /. i)) * (F /. i) ) )
proof
deffunc H1( set ) -> Element of the carrier of V = (f . (F /. $1)) * (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 . (F /. y)) * (F /. y) by A2, A3;
hence x in the carrier of V by A4; ::_thesis: verum
end;
then reconsider G = G as FinSequence of the carrier of V by FINSEQ_1:def_4;
take G ; ::_thesis: ( len G = len F & ( for i being Element of NAT st i in dom G holds
G . i = (f . (F /. i)) * (F /. i) ) )
thus ( len G = len F & ( for i being Element of NAT st i in dom G holds
G . i = (f . (F /. i)) * (F /. i) ) ) by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of the carrier of V st len b1 = len F & ( for i being Element of NAT st i in dom b1 holds
b1 . i = (f . (F /. i)) * (F /. i) ) & len b2 = len F & ( for i being Element of NAT st i in dom b2 holds
b2 . i = (f . (F /. i)) * (F /. i) ) holds
b1 = b2
proof
let H1, H2 be FinSequence of V; ::_thesis: ( len H1 = len F & ( for i being Element of NAT st i in dom H1 holds
H1 . i = (f . (F /. i)) * (F /. i) ) & len H2 = len F & ( for i being Element of NAT st i in dom H2 holds
H2 . i = (f . (F /. i)) * (F /. i) ) implies H1 = H2 )
assume that
A5: len H1 = len F and
A6: for i being Element of NAT st i in dom H1 holds
H1 . i = (f . (F /. i)) * (F /. i) and
A7: len H2 = len F and
A8: for i being Element of NAT st i in dom H2 holds
H2 . i = (f . (F /. i)) * (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 . (F /. k)) * (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 Def7 defines (#) RLVECT_2:def_7_:_
for V being RealLinearSpace
for F being FinSequence of V
for f being Function of the carrier of V,REAL
for b4 being FinSequence of the carrier of V holds
( b4 = f (#) F iff ( len b4 = len F & ( for i being Element of NAT st i in dom b4 holds
b4 . i = (f . (F /. i)) * (F /. i) ) ) );
theorem Th24: :: RLVECT_2:24
for i being Element of NAT
for V being RealLinearSpace
for v being VECTOR of V
for F being FinSequence of V
for f being Function of the carrier of V,REAL st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
proof
let i be Element of NAT ; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V
for F being FinSequence of V
for f being Function of the carrier of V,REAL st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for F being FinSequence of V
for f being Function of the carrier of V,REAL st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let v be VECTOR of V; ::_thesis: for F being FinSequence of V
for f being Function of the carrier of V,REAL st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let F be FinSequence of V; ::_thesis: for f being Function of the carrier of V,REAL st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let f be Function of the carrier of V,REAL; ::_thesis: ( i in dom F & v = F . i implies (f (#) F) . i = (f . v) * v )
assume that
A1: i in dom F and
A2: v = F . i ; ::_thesis: (f (#) F) . i = (f . v) * v
A3: F /. i = F . i by A1, PARTFUN1:def_6;
len (f (#) F) = len F by Def7;
then i in dom (f (#) F) by A1, FINSEQ_3:29;
hence (f (#) F) . i = (f . v) * v by A2, A3, Def7; ::_thesis: verum
end;
theorem :: RLVECT_2:25
for V being RealLinearSpace
for f being Function of the carrier of V,REAL holds f (#) (<*> the carrier of V) = <*> the carrier of V
proof
let V be RealLinearSpace; ::_thesis: for f being Function of the carrier of V,REAL holds f (#) (<*> the carrier of V) = <*> the carrier of V
let f be Function of the carrier of V,REAL; ::_thesis: f (#) (<*> the carrier of V) = <*> the carrier of V
len (f (#) (<*> the carrier of V)) = len (<*> the carrier of V) by Def7
.= 0 ;
hence f (#) (<*> the carrier of V) = <*> the carrier of V ; ::_thesis: verum
end;
theorem Th26: :: RLVECT_2:26
for V being RealLinearSpace
for v being VECTOR of V
for f being Function of the carrier of V,REAL holds f (#) <*v*> = <*((f . v) * v)*>
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for f being Function of the carrier of V,REAL holds f (#) <*v*> = <*((f . v) * v)*>
let v be VECTOR of V; ::_thesis: for f being Function of the carrier of V,REAL holds f (#) <*v*> = <*((f . v) * v)*>
let f be Function of the carrier of V,REAL; ::_thesis: f (#) <*v*> = <*((f . v) * v)*>
A1: 1 in {1} by TARSKI:def_1;
A2: len (f (#) <*v*>) = len <*v*> by Def7
.= 1 by FINSEQ_1:40 ;
then dom (f (#) <*v*>) = {1} by FINSEQ_1:2, FINSEQ_1:def_3;
then (f (#) <*v*>) . 1 = (f . (<*v*> /. 1)) * (<*v*> /. 1) by A1, Def7
.= (f . (<*v*> /. 1)) * v by FINSEQ_4:16
.= (f . v) * v by FINSEQ_4:16 ;
hence f (#) <*v*> = <*((f . v) * v)*> by A2, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th27: :: RLVECT_2:27
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for f being Function of the carrier of V,REAL holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
proof
let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V
for f being Function of the carrier of V,REAL holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
let v1, v2 be VECTOR of V; ::_thesis: for f being Function of the carrier of V,REAL holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
let f be Function of the carrier of V,REAL; ::_thesis: f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
A1: len (f (#) <*v1,v2*>) = len <*v1,v2*> by Def7
.= 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 = (f . (<*v1,v2*> /. 2)) * (<*v1,v2*> /. 2) by A2, Def7
.= (f . (<*v1,v2*> /. 2)) * v2 by FINSEQ_4:17
.= (f . v2) * v2 by FINSEQ_4:17 ;
1 in {1,2} by TARSKI:def_2;
then (f (#) <*v1,v2*>) . 1 = (f . (<*v1,v2*> /. 1)) * (<*v1,v2*> /. 1) by A2, Def7
.= (f . (<*v1,v2*> /. 1)) * v1 by FINSEQ_4:17
.= (f . v1) * v1 by FINSEQ_4:17 ;
hence f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> by A1, A3, FINSEQ_1:44; ::_thesis: verum
end;
theorem :: RLVECT_2:28
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for f being Function of the carrier of V,REAL holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
proof
let V be RealLinearSpace; ::_thesis: for v1, v2, v3 being VECTOR of V
for f being Function of the carrier of V,REAL holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
let v1, v2, v3 be VECTOR of V; ::_thesis: for f being Function of the carrier of V,REAL holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
let f be Function of the carrier of V,REAL; ::_thesis: f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
A1: len (f (#) <*v1,v2,v3*>) = len <*v1,v2,v3*> by Def7
.= 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 = (f . (<*v1,v2,v3*> /. 3)) * (<*v1,v2,v3*> /. 3) by A2, Def7
.= (f . (<*v1,v2,v3*> /. 3)) * v3 by FINSEQ_4:18
.= (f . v3) * v3 by FINSEQ_4:18 ;
2 in {1,2,3} by ENUMSET1:def_1;
then A4: (f (#) <*v1,v2,v3*>) . 2 = (f . (<*v1,v2,v3*> /. 2)) * (<*v1,v2,v3*> /. 2) by A2, Def7
.= (f . (<*v1,v2,v3*> /. 2)) * v2 by FINSEQ_4:18
.= (f . v2) * v2 by FINSEQ_4:18 ;
1 in {1,2,3} by ENUMSET1:def_1;
then (f (#) <*v1,v2,v3*>) . 1 = (f . (<*v1,v2,v3*> /. 1)) * (<*v1,v2,v3*> /. 1) by A2, Def7
.= (f . (<*v1,v2,v3*> /. 1)) * v1 by FINSEQ_4:18
.= (f . v1) * v1 by FINSEQ_4:18 ;
hence f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> by A1, A4, A3, FINSEQ_1:45; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
func Sum L -> Element of V means :Def8: :: RLVECT_2:def 8
ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) );
existence
ex b1 being Element 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 the carrier 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 Element 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 Element 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 the carrier 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 the carrier 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: dom F2 = Seg (len F2) by FINSEQ_1:def_3;
A10: dom F1 = Seg (len F1) by FINSEQ_1:def_3;
A11: len F1 = len F2 by A3, A4, A6, A7, FINSEQ_1:48;
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, A11, A10, A9, 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: f is one-to-one
proof
let y1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not y1 in dom f or not b1 in dom f or not f . y1 = f . b1 or y1 = b1 )
let y2 be set ; ::_thesis: ( not y1 in dom f or not y2 in dom f or not f . y1 = f . y2 or y1 = y2 )
assume that
A16: y1 in dom f and
A17: y2 in dom f and
A18: f . y1 = f . y2 ; ::_thesis: y1 = y2
F2 . y1 in rng F1 by A4, A7, A11, A10, A9, A16, FUNCT_1:def_3;
then A19: {(F2 . y1)} c= rng F1 by ZFMISC_1:31;
F2 . y2 in rng F1 by A4, A7, A11, A10, A9, A17, FUNCT_1:def_3;
then A20: {(F2 . y2)} c= rng F1 by ZFMISC_1:31;
( F1 " {(F2 . y1)} = {(f . y1)} & F1 " {(F2 . y2)} = {(f . y2)} ) by A14, A16, A17;
then {(F2 . y1)} = {(F2 . y2)} by A18, A19, A20, FUNCT_1:91;
then F2 . y1 = F2 . y2 by ZFMISC_1:3;
hence y1 = y2 by A6, A11, A10, A9, A16, A17, FUNCT_1:def_4; ::_thesis: verum
end;
set G1 = L (#) F1;
A21: len (L (#) F1) = len F1 by Def7;
A22: rng f = dom F1
proof
thus rng f c= dom F1 ; :: 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 A23: 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
A24: x in dom F2 and
A25: F2 . x = F1 . y by FUNCT_1:def_3;
F1 " {(F2 . x)} = F1 " (Im (F1,y)) by A23, A25, FUNCT_1:59;
then F1 " {(F2 . x)} c= {y} by A3, FUNCT_1:82;
then {(f . x)} c= {y} by A11, A10, A9, A14, A24;
then A26: f . x = y by ZFMISC_1:18;
x in dom f by A11, A10, A9, A24, FUNCT_2:def_1;
hence y in rng f by A26, FUNCT_1:def_3; ::_thesis: verum
end;
then reconsider f = f as Permutation of (dom F1) by A15, 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 A21;
set G2 = L (#) F2;
A27: dom (L (#) F2) = Seg (len (L (#) F2)) by FINSEQ_1:def_3;
A28: len (L (#) F2) = len F2 by Def7;
A29: 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 A30: i in dom (L (#) F2) ; ::_thesis: (L (#) F2) . i = (L (#) F1) . (f . i)
then reconsider u = F2 . i as VECTOR of V by A28, A9, A27, FUNCT_1:102;
A31: ( (L (#) F2) . i = (L . (F2 /. i)) * (F2 /. i) & F2 . i = F2 /. i ) by A28, A9, A27, A30, Def7, PARTFUN1:def_6;
i in dom f by A11, A21, A28, A29, A27, A30, FUNCT_2:def_1;
then A32: f . i in dom F1 by A22, FUNCT_1:def_3;
then reconsider m = f . i as Element of NAT ;
reconsider v = F1 . m as VECTOR of V by A32, FUNCT_1:102;
{(F1 . (f . i))} = Im (F1,(f . i)) by A32, FUNCT_1:59
.= F1 .: (F1 " {(F2 . i)}) by A11, A28, A10, A27, A14, A30 ;
then A33: u = v by FUNCT_1:75, ZFMISC_1:18;
F1 . m = F1 /. m by A32, PARTFUN1:def_6;
hence (L (#) F2) . i = (L (#) F1) . (f . i) by A21, A10, A29, A32, A33, A31, Def7; ::_thesis: verum
end;
hence v1 = v2 by A3, A4, A5, A6, A7, A8, A21, A28, Th6, FINSEQ_1:48; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines Sum RLVECT_2:def_8_:_
for V being RealLinearSpace
for L being Linear_Combination of V
for b3 being Element of V holds
( b3 = Sum L iff ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & b3 = Sum (L (#) F) ) );
Lm2: for V being RealLinearSpace holds Sum (ZeroLC V) = 0. V
proof
let V be RealLinearSpace; ::_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 Def8;
Carrier (ZeroLC V) = {} by Def5;
then F = {} by A1, RELAT_1:41;
then len F = 0 ;
then len ((ZeroLC V) (#) F) = 0 by Def7;
hence Sum (ZeroLC V) = 0. V by A2, RLVECT_1:75; ::_thesis: verum
end;
theorem :: RLVECT_2:29
for V being RealLinearSpace
for A being Subset of V holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V 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: ( ( 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[ Element of NAT ] means for l being Linear_Combination of A st card (Carrier l) = $1 holds
Sum l in A;
assume that
A1: A <> {} and
A2: 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 Def5;
then Sum l = 0. V by Lm2;
hence Sum l in A by A1, A2, RLSUB_1:1; ::_thesis: verum
end;
then A3: 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 A4: 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 REAL = l . $1;
consider F being FinSequence of V such that
A5: F is one-to-one and
A6: rng F = Carrier l and
A7: Sum l = Sum (l (#) F) by Def8;
reconsider G = F | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18;
assume A8: card (Carrier l) = k + 1 ; ::_thesis: Sum l in A
then A9: len F = k + 1 by A5, A6, FINSEQ_4:62;
then A10: len (l (#) F) = k + 1 by Def7;
A11: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A12: k + 1 in dom F by A9, FINSEQ_1:def_3;
k + 1 in dom F by A9, A11, FINSEQ_1:def_3;
then reconsider v = F . (k + 1) as VECTOR of V by FUNCT_1:102;
consider f being Function of the carrier of V,REAL such that
A13: f . v = 0 and
A14: 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,REAL) by FUNCT_2:8;
A15: v in Carrier l by A6, A12, FUNCT_1:def_3;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_Carrier_l_holds_
f_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in Carrier l implies f . u = 0 )
assume A16: not u in Carrier l ; ::_thesis: f . u = 0
hence f . u = l . u by A15, A14
.= 0 by A16 ;
::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def3;
A17: A \ {v} c= A by XBOOLE_1:36;
A18: Carrier l c= A by Def6;
then A19: (l . v) * v in A by A2, A15, RLSUB_1:def_1;
A20: 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
A21: u = x and
A22: f . u <> 0 ;
f . u = l . u by A13, A14, A22;
then A23: x in Carrier l by A21, A22;
not x in {v} by A13, A21, A22, TARSKI:def_1;
hence x in (Carrier l) \ {v} by A23, 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 A24: 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
A25: x = u and
A26: l . u <> 0 ;
not x in {v} by A24, XBOOLE_0:def_5;
then x <> v by TARSKI:def_1;
then l . u = f . u by A14, A25;
hence x in Carrier f by A25, A26; ::_thesis: verum
end;
then Carrier f c= A \ {v} by A18, XBOOLE_1:33;
then Carrier f c= A by A17, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by Def6;
A27: len G = k by A9, FINSEQ_3:53;
then A28: len (f (#) G) = k by Def7;
A29: 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
A30: y in dom G and
A31: G . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A30;
A32: ( dom G c= dom F & G . y = F . y ) by A30, FUNCT_1:47, RELAT_1:60;
now__::_thesis:_not_x_=_v
assume x = v ; ::_thesis: contradiction
then A33: k + 1 = y by A5, A12, A30, A31, A32, FUNCT_1:def_4;
y <= k by A27, A30, FINSEQ_3:25;
hence contradiction by A33, XREAL_1:29; ::_thesis: verum
end;
then A34: not x in {v} by TARSKI:def_1;
x in rng F by A30, A31, A32, FUNCT_1:def_3;
hence x in Carrier f by A6, A20, A34, 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 A35: x in Carrier f ; ::_thesis: x in rng G
then x in rng F by A6, A20, XBOOLE_0:def_5;
then consider y being set such that
A36: y in dom F and
A37: F . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A36;
now__::_thesis:_y_in_Seg_k
assume not y in Seg k ; ::_thesis: contradiction
then y in (dom F) \ (Seg k) by A36, XBOOLE_0:def_5;
then y in (Seg (k + 1)) \ (Seg k) by A9, 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 A20, A35, A37, XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
then y in (dom F) /\ (Seg k) by A36, XBOOLE_0:def_4;
then A38: y in dom G by RELAT_1:61;
then G . y = F . y by FUNCT_1:47;
hence x in rng G by A37, A38, 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 A28, FINSEQ_1:def_3 ;
then A39: dom (f (#) G) = (dom (l (#) F)) /\ (Seg k) by A10, 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 )
assume A40: x in dom (f (#) G) ; ::_thesis: (f (#) G) . x = (l (#) F) . x
then reconsider n = x as Element of NAT ;
n in dom (l (#) F) by A39, A40, XBOOLE_0:def_4;
then A41: n in dom F by A9, A10, FINSEQ_3:29;
then F . n in rng F by FUNCT_1:def_3;
then reconsider w = F . n as VECTOR of V ;
A42: n in dom G by A27, A28, A40, FINSEQ_3:29;
then A43: G . n in rng G by FUNCT_1:def_3;
then reconsider u = G . n as VECTOR of V ;
not u in {v} by A20, A29, A43, XBOOLE_0:def_5;
then A44: u <> v by TARSKI:def_1;
A45: (f (#) G) . n = (f . u) * u by A42, Th24
.= (l . u) * u by A14, A44 ;
w = u by A42, FUNCT_1:47;
hence (f (#) G) . x = (l (#) F) . x by A45, A41, Th24; ::_thesis: verum
end;
then A46: f (#) G = (l (#) F) | (Seg k) by A39, FUNCT_1:46;
v in rng F by A12, FUNCT_1:def_3;
then {v} c= Carrier l by A6, ZFMISC_1:31;
then card (Carrier f) = (k + 1) - (card {v}) by A8, A20, CARD_2:44
.= (k + 1) - 1 by CARD_1:30
.= k ;
then A47: Sum f in A by A4;
G is one-to-one by A5, FUNCT_1:52;
then A48: Sum (f (#) G) = Sum f by A29, Def8;
( dom (f (#) G) = Seg (len (f (#) G)) & (l (#) F) . (len F) = (l . v) * v ) by A9, A12, Th24, FINSEQ_1:def_3;
then Sum (l (#) F) = (Sum (f (#) G)) + ((l . v) * v) by A9, A10, A28, A46, RLVECT_1:38;
hence Sum l in A by A2, A7, A19, A48, A47, RLSUB_1:def_1; ::_thesis: verum
end;
then A49: 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
A50: card (Carrier l) = card (Carrier l) ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A49);
hence Sum l in A by A50; ::_thesis: verum
end;
assume A51: 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 Lm2, Th22;
then A52: 0. V in A by A51;
A53: for a being Real
for v being VECTOR of V st v in A holds
a * v in A
proof
let a be Real; ::_thesis: for v being VECTOR of V st v in A holds
a * v in A
let v be VECTOR of V; ::_thesis: ( v in A implies a * v in A )
assume A54: v in A ; ::_thesis: a * v in A
now__::_thesis:_a_*_v_in_A
percases ( a = 0 or a <> 0 ) ;
suppose a = 0 ; ::_thesis: a * v in A
hence a * v in A by A52, RLVECT_1:10; ::_thesis: verum
end;
supposeA55: a <> 0 ; ::_thesis: a * v in A
deffunc H1( Element of V) -> Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A56: f . v = a and
A57: 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,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v}_holds_
f_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in {v} implies f . u = 0 )
assume not u in {v} ; ::_thesis: f . u = 0
then u <> v by TARSKI:def_1;
hence f . u = 0 by A57; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def3;
A58: 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
A59: x = u and
A60: f . u <> 0 ;
u = v by A57, A60;
hence x in {v} by A59, 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 A55, A56; ::_thesis: verum
end;
{v} c= A by A54, ZFMISC_1:31;
then reconsider f = f as Linear_Combination of A by A58, Def6;
consider F being FinSequence of V such that
A61: ( F is one-to-one & rng F = Carrier f ) and
A62: Sum (f (#) F) = Sum f by Def8;
F = <*v*> by A58, A61, FINSEQ_3:97;
then f (#) F = <*((f . v) * v)*> by Th26;
then Sum f = a * v by A56, A62, RLVECT_1:44;
hence a * v in A by A51; ::_thesis: verum
end;
end;
end;
hence a * v 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 RLSUB_1:def_1 ::_thesis: for b1 being Element of REAL
for b2 being Element of the carrier of V holds
( not b2 in A or b1 * b2 in A )
proof
let v, u be VECTOR of V; ::_thesis: ( v in A & u in A implies v + u in A )
assume that
A63: v in A and
A64: 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 = (1 * v) + v by RLVECT_1:def_8
.= (1 * v) + (1 * v) by RLVECT_1:def_8
.= (1 + 1) * v by RLVECT_1:def_6
.= 2 * v ;
hence v + u in A by A53, A63; ::_thesis: verum
end;
supposeA65: v <> u ; ::_thesis: v + u in A
deffunc H1( Element of V) -> Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A66: ( f . v = 1 & f . u = 1 ) and
A67: for w being Element of V st w <> v & w <> u holds
f . w = H1(w) from FUNCT_2:sch_7(A65);
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_w_being_VECTOR_of_V_st_not_w_in_{v,u}_holds_
f_._w_=_0
let w be VECTOR of V; ::_thesis: ( not w in {v,u} implies f . w = 0 )
assume not w in {v,u} ; ::_thesis: f . w = 0
then ( w <> v & w <> u ) by TARSKI:def_2;
hence f . w = 0 by A67; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def3;
A68: 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 ) ;
then ( x = v or x = u ) by A67;
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 A66; ::_thesis: verum
end;
then A69: Carrier f c= A by A63, A64, ZFMISC_1:32;
A70: ( 1 * u = u & 1 * v = v ) by RLVECT_1:def_8;
reconsider f = f as Linear_Combination of A by A69, Def6;
consider F being FinSequence of V such that
A71: ( F is one-to-one & rng F = Carrier f ) and
A72: Sum (f (#) F) = Sum f by Def8;
( F = <*v,u*> or F = <*u,v*> ) by A65, A68, A71, FINSEQ_3:99;
then ( f (#) F = <*(1 * v),(1 * u)*> or f (#) F = <*(1 * u),(1 * v)*> ) by A66, Th27;
then Sum f = v + u by A72, A70, RLVECT_1:45;
hence v + u in A by A51; ::_thesis: verum
end;
end;
end;
hence v + u in A ; ::_thesis: verum
end;
thus for b1 being Element of REAL
for b2 being Element of the carrier of V holds
( not b2 in A or b1 * b2 in A ) by A53; ::_thesis: verum
end;
theorem :: RLVECT_2:30
for V being RealLinearSpace holds Sum (ZeroLC V) = 0. V by Lm2;
theorem :: RLVECT_2:31
for V being RealLinearSpace
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V
proof
let V be RealLinearSpace; ::_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 Th23;
hence Sum l = 0. V by Lm2; ::_thesis: verum
end;
theorem Th32: :: RLVECT_2:32
for V being RealLinearSpace
for v being VECTOR of V
for l being Linear_Combination of {v} holds Sum l = (l . v) * v
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for l being Linear_Combination of {v} holds Sum l = (l . v) * v
let v be VECTOR of V; ::_thesis: for l being Linear_Combination of {v} holds Sum l = (l . v) * v
let l be Linear_Combination of {v}; ::_thesis: Sum l = (l . v) * v
A1: Carrier l c= {v} by Def6;
now__::_thesis:_Sum_l_=_(l_._v)_*_v
percases ( Carrier l = {} or Carrier l = {v} ) by A1, ZFMISC_1:33;
suppose Carrier l = {} ; ::_thesis: Sum l = (l . v) * v
then A2: l = ZeroLC V by Def5;
hence Sum l = 0. V by Lm2
.= 0 * v by RLVECT_1:10
.= (l . v) * v by A2, Th20 ;
::_thesis: verum
end;
suppose Carrier l = {v} ; ::_thesis: Sum l = (l . v) * 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 Def8;
F = <*v*> by A3, FINSEQ_3:97;
then l (#) F = <*((l . v) * v)*> by Th26;
hence Sum l = (l . v) * v by A4, RLVECT_1:44; ::_thesis: verum
end;
end;
end;
hence Sum l = (l . v) * v ; ::_thesis: verum
end;
theorem Th33: :: RLVECT_2:33
for V being RealLinearSpace
for v1, v2 being VECTOR of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)
proof
let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)
let v1, v2 be VECTOR of V; ::_thesis: ( v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) )
assume A1: v1 <> v2 ; ::_thesis: for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)
let l be Linear_Combination of {v1,v2}; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
A2: Carrier l c= {v1,v2} by Def6;
now__::_thesis:_Sum_l_=_((l_._v1)_*_v1)_+_((l_._v2)_*_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 = ((l . v1) * v1) + ((l . v2) * v2)
then A3: l = ZeroLC V by Def5;
hence Sum l = 0. V by Lm2
.= (0. V) + (0. V) by RLVECT_1:4
.= (0 * v1) + (0. V) by RLVECT_1:10
.= (0 * v1) + (0 * v2) by RLVECT_1:10
.= ((l . v1) * v1) + (0 * v2) by A3, Th20
.= ((l . v1) * v1) + ((l . v2) * v2) by A3, Th20 ;
::_thesis: verum
end;
supposeA4: Carrier l = {v1} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
then reconsider L = l as Linear_Combination of {v1} by Def6;
A5: not v2 in Carrier l by A1, A4, TARSKI:def_1;
thus Sum l = Sum L
.= (l . v1) * v1 by Th32
.= ((l . v1) * v1) + (0. V) by RLVECT_1:4
.= ((l . v1) * v1) + (0 * v2) by RLVECT_1:10
.= ((l . v1) * v1) + ((l . v2) * v2) by A5 ; ::_thesis: verum
end;
supposeA6: Carrier l = {v2} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
then reconsider L = l as Linear_Combination of {v2} by Def6;
A7: not v1 in Carrier l by A1, A6, TARSKI:def_1;
thus Sum l = Sum L
.= (l . v2) * v2 by Th32
.= (0. V) + ((l . v2) * v2) by RLVECT_1:4
.= (0 * v1) + ((l . v2) * v2) by RLVECT_1:10
.= ((l . v1) * v1) + ((l . v2) * v2) by A7 ; ::_thesis: verum
end;
suppose Carrier l = {v1,v2} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * 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 Def8;
( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A8, FINSEQ_3:99;
then ( l (#) F = <*((l . v1) * v1),((l . v2) * v2)*> or l (#) F = <*((l . v2) * v2),((l . v1) * v1)*> ) by Th27;
hence Sum l = ((l . v1) * v1) + ((l . v2) * v2) by A9, RLVECT_1:45; ::_thesis: verum
end;
end;
end;
hence Sum l = ((l . v1) * v1) + ((l . v2) * v2) ; ::_thesis: verum
end;
theorem :: RLVECT_2:34
for V being RealLinearSpace
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V
proof
let V be RealLinearSpace; ::_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 Def5;
hence Sum L = 0. V by Lm2; ::_thesis: verum
end;
theorem :: RLVECT_2:35
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = (L . v) * v
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = (L . v) * v
let v be VECTOR of V; ::_thesis: for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = (L . v) * v
let L be Linear_Combination of V; ::_thesis: ( Carrier L = {v} implies Sum L = (L . v) * v )
assume Carrier L = {v} ; ::_thesis: Sum L = (L . v) * v
then L is Linear_Combination of {v} by Def6;
hence Sum L = (L . v) * v by Th32; ::_thesis: verum
end;
theorem :: RLVECT_2:36
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = ((L . v1) * v1) + ((L . v2) * v2)
proof
let V be RealLinearSpace; ::_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 = ((L . v1) * v1) + ((L . v2) * 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 = ((L . v1) * v1) + ((L . v2) * v2)
let L be Linear_Combination of V; ::_thesis: ( Carrier L = {v1,v2} & v1 <> v2 implies Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
assume that
A1: Carrier L = {v1,v2} and
A2: v1 <> v2 ; ::_thesis: Sum L = ((L . v1) * v1) + ((L . v2) * v2)
L is Linear_Combination of {v1,v2} by A1, Def6;
hence Sum L = ((L . v1) * v1) + ((L . v2) * v2) by A2, Th33; ::_thesis: verum
end;
definition
let V be non empty addLoopStr ;
let L1, L2 be Linear_Combination of V;
:: original: =
redefine predL1 = L2 means :: RLVECT_2:def 9
for v being Element of V holds L1 . v = L2 . v;
compatibility
( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) by FUNCT_2:63;
end;
:: deftheorem defines = RLVECT_2:def_9_:_
for V being non empty addLoopStr
for L1, L2 being Linear_Combination of V holds
( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v );
definition
let V be non empty addLoopStr ;
let L1, L2 be Linear_Combination of V;
:: original: +
redefine funcL1 + L2 -> Linear_Combination of V means :Def10: :: RLVECT_2:def 10
for v being Element of V holds it . v = (L1 . v) + (L2 . v);
coherence
L1 + L2 is Linear_Combination of V
proof
reconsider f = L1 + L2 as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_v_being_Element_of_V_st_not_v_in_(Carrier_L1)_\/_(Carrier_L2)_holds_
f_._v_=_0
let v be Element of V; ::_thesis: ( not v in (Carrier L1) \/ (Carrier L2) implies f . v = 0 )
assume A1: not v in (Carrier L1) \/ (Carrier L2) ; ::_thesis: f . v = 0
then not v in Carrier L2 by XBOOLE_0:def_3;
then A2: L2 . v = 0 ;
not v in Carrier L1 by A1, XBOOLE_0:def_3;
then L1 . v = 0 ;
hence f . v = 0 + 0 by A2, VALUED_1:1
.= 0 ;
::_thesis: verum
end;
hence L1 + L2 is Linear_Combination of V by Def3; ::_thesis: verum
end;
compatibility
for b1 being Linear_Combination of V holds
( b1 = L1 + L2 iff for v being Element of V holds b1 . v = (L1 . v) + (L2 . v) )
proof
let f be Linear_Combination of V; ::_thesis: ( f = L1 + L2 iff for v being Element of V holds f . v = (L1 . v) + (L2 . v) )
thus ( f = L1 + L2 implies for v being Element of V holds f . v = (L1 . v) + (L2 . v) ) by VALUED_1:1; ::_thesis: ( ( for v being Element of V holds f . v = (L1 . v) + (L2 . v) ) implies f = L1 + L2 )
assume A3: for v being Element of V holds f . v = (L1 . v) + (L2 . v) ; ::_thesis: f = L1 + L2
thus f = L1 + L2 ::_thesis: verum
proof
let v be Element of the carrier of V; :: according to FUNCT_2:def_8 ::_thesis: f . v = (L1 + L2) . v
thus f . v = (L1 . v) + (L2 . v) by A3
.= (L1 + L2) . v by VALUED_1:1 ; ::_thesis: verum
end;
end;
end;
:: deftheorem Def10 defines + RLVECT_2:def_10_:_
for V being non empty addLoopStr
for L1, L2, b4 being Linear_Combination of V holds
( b4 = L1 + L2 iff for v being Element of V holds b4 . v = (L1 . v) + (L2 . v) );
theorem Th37: :: RLVECT_2:37
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
proof
let V be RealLinearSpace; ::_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 ;
(L1 + L2) . u = (L1 . u) + (L2 . u) by Def10;
then ( L1 . u <> 0 or L2 . u <> 0 ) by A2;
then ( x in { v1 where v1 is VECTOR of V : L1 . v1 <> 0 } or x in { v2 where v2 is VECTOR of V : L2 . v2 <> 0 } ) by A1;
hence x in (Carrier L1) \/ (Carrier L2) by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th38: :: RLVECT_2:38
for V being RealLinearSpace
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 V be RealLinearSpace; ::_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 Def6;
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 RLVECT_2:def_6 ::_thesis: verum
end;
theorem :: RLVECT_2:39
for V being non empty addLoopStr
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1 ;
theorem Th40: :: RLVECT_2:40
for V being RealLinearSpace
for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3
proof
let V be RealLinearSpace; ::_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 RLVECT_2:def_9 ::_thesis: (L1 + (L2 + L3)) . v = ((L1 + L2) + L3) . v
thus (L1 + (L2 + L3)) . v = (L1 . v) + ((L2 + L3) . v) by Def10
.= (L1 . v) + ((L2 . v) + (L3 . v)) by Def10
.= ((L1 . v) + (L2 . v)) + (L3 . v)
.= ((L1 + L2) . v) + (L3 . v) by Def10
.= ((L1 + L2) + L3) . v by Def10 ; ::_thesis: verum
end;
theorem Th41: :: RLVECT_2:41
for V being RealLinearSpace
for L being Linear_Combination of V holds
( L + (ZeroLC V) = L & (ZeroLC V) + L = L )
proof
let V be RealLinearSpace; ::_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 RLVECT_2:def_9 ::_thesis: (L + (ZeroLC V)) . v = L . v
thus (L + (ZeroLC V)) . v = (L . v) + ((ZeroLC V) . v) by Def10
.= (L . v) + 0 by Th20
.= L . v ; ::_thesis: verum
end;
hence (ZeroLC V) + L = L ; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
let a be Real;
let L be Linear_Combination of V;
funca * L -> Linear_Combination of V means :Def11: :: RLVECT_2:def 11
for v being VECTOR of V holds it . v = a * (L . v);
existence
ex b1 being Linear_Combination of V st
for v being VECTOR of V holds b1 . v = a * (L . v)
proof
deffunc H1( Element of V) -> Element of REAL = a * (L . $1);
consider f being Function of the carrier of V,REAL 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,REAL) by FUNCT_2:8;
now__::_thesis:_for_v_being_VECTOR_of_V_st_not_v_in_Carrier_L_holds_
f_._v_=_0
let v be VECTOR of V; ::_thesis: ( not v in Carrier L implies f . v = 0 )
assume not v in Carrier L ; ::_thesis: f . v = 0
then L . v = 0 ;
hence f . v = a * 0 by A1
.= 0 ;
::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def3;
take f ; ::_thesis: for v being VECTOR of V holds f . v = a * (L . v)
let v be VECTOR of V; ::_thesis: f . v = a * (L . v)
thus f . v = a * (L . 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 = a * (L . v) ) & ( for v being VECTOR of V holds b2 . v = a * (L . v) ) holds
b1 = b2
proof
let L1, L2 be Linear_Combination of V; ::_thesis: ( ( for v being VECTOR of V holds L1 . v = a * (L . v) ) & ( for v being VECTOR of V holds L2 . v = a * (L . v) ) implies L1 = L2 )
assume A2: for v being VECTOR of V holds L1 . v = a * (L . v) ; ::_thesis: ( ex v being VECTOR of V st not L2 . v = a * (L . v) or L1 = L2 )
assume A3: for v being VECTOR of V holds L2 . v = a * (L . v) ; ::_thesis: L1 = L2
let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: L1 . v = L2 . v
thus L1 . v = a * (L . v) by A2
.= L2 . v by A3 ; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines * RLVECT_2:def_11_:_
for V being RealLinearSpace
for a being Real
for L, b4 being Linear_Combination of V holds
( b4 = a * L iff for v being VECTOR of V holds b4 . v = a * (L . v) );
theorem Th42: :: RLVECT_2:42
for V being RealLinearSpace
for a being Real
for L being Linear_Combination of V st a <> 0 holds
Carrier (a * L) = Carrier L
proof
let V be RealLinearSpace; ::_thesis: for a being Real
for L being Linear_Combination of V st a <> 0 holds
Carrier (a * L) = Carrier L
let a be Real; ::_thesis: for L being Linear_Combination of V st a <> 0 holds
Carrier (a * L) = Carrier L
let L be Linear_Combination of V; ::_thesis: ( a <> 0 implies Carrier (a * L) = Carrier L )
set T = { u where u is VECTOR of V : (a * L) . u <> 0 } ;
set S = { v where v is VECTOR of V : L . v <> 0 } ;
assume A1: a <> 0 ; ::_thesis: Carrier (a * L) = Carrier L
{ u where u is VECTOR of V : (a * L) . u <> 0 } = { v where v is VECTOR of V : L . v <> 0 }
proof
thus { u where u is VECTOR of V : (a * L) . u <> 0 } c= { v where v is VECTOR of V : L . v <> 0 } :: according to XBOOLE_0:def_10 ::_thesis: { v where v is VECTOR of V : L . v <> 0 } c= { u where u is VECTOR of V : (a * L) . u <> 0 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is VECTOR of V : (a * L) . u <> 0 } or x in { v where v is VECTOR of V : L . v <> 0 } )
assume x in { u where u is VECTOR of V : (a * L) . u <> 0 } ; ::_thesis: x in { v where v is VECTOR of V : L . v <> 0 }
then consider u being VECTOR of V such that
A2: x = u and
A3: (a * L) . u <> 0 ;
(a * L) . u = a * (L . u) by Def11;
then L . u <> 0 by A3;
hence x in { v where v is VECTOR of V : L . v <> 0 } by A2; ::_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 } or x in { u where u is VECTOR of V : (a * L) . u <> 0 } )
assume x in { v where v is VECTOR of V : L . v <> 0 } ; ::_thesis: x in { u where u is VECTOR of V : (a * L) . u <> 0 }
then consider v being VECTOR of V such that
A4: x = v and
A5: L . v <> 0 ;
(a * L) . v = a * (L . v) by Def11;
then (a * L) . v <> 0 by A1, A5, XCMPLX_1:6;
hence x in { u where u is VECTOR of V : (a * L) . u <> 0 } by A4; ::_thesis: verum
end;
hence Carrier (a * L) = Carrier L ; ::_thesis: verum
end;
theorem Th43: :: RLVECT_2:43
for V being RealLinearSpace
for L being Linear_Combination of V holds 0 * L = ZeroLC V
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds 0 * L = ZeroLC V
let L be Linear_Combination of V; ::_thesis: 0 * L = ZeroLC V
let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (0 * L) . v = (ZeroLC V) . v
thus (0 * L) . v = 0 * (L . v) by Def11
.= (ZeroLC V) . v by Th20 ; ::_thesis: verum
end;
theorem Th44: :: RLVECT_2:44
for V being RealLinearSpace
for a being Real
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A
proof
let V be RealLinearSpace; ::_thesis: for a being Real
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A
let a be Real; ::_thesis: for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L 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
a * L is Linear_Combination of A
let L be Linear_Combination of V; ::_thesis: ( L is Linear_Combination of A implies a * L is Linear_Combination of A )
assume A1: L is Linear_Combination of A ; ::_thesis: a * L is Linear_Combination of A
now__::_thesis:_a_*_L_is_Linear_Combination_of_A
percases ( a = 0 or a <> 0 ) ;
suppose a = 0 ; ::_thesis: a * L is Linear_Combination of A
then a * L = ZeroLC V by Th43;
hence a * L is Linear_Combination of A by Th22; ::_thesis: verum
end;
suppose a <> 0 ; ::_thesis: a * L is Linear_Combination of A
then Carrier (a * L) = Carrier L by Th42;
hence a * L is Linear_Combination of A by A1, Def6; ::_thesis: verum
end;
end;
end;
hence a * L is Linear_Combination of A ; ::_thesis: verum
end;
theorem Th45: :: RLVECT_2:45
for V being RealLinearSpace
for a, b being Real
for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)
proof
let V be RealLinearSpace; ::_thesis: for a, b being Real
for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)
let a, b be Real; ::_thesis: for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)
let L be Linear_Combination of V; ::_thesis: (a + b) * L = (a * L) + (b * L)
let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: ((a + b) * L) . v = ((a * L) + (b * L)) . v
thus ((a + b) * L) . v = (a + b) * (L . v) by Def11
.= (a * (L . v)) + (b * (L . v))
.= ((a * L) . v) + (b * (L . v)) by Def11
.= ((a * L) . v) + ((b * L) . v) by Def11
.= ((a * L) + (b * L)) . v by Def10 ; ::_thesis: verum
end;
theorem Th46: :: RLVECT_2:46
for V being RealLinearSpace
for a being Real
for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)
proof
let V be RealLinearSpace; ::_thesis: for a being Real
for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)
let a be Real; ::_thesis: for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)
let L1, L2 be Linear_Combination of V; ::_thesis: a * (L1 + L2) = (a * L1) + (a * L2)
let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (a * (L1 + L2)) . v = ((a * L1) + (a * L2)) . v
thus (a * (L1 + L2)) . v = a * ((L1 + L2) . v) by Def11
.= a * ((L1 . v) + (L2 . v)) by Def10
.= (a * (L1 . v)) + (a * (L2 . v))
.= ((a * L1) . v) + (a * (L2 . v)) by Def11
.= ((a * L1) . v) + ((a * L2) . v) by Def11
.= ((a * L1) + (a * L2)) . v by Def10 ; ::_thesis: verum
end;
theorem Th47: :: RLVECT_2:47
for V being RealLinearSpace
for a, b being Real
for L being Linear_Combination of V holds a * (b * L) = (a * b) * L
proof
let V be RealLinearSpace; ::_thesis: for a, b being Real
for L being Linear_Combination of V holds a * (b * L) = (a * b) * L
let a, b be Real; ::_thesis: for L being Linear_Combination of V holds a * (b * L) = (a * b) * L
let L be Linear_Combination of V; ::_thesis: a * (b * L) = (a * b) * L
let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (a * (b * L)) . v = ((a * b) * L) . v
thus (a * (b * L)) . v = a * ((b * L) . v) by Def11
.= a * (b * (L . v)) by Def11
.= (a * b) * (L . v)
.= ((a * b) * L) . v by Def11 ; ::_thesis: verum
end;
theorem Th48: :: RLVECT_2:48
for V being RealLinearSpace
for L being Linear_Combination of V holds 1 * L = L
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds 1 * L = L
let L be Linear_Combination of V; ::_thesis: 1 * L = L
let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (1 * L) . v = L . v
thus (1 * L) . v = 1 * (L . v) by Def11
.= L . v ; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
func - L -> Linear_Combination of V equals :: RLVECT_2:def 12
(- 1) * L;
correctness
coherence
(- 1) * L is Linear_Combination of V;
;
end;
:: deftheorem defines - RLVECT_2:def_12_:_
for V being RealLinearSpace
for L being Linear_Combination of V holds - L = (- 1) * L;
theorem Th49: :: RLVECT_2:49
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V holds (- L) . v = - (L . v)
proof
let V be RealLinearSpace; ::_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 = (- 1) * (L . v) by Def11
.= - (L . v) ; ::_thesis: verum
end;
theorem :: RLVECT_2:50
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1
proof
let V be RealLinearSpace; ::_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 RLVECT_2:def_9 ::_thesis: L2 . v = (- L1) . v
(L1 . v) + (L2 . v) = (ZeroLC V) . v by A1, Def10
.= 0 by Th20 ;
hence L2 . v = - (L1 . v)
.= (- L1) . v by Th49 ;
::_thesis: verum
end;
theorem :: RLVECT_2:51
for V being RealLinearSpace
for L being Linear_Combination of V holds Carrier (- L) = Carrier L by Th42;
theorem :: RLVECT_2:52
for V being RealLinearSpace
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 Th44;
theorem :: RLVECT_2:53
for V being RealLinearSpace
for L being Linear_Combination of V holds - (- L) = L
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds - (- L) = L
let L be Linear_Combination of V; ::_thesis: - (- L) = L
let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (- (- L)) . v = L . v
thus (- (- L)) . v = (((- 1) * (- 1)) * L) . v by Th47
.= 1 * (L . v) by Def11
.= L . v ; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
let L1, L2 be Linear_Combination of V;
funcL1 - L2 -> Linear_Combination of V equals :: RLVECT_2:def 13
L1 + (- L2);
correctness
coherence
L1 + (- L2) is Linear_Combination of V;
;
end;
:: deftheorem defines - RLVECT_2:def_13_:_
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);
theorem Th54: :: RLVECT_2:54
for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
proof
let V be RealLinearSpace; ::_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 Def10
.= (L1 . v) + (- (L2 . v)) by Th49
.= (L1 . v) - (L2 . v) ; ::_thesis: verum
end;
theorem :: RLVECT_2:55
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
proof
let V be RealLinearSpace; ::_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 Th42; ::_thesis: verum
end;
theorem :: RLVECT_2:56
for V being RealLinearSpace
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 V be RealLinearSpace; ::_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, Th44;
hence L1 - L2 is Linear_Combination of A by A1, Th38; ::_thesis: verum
end;
theorem Th57: :: RLVECT_2:57
for V being RealLinearSpace
for L being Linear_Combination of V holds L - L = ZeroLC V
proof
let V be RealLinearSpace; ::_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 RLVECT_2:def_9 ::_thesis: (L - L) . v = (ZeroLC V) . v
thus (L - L) . v = (L . v) - (L . v) by Th54
.= (ZeroLC V) . v by Th20 ; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
func LinComb V -> set means :Def14: :: RLVECT_2:def 14
for x being set holds
( x in it iff x is Linear_Combination of V );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is Linear_Combination of V )
proof
defpred S1[ set ] means $1 is Linear_Combination of V;
consider A being set such that
A1: for x being set holds
( x in A iff ( x in Funcs ( the carrier of V,REAL) & S1[x] ) ) from XBOOLE_0:sch_1();
take A ; ::_thesis: for x being set holds
( x in A iff x is Linear_Combination of V )
let x be set ; ::_thesis: ( x in A iff x is Linear_Combination of V )
thus ( x in A implies x is Linear_Combination of V ) by A1; ::_thesis: ( x is Linear_Combination of V implies x in A )
assume x is Linear_Combination of V ; ::_thesis: x in A
hence x in A by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Linear_Combination of V ) ) & ( for x being set holds
( x in b2 iff x is Linear_Combination of V ) ) holds
b1 = b2
proof
let D1, D2 be set ; ::_thesis: ( ( for x being set holds
( x in D1 iff x is Linear_Combination of V ) ) & ( for x being set holds
( x in D2 iff x is Linear_Combination of V ) ) implies D1 = D2 )
assume A2: for x being set holds
( x in D1 iff x is Linear_Combination of V ) ; ::_thesis: ( ex x being set st
( ( x in D2 implies x is Linear_Combination of V ) implies ( x is Linear_Combination of V & not x in D2 ) ) or D1 = D2 )
assume A3: for x being set holds
( x in D2 iff x is Linear_Combination of V ) ; ::_thesis: D1 = D2
thus D1 c= D2 :: according to XBOOLE_0:def_10 ::_thesis: D2 c= D1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 or x in D2 )
assume x in D1 ; ::_thesis: x in D2
then x is Linear_Combination of V by A2;
hence x in D2 by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D2 or x in D1 )
assume x in D2 ; ::_thesis: x in D1
then x is Linear_Combination of V by A3;
hence x in D1 by A2; ::_thesis: verum
end;
end;
:: deftheorem Def14 defines LinComb RLVECT_2:def_14_:_
for V being RealLinearSpace
for b2 being set holds
( b2 = LinComb V iff for x being set holds
( x in b2 iff x is Linear_Combination of V ) );
registration
let V be RealLinearSpace;
cluster LinComb V -> non empty ;
coherence
not LinComb V is empty
proof
set x = the Linear_Combination of V;
the Linear_Combination of V in LinComb V by Def14;
hence not LinComb V is empty ; ::_thesis: verum
end;
end;
definition
let V be RealLinearSpace;
let e be Element of LinComb V;
func @ e -> Linear_Combination of V equals :: RLVECT_2:def 15
e;
coherence
e is Linear_Combination of V by Def14;
end;
:: deftheorem defines @ RLVECT_2:def_15_:_
for V being RealLinearSpace
for e being Element of LinComb V holds @ e = e;
definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
func @ L -> Element of LinComb V equals :: RLVECT_2:def 16
L;
coherence
L is Element of LinComb V by Def14;
end;
:: deftheorem defines @ RLVECT_2:def_16_:_
for V being RealLinearSpace
for L being Linear_Combination of V holds @ L = L;
definition
let V be RealLinearSpace;
func LCAdd V -> BinOp of (LinComb V) means :Def17: :: RLVECT_2:def 17
for e1, e2 being Element of LinComb V holds it . (e1,e2) = (@ e1) + (@ e2);
existence
ex b1 being BinOp of (LinComb V) st
for e1, e2 being Element of LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2)
proof
deffunc H1( Element of LinComb V, Element of LinComb V) -> Element of LinComb V = @ ((@ $1) + (@ $2));
consider o being BinOp of (LinComb V) such that
A1: for e1, e2 being Element of LinComb V holds o . (e1,e2) = H1(e1,e2) from BINOP_1:sch_4();
take o ; ::_thesis: for e1, e2 being Element of LinComb V holds o . (e1,e2) = (@ e1) + (@ e2)
let e1, e2 be Element of LinComb V; ::_thesis: o . (e1,e2) = (@ e1) + (@ e2)
thus o . (e1,e2) = @ ((@ e1) + (@ e2)) by A1
.= (@ e1) + (@ e2) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (LinComb V) st ( for e1, e2 being Element of LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of LinComb V holds b2 . (e1,e2) = (@ e1) + (@ e2) ) holds
b1 = b2
proof
let o1, o2 be BinOp of (LinComb V); ::_thesis: ( ( for e1, e2 being Element of LinComb V holds o1 . (e1,e2) = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of LinComb V holds o2 . (e1,e2) = (@ e1) + (@ e2) ) implies o1 = o2 )
assume A2: for e1, e2 being Element of LinComb V holds o1 . (e1,e2) = (@ e1) + (@ e2) ; ::_thesis: ( ex e1, e2 being Element of LinComb V st not o2 . (e1,e2) = (@ e1) + (@ e2) or o1 = o2 )
assume A3: for e1, e2 being Element of LinComb V holds o2 . (e1,e2) = (@ e1) + (@ e2) ; ::_thesis: o1 = o2
now__::_thesis:_for_e1,_e2_being_Element_of_LinComb_V_holds_o1_._(e1,e2)_=_o2_._(e1,e2)
let e1, e2 be Element of LinComb V; ::_thesis: o1 . (e1,e2) = o2 . (e1,e2)
thus o1 . (e1,e2) = (@ e1) + (@ e2) by A2
.= o2 . (e1,e2) by A3 ; ::_thesis: verum
end;
hence o1 = o2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def17 defines LCAdd RLVECT_2:def_17_:_
for V being RealLinearSpace
for b2 being BinOp of (LinComb V) holds
( b2 = LCAdd V iff for e1, e2 being Element of LinComb V holds b2 . (e1,e2) = (@ e1) + (@ e2) );
definition
let V be RealLinearSpace;
func LCMult V -> Function of [:REAL,(LinComb V):],(LinComb V) means :Def18: :: RLVECT_2:def 18
for a being Real
for e being Element of LinComb V holds it . [a,e] = a * (@ e);
existence
ex b1 being Function of [:REAL,(LinComb V):],(LinComb V) st
for a being Real
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e)
proof
defpred S1[ Element of REAL , Element of LinComb V, set ] means ex a being Real st
( a = $1 & $3 = a * (@ $2) );
A1: for x being Element of REAL
for e1 being Element of LinComb V ex e2 being Element of LinComb V st S1[x,e1,e2]
proof
let x be Element of REAL ; ::_thesis: for e1 being Element of LinComb V ex e2 being Element of LinComb V st S1[x,e1,e2]
let e1 be Element of LinComb V; ::_thesis: ex e2 being Element of LinComb V st S1[x,e1,e2]
take @ (x * (@ e1)) ; ::_thesis: S1[x,e1, @ (x * (@ e1))]
take x ; ::_thesis: ( x = x & @ (x * (@ e1)) = x * (@ e1) )
thus ( x = x & @ (x * (@ e1)) = x * (@ e1) ) ; ::_thesis: verum
end;
consider g being Function of [:REAL,(LinComb V):],(LinComb V) such that
A2: for x being Element of REAL
for e being Element of LinComb V holds S1[x,e,g . (x,e)] from BINOP_1:sch_3(A1);
take g ; ::_thesis: for a being Real
for e being Element of LinComb V holds g . [a,e] = a * (@ e)
let a be Real; ::_thesis: for e being Element of LinComb V holds g . [a,e] = a * (@ e)
let e be Element of LinComb V; ::_thesis: g . [a,e] = a * (@ e)
ex b being Real st
( b = a & g . (a,e) = b * (@ e) ) by A2;
hence g . [a,e] = a * (@ e) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of [:REAL,(LinComb V):],(LinComb V) st ( for a being Real
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e) ) & ( for a being Real
for e being Element of LinComb V holds b2 . [a,e] = a * (@ e) ) holds
b1 = b2
proof
let g1, g2 be Function of [:REAL,(LinComb V):],(LinComb V); ::_thesis: ( ( for a being Real
for e being Element of LinComb V holds g1 . [a,e] = a * (@ e) ) & ( for a being Real
for e being Element of LinComb V holds g2 . [a,e] = a * (@ e) ) implies g1 = g2 )
assume A3: for a being Real
for e being Element of LinComb V holds g1 . [a,e] = a * (@ e) ; ::_thesis: ( ex a being Real ex e being Element of LinComb V st not g2 . [a,e] = a * (@ e) or g1 = g2 )
assume A4: for a being Real
for e being Element of LinComb V holds g2 . [a,e] = a * (@ e) ; ::_thesis: g1 = g2
now__::_thesis:_for_x_being_Element_of_REAL_
for_e_being_Element_of_LinComb_V_holds_g1_._(x,e)_=_g2_._(x,e)
let x be Element of REAL ; ::_thesis: for e being Element of LinComb V holds g1 . (x,e) = g2 . (x,e)
let e be Element of LinComb V; ::_thesis: g1 . (x,e) = g2 . (x,e)
thus g1 . (x,e) = x * (@ e) by A3
.= g2 . (x,e) by A4 ; ::_thesis: verum
end;
hence g1 = g2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines LCMult RLVECT_2:def_18_:_
for V being RealLinearSpace
for b2 being Function of [:REAL,(LinComb V):],(LinComb V) holds
( b2 = LCMult V iff for a being Real
for e being Element of LinComb V holds b2 . [a,e] = a * (@ e) );
definition
let V be RealLinearSpace;
func LC_RLSpace V -> RLSStruct equals :: RLVECT_2:def 19
RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #);
coherence
RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #) is RLSStruct ;
end;
:: deftheorem defines LC_RLSpace RLVECT_2:def_19_:_
for V being RealLinearSpace holds LC_RLSpace V = RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #);
registration
let V be RealLinearSpace;
cluster LC_RLSpace V -> non empty strict ;
coherence
( LC_RLSpace V is strict & not LC_RLSpace V is empty ) ;
end;
registration
let V be RealLinearSpace;
cluster LC_RLSpace V -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( LC_RLSpace V is Abelian & LC_RLSpace V is add-associative & LC_RLSpace V is right_zeroed & LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )
proof
set S = LC_RLSpace V;
A1: now__::_thesis:_for_v,_u_being_VECTOR_of_(LC_RLSpace_V)
for_K,_L_being_Linear_Combination_of_V_st_v_=_K_&_u_=_L_holds_
v_+_u_=_K_+_L
let v, u be VECTOR of (LC_RLSpace V); ::_thesis: for K, L being Linear_Combination of V st v = K & u = L holds
v + u = K + L
let K, L be Linear_Combination of V; ::_thesis: ( v = K & u = L implies v + u = K + L )
A2: ( @ (@ K) = K & @ (@ L) = L ) ;
assume ( v = K & u = L ) ; ::_thesis: v + u = K + L
hence v + u = K + L by A2, Def17; ::_thesis: verum
end;
thus LC_RLSpace V is Abelian ::_thesis: ( LC_RLSpace V is add-associative & LC_RLSpace V is right_zeroed & LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )
proof
let u, v be Element of (LC_RLSpace V); :: according to RLVECT_1:def_2 ::_thesis: u + v = v + u
reconsider K = u, L = v as Linear_Combination of V by Def14;
thus u + v = L + K by A1
.= v + u by A1 ; ::_thesis: verum
end;
thus LC_RLSpace V is add-associative ::_thesis: ( LC_RLSpace V is right_zeroed & LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )
proof
let u, v, w be Element of (LC_RLSpace V); :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w)
reconsider L = u, K = v, M = w as Linear_Combination of V by Def14;
A3: v + w = K + M by A1;
u + v = L + K by A1;
hence (u + v) + w = (L + K) + M by A1
.= L + (K + M) by Th40
.= u + (v + w) by A1, A3 ;
::_thesis: verum
end;
thus LC_RLSpace V is right_zeroed ::_thesis: ( LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )
proof
let v be Element of (LC_RLSpace V); :: according to RLVECT_1:def_4 ::_thesis: v + (0. (LC_RLSpace V)) = v
reconsider K = v as Linear_Combination of V by Def14;
thus v + (0. (LC_RLSpace V)) = K + (ZeroLC V) by A1
.= v by Th41 ; ::_thesis: verum
end;
thus LC_RLSpace V is right_complementable ::_thesis: ( LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )
proof
let v be Element of (LC_RLSpace V); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider K = v as Linear_Combination of V by Def14;
- K in the carrier of (LC_RLSpace V) by Def14;
then - K in LC_RLSpace V by STRUCT_0:def_5;
then - K = vector ((LC_RLSpace V),(- K)) by Def1;
then v + (vector ((LC_RLSpace V),(- K))) = K - K by A1
.= 0. (LC_RLSpace V) by Th57 ;
hence ex w being VECTOR of (LC_RLSpace V) st v + w = 0. (LC_RLSpace V) ; :: according to ALGSTR_0:def_11 ::_thesis: verum
end;
A4: now__::_thesis:_for_v_being_VECTOR_of_(LC_RLSpace_V)
for_L_being_Linear_Combination_of_V
for_a_being_Real_st_v_=_L_holds_
a_*_v_=_a_*_L
let v be VECTOR of (LC_RLSpace V); ::_thesis: for L being Linear_Combination of V
for a being Real st v = L holds
a * v = a * L
let L be Linear_Combination of V; ::_thesis: for a being Real st v = L holds
a * v = a * L
let a be Real; ::_thesis: ( v = L implies a * v = a * L )
A5: @ (@ L) = L ;
assume v = L ; ::_thesis: a * v = a * L
hence a * v = a * L by A5, Def18; ::_thesis: verum
end;
thus for a being real number
for v, w being VECTOR of (LC_RLSpace V) holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def_5 ::_thesis: ( LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )
proof
let a be real number ; ::_thesis: for v, w being VECTOR of (LC_RLSpace V) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of (LC_RLSpace V); ::_thesis: a * (v + w) = (a * v) + (a * w)
reconsider K = v, M = w as Linear_Combination of V by Def14;
reconsider a = a as Real by XREAL_0:def_1;
A6: ( a * v = a * K & a * w = a * M ) by A4;
v + w = K + M by A1;
then a * (v + w) = a * (K + M) by A4
.= (a * K) + (a * M) by Th46
.= (a * v) + (a * w) by A1, A6 ;
hence a * (v + w) = (a * v) + (a * w) ; ::_thesis: verum
end;
thus for a, b being real number
for v being VECTOR of (LC_RLSpace V) holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def_6 ::_thesis: ( LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )
proof
let a, b be real number ; ::_thesis: for v being VECTOR of (LC_RLSpace V) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of (LC_RLSpace V); ::_thesis: (a + b) * v = (a * v) + (b * v)
reconsider K = v as Linear_Combination of V by Def14;
reconsider a = a, b = b as Real by XREAL_0:def_1;
A7: ( a * v = a * K & b * v = b * K ) by A4;
(a + b) * v = (a + b) * K by A4
.= (a * K) + (b * K) by Th45
.= (a * v) + (b * v) by A1, A7 ;
hence (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum
end;
thus for a, b being real number
for v being VECTOR of (LC_RLSpace V) holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def_7 ::_thesis: LC_RLSpace V is scalar-unital
proof
let a, b be real number ; ::_thesis: for v being VECTOR of (LC_RLSpace V) holds (a * b) * v = a * (b * v)
let v be VECTOR of (LC_RLSpace V); ::_thesis: (a * b) * v = a * (b * v)
reconsider K = v as Linear_Combination of V by Def14;
reconsider a = a, b = b as Real by XREAL_0:def_1;
A8: b * v = b * K by A4;
(a * b) * v = (a * b) * K by A4
.= a * (b * K) by Th47
.= a * (b * v) by A4, A8 ;
hence (a * b) * v = a * (b * v) ; ::_thesis: verum
end;
let v be VECTOR of (LC_RLSpace V); :: according to RLVECT_1:def_8 ::_thesis: 1 * v = v
reconsider K = v as Linear_Combination of V by Def14;
thus 1 * v = 1 * K by A4
.= v by Th48 ; ::_thesis: verum
end;
end;
theorem :: RLVECT_2:58
for V being RealLinearSpace holds the carrier of (LC_RLSpace V) = LinComb V ;
theorem :: RLVECT_2:59
for V being RealLinearSpace holds 0. (LC_RLSpace V) = ZeroLC V ;
theorem :: RLVECT_2:60
for V being RealLinearSpace holds the addF of (LC_RLSpace V) = LCAdd V ;
theorem :: RLVECT_2:61
for V being RealLinearSpace holds the Mult of (LC_RLSpace V) = LCMult V ;
theorem Th62: :: RLVECT_2:62
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds (vector ((LC_RLSpace V),L1)) + (vector ((LC_RLSpace V),L2)) = L1 + L2
proof
let V be RealLinearSpace; ::_thesis: for L1, L2 being Linear_Combination of V holds (vector ((LC_RLSpace V),L1)) + (vector ((LC_RLSpace V),L2)) = L1 + L2
let L1, L2 be Linear_Combination of V; ::_thesis: (vector ((LC_RLSpace V),L1)) + (vector ((LC_RLSpace V),L2)) = L1 + L2
set v2 = vector ((LC_RLSpace V),L2);
A1: ( L1 = @ (@ L1) & L2 = @ (@ L2) ) ;
L2 in the carrier of (LC_RLSpace V) by Def14;
then A2: L2 in LC_RLSpace V by STRUCT_0:def_5;
L1 in the carrier of (LC_RLSpace V) by Def14;
then L1 in LC_RLSpace V by STRUCT_0:def_5;
hence (vector ((LC_RLSpace V),L1)) + (vector ((LC_RLSpace V),L2)) = (LCAdd V) . [L1,(vector ((LC_RLSpace V),L2))] by Def1
.= (LCAdd V) . ((@ L1),(@ L2)) by A2, Def1
.= L1 + L2 by A1, Def17 ;
::_thesis: verum
end;
theorem Th63: :: RLVECT_2:63
for V being RealLinearSpace
for a being Real
for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L
proof
let V be RealLinearSpace; ::_thesis: for a being Real
for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L
let a be Real; ::_thesis: for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L
let L be Linear_Combination of V; ::_thesis: a * (vector ((LC_RLSpace V),L)) = a * L
A1: @ (@ L) = L ;
L in the carrier of (LC_RLSpace V) by Def14;
then L in LC_RLSpace V by STRUCT_0:def_5;
hence a * (vector ((LC_RLSpace V),L)) = (LCMult V) . [a,(@ L)] by Def1
.= a * L by A1, Def18 ;
::_thesis: verum
end;
theorem Th64: :: RLVECT_2:64
for V being RealLinearSpace
for L being Linear_Combination of V holds - (vector ((LC_RLSpace V),L)) = - L
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds - (vector ((LC_RLSpace V),L)) = - L
let L be Linear_Combination of V; ::_thesis: - (vector ((LC_RLSpace V),L)) = - L
thus - (vector ((LC_RLSpace V),L)) = (- 1) * (vector ((LC_RLSpace V),L)) by RLVECT_1:16
.= - L by Th63 ; ::_thesis: verum
end;
theorem :: RLVECT_2:65
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2
proof
let V be RealLinearSpace; ::_thesis: for L1, L2 being Linear_Combination of V holds (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2
let L1, L2 be Linear_Combination of V; ::_thesis: (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2
- L2 in LinComb V by Def14;
then A1: - L2 in LC_RLSpace V by STRUCT_0:def_5;
- (vector ((LC_RLSpace V),L2)) = - L2 by Th64
.= vector ((LC_RLSpace V),(- L2)) by A1, Def1 ;
hence (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2 by Th62; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
let A be Subset of V;
func LC_RLSpace A -> strict Subspace of LC_RLSpace V means :: RLVECT_2:def 20
the carrier of it = { l where l is Linear_Combination of A : verum } ;
existence
ex b1 being strict Subspace of LC_RLSpace V st the carrier of b1 = { l where l is Linear_Combination of A : verum }
proof
set X = { l where l is Linear_Combination of A : verum } ;
{ l where l is Linear_Combination of A : verum } c= the carrier of (LC_RLSpace V)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { l where l is Linear_Combination of A : verum } or x in the carrier of (LC_RLSpace V) )
assume x in { l where l is Linear_Combination of A : verum } ; ::_thesis: x in the carrier of (LC_RLSpace V)
then ex l being Linear_Combination of A st x = l ;
hence x in the carrier of (LC_RLSpace V) by Def14; ::_thesis: verum
end;
then reconsider X = { l where l is Linear_Combination of A : verum } as Subset of (LC_RLSpace V) ;
A1: X is linearly-closed
proof
thus for v, u being VECTOR of (LC_RLSpace V) st v in X & u in X holds
v + u in X :: according to RLSUB_1:def_1 ::_thesis: for b1 being Element of REAL
for b2 being Element of the carrier of (LC_RLSpace V) holds
( not b2 in X or b1 * b2 in X )
proof
let v, u be VECTOR of (LC_RLSpace V); ::_thesis: ( v in X & u in X implies v + u in X )
assume that
A2: v in X and
A3: u in X ; ::_thesis: v + u in X
consider l1 being Linear_Combination of A such that
A4: v = l1 by A2;
consider l2 being Linear_Combination of A such that
A5: u = l2 by A3;
A6: u = vector ((LC_RLSpace V),l2) by A5, Def1, RLVECT_1:1;
v = vector ((LC_RLSpace V),l1) by A4, Def1, RLVECT_1:1;
then v + u = l1 + l2 by A6, Th62;
then v + u is Linear_Combination of A by Th38;
hence v + u in X ; ::_thesis: verum
end;
let a be Real; ::_thesis: for b1 being Element of the carrier of (LC_RLSpace V) holds
( not b1 in X or a * b1 in X )
let v be VECTOR of (LC_RLSpace V); ::_thesis: ( not v in X or a * v in X )
assume v in X ; ::_thesis: a * v in X
then consider l being Linear_Combination of A such that
A7: v = l ;
a * v = a * (vector ((LC_RLSpace V),l)) by A7, Def1, RLVECT_1:1
.= a * l by Th63 ;
then a * v is Linear_Combination of A by Th44;
hence a * v in X ; ::_thesis: verum
end;
ZeroLC V is Linear_Combination of A by Th22;
then ZeroLC V in X ;
hence ex b1 being strict Subspace of LC_RLSpace V st the carrier of b1 = { l where l is Linear_Combination of A : verum } by A1, RLSUB_1:35; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subspace of LC_RLSpace V st the carrier of b1 = { l where l is Linear_Combination of A : verum } & the carrier of b2 = { l where l is Linear_Combination of A : verum } holds
b1 = b2 by RLSUB_1:30;
end;
:: deftheorem defines LC_RLSpace RLVECT_2:def_20_:_
for V being RealLinearSpace
for A being Subset of V
for b3 being strict Subspace of LC_RLSpace V holds
( b3 = LC_RLSpace A iff the carrier of b3 = { l where l is Linear_Combination of A : verum } );
theorem Th66: :: RLVECT_2:66
for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT
for v being Element of V st k in dom F & v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)
proof
let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT
for v being Element of V st k in dom F & v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)
let a be Element of R; ::_thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT
for v being Element of V st k in dom F & v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R; ::_thesis: for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT
for v being Element of V st k in dom F & v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)
let F, G be FinSequence of V; ::_thesis: ( len F = len G & ( for k being Element of NAT
for v being Element of V st k in dom F & v = G . k holds
F . k = a * v ) implies Sum F = a * (Sum G) )
defpred S1[ Element of NAT ] means for H, I being FinSequence of V st len H = len I & len H = $1 & ( for k being Element of NAT
for v being Element of V st k in dom H & v = I . k holds
H . k = a * v ) holds
Sum H = a * (Sum I);
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Element of NAT
for v being Element of V st k in dom H & v = I . k holds
H . k = a * v ) holds
Sum H = a * (Sum I) ; ::_thesis: S1[n + 1]
let H, I be FinSequence of V; ::_thesis: ( len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being Element of V st k in dom H & v = I . k holds
H . k = a * v ) implies Sum H = a * (Sum I) )
assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k being Element of NAT
for v being Element of V st k in dom H & v = I . k holds
H . k = a * v ; ::_thesis: Sum H = a * (Sum I)
reconsider p = H | (Seg n), q = I | (Seg n) as FinSequence of V by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12;
then A7: q = I | (dom q) by A3, A4, FINSEQ_1:17;
A8: len p = n by A4, A6, FINSEQ_1:17;
A9: len q = n by A3, A4, A6, FINSEQ_1:17;
A10: now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_Element_of_V_st_k_in_dom_p_&_v_=_q_._k_holds_
p_._k_=_a_*_v
A11: dom p c= dom H by A4, A6, A8, FINSEQ_3:30;
let k be Element of NAT ; ::_thesis: for v being Element of V st k in dom p & v = q . k holds
p . k = a * v
let v be Element of V; ::_thesis: ( k in dom p & v = q . k implies p . k = a * v )
assume that
A12: k in dom p and
A13: v = q . k ; ::_thesis: p . k = a * v
dom q = dom p by A8, A9, FINSEQ_3:29;
then I . k = q . k by A12, FUNCT_1:47;
then H . k = a * v by A5, A12, A13, A11;
hence p . k = a * v by A12, FUNCT_1:47; ::_thesis: verum
end;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A14: n + 1 in dom H by A4, FINSEQ_1:def_3;
dom H = dom I by A3, FINSEQ_3:29;
then reconsider v1 = H . (n + 1), v2 = I . (n + 1) as Element of V by A14, FINSEQ_2:11;
A15: v1 = a * v2 by A5, A14;
p = H | (dom p) by A4, A6, FINSEQ_1:17;
hence Sum H = (Sum p) + v1 by A4, A8, RLVECT_1:38
.= (a * (Sum q)) + (a * v2) by A2, A8, A9, A10, A15
.= a * ((Sum q) + v2) by VECTSP_1:def_14
.= a * (Sum I) by A3, A4, A9, A7, RLVECT_1:38 ;
::_thesis: verum
end;
A16: S1[ 0 ]
proof
let H, I be FinSequence of V; ::_thesis: ( len H = len I & len H = 0 & ( for k being Element of NAT
for v being Element of V st k in dom H & v = I . k holds
H . k = a * v ) implies Sum H = a * (Sum I) )
assume that
A17: len H = len I and
A18: len H = 0 and
for k being Element of NAT
for v being Element of V st k in dom H & v = I . k holds
H . k = a * v ; ::_thesis: Sum H = a * (Sum I)
H = <*> the carrier of V by A18;
then A19: Sum H = 0. V by RLVECT_1:43;
I = <*> the carrier of V by A17, A18;
then Sum I = 0. V by RLVECT_1:43;
hence Sum H = a * (Sum I) by A19, VECTSP_1:14; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A16, A1);
hence ( len F = len G & ( for k being Element of NAT
for v being Element of V st k in dom F & v = G . k holds
F . k = a * v ) implies Sum F = a * (Sum G) ) ; ::_thesis: verum
end;
theorem :: RLVECT_2:67
for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
proof
let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
let a be Element of R; ::_thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R; ::_thesis: for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
let F, G be FinSequence of V; ::_thesis: ( len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) implies Sum G = a * (Sum F) )
assume that
A1: len F = len G and
A2: for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ; ::_thesis: Sum G = a * (Sum F)
now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_Element_of_V_st_k_in_dom_G_&_v_=_F_._k_holds_
G_._k_=_a_*_v
let k be Element of NAT ; ::_thesis: for v being Element of V st k in dom G & v = F . k holds
G . k = a * v
let v be Element of V; ::_thesis: ( k in dom G & v = F . k implies G . k = a * v )
assume that
A3: k in dom G and
A4: v = F . k ; ::_thesis: G . k = a * v
A5: k in dom F by A1, A3, FINSEQ_3:29;
then v = F /. k by A4, PARTFUN1:def_6;
hence G . k = a * v by A2, A5; ::_thesis: verum
end;
hence Sum G = a * (Sum F) by A1, Th66; ::_thesis: verum
end;
theorem :: RLVECT_2:68
for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty right_complementable Abelian add-associative right_zeroed VectSpStr over R
for F, G, H being FinSequence of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ) holds
Sum H = (Sum F) - (Sum G)
proof
let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being non empty right_complementable Abelian add-associative right_zeroed VectSpStr over R
for F, G, H being FinSequence of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ) holds
Sum H = (Sum F) - (Sum G)
let V be non empty right_complementable Abelian add-associative right_zeroed VectSpStr over R; ::_thesis: for F, G, H being FinSequence of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ) holds
Sum H = (Sum F) - (Sum G)
let F, G, H be FinSequence of V; ::_thesis: ( len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ) implies Sum H = (Sum F) - (Sum G) )
assume that
A1: len F = len G and
A2: len F = len H and
A3: for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ; ::_thesis: Sum H = (Sum F) - (Sum G)
deffunc H1( Nat) -> Element of the carrier of V = - (G /. $1);
consider I being FinSequence such that
A4: len I = len G and
A5: for k being Nat st k in dom I holds
I . k = H1(k) from FINSEQ_1:sch_2();
A6: dom I = Seg (len G) by A4, FINSEQ_1:def_3;
then A7: for k being Element of NAT st k in Seg (len G) holds
I . k = H1(k) by A5;
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
A8: y in dom I and
A9: I . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A8;
x = - (G /. y) by A5, A8, A9;
then reconsider v = x as Element of V ;
v in V by RLVECT_1:1;
hence x in the carrier of V ; ::_thesis: verum
end;
then reconsider I = I as FinSequence of V by FINSEQ_1:def_4;
A10: Seg (len G) = dom G by FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_F_holds_
H_._k_=_(F_/._k)_+_(I_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom F implies H . k = (F /. k) + (I /. k) )
A11: dom F = dom G by A1, FINSEQ_3:29;
assume A12: k in dom F ; ::_thesis: H . k = (F /. k) + (I /. k)
then k in dom I by A1, A4, FINSEQ_3:29;
then A13: I . k = I /. k by PARTFUN1:def_6;
thus H . k = (F /. k) - (G /. k) by A3, A12
.= (F /. k) + (- (G /. k))
.= (F /. k) + (I /. k) by A5, A6, A10, A12, A13, A11 ; ::_thesis: verum
end;
then A14: Sum H = (Sum F) + (Sum I) by A1, A2, A4, Th2;
Sum I = - (Sum G) by A4, A7, A10, Th4;
hence Sum H = (Sum F) - (Sum G) by A14; ::_thesis: verum
end;
theorem :: RLVECT_2:69
for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R holds a * (Sum (<*> the carrier of V)) = 0. V
proof
let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R holds a * (Sum (<*> the carrier of V)) = 0. V
let a be Element of R; ::_thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R holds a * (Sum (<*> the carrier of V)) = 0. V
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R; ::_thesis: a * (Sum (<*> the carrier of V)) = 0. V
thus a * (Sum (<*> the carrier of V)) = a * (0. V) by RLVECT_1:43
.= 0. V by VECTSP_1:14 ; ::_thesis: verum
end;
theorem :: RLVECT_2:70
for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for v, u being Element of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)
proof
let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for v, u being Element of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)
let a be Element of R; ::_thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for v, u being Element of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R; ::_thesis: for v, u being Element of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)
let v, u be Element of V; ::_thesis: a * (Sum <*v,u*>) = (a * v) + (a * u)
thus a * (Sum <*v,u*>) = a * (v + u) by RLVECT_1:45
.= (a * v) + (a * u) by VECTSP_1:def_14 ; ::_thesis: verum
end;
theorem :: RLVECT_2:71
for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
proof
let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
let a be Element of R; ::_thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R; ::_thesis: for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
let v, u, w be Element of V; ::_thesis: a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
thus a * (Sum <*v,u,w*>) = a * ((v + u) + w) by RLVECT_1:46
.= (a * (v + u)) + (a * w) by VECTSP_1:def_14
.= ((a * v) + (a * u)) + (a * w) by VECTSP_1:def_14 ; ::_thesis: verum
end;