let X be RealNormSpace; for w being Point of X
for e being Real
for l being Linear_Combination of {w} st 0 < e holds
ex m being Linear_Combination of {w} st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )
let w be Point of X; for e being Real
for l being Linear_Combination of {w} st 0 < e holds
ex m being Linear_Combination of {w} st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )
let e be Real; for l being Linear_Combination of {w} st 0 < e holds
ex m being Linear_Combination of {w} st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )
let l be Linear_Combination of {w}; ( 0 < e implies ex m being Linear_Combination of {w} st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e ) )
assume A1:
0 < e
; ex m being Linear_Combination of {w} st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )
A2:
Carrier l c= {w}
by RLVECT_2:def 6;
per cases
( not w in Carrier l or w in Carrier l )
;
suppose A5:
w in Carrier l
;
ex m being Linear_Combination of {w} st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )then A6:
(
Carrier l = {w} &
l . w <> 0 )
by RLVECT_2:19, RLVECT_2:def 6, ZFMISC_1:31;
per cases
( w = 0. X or w <> 0. X )
;
suppose A11:
w <> 0. X
;
ex m being Linear_Combination of {w} st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )then A12:
||.w.|| <> 0
by NORMSP_0:def 5;
then consider q being
Element of
RAT such that A13:
(
q <> 0 &
|.((l . w) - q).| < e / ||.w.|| )
by A1, Th21;
set m =
(q / (l . w)) * l;
Carrier ((q / (l . w)) * l) = Carrier l
by A6, A13, RLVECT_2:42;
then reconsider m =
(q / (l . w)) * l as
Linear_Combination of
{w} by RLVECT_2:def 6;
take
m
;
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )thus
Carrier m = Carrier l
by A6, A13, RLVECT_2:42;
( rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )
for
y being
object st
y in rng m holds
y in RAT
hence
rng m c= RAT
;
||.((Sum l) - (Sum m)).|| < eA16:
Sum m =
(q / (l . w)) * (Sum l)
by RLVECT_3:2
.=
(q / (l . w)) * ((l . w) * w)
by RLVECT_2:32
.=
((q / (l . w)) * (l . w)) * w
by RLVECT_1:def 7
.=
q * w
by A5, RLVECT_2:19, XCMPLX_1:87
;
(Sum l) - (Sum m) =
((l . w) * w) - (Sum m)
by RLVECT_2:32
.=
((l . w) - q) * w
by A16, RLVECT_1:35
;
then A17:
||.((Sum l) - (Sum m)).|| = |.((l . w) - q).| * ||.w.||
by NORMSP_1:def 1;
|.((l . w) - q).| * ||.w.|| < (e / ||.w.||) * ||.w.||
by A12, A13, XREAL_1:68;
hence
||.((Sum l) - (Sum m)).|| < e
by A11, A17, NORMSP_0:def 5, XCMPLX_1:87;
verum end; end; end; end;