let n be Element of NAT ; for x0 being Element of (REAL-US n)
for B being Subset of (REAL-US n) st B = RN_Base n holds
ex l being Linear_Combination of B st x0 = Sum l
let x0 be Element of (REAL-US n); for B being Subset of (REAL-US n) st B = RN_Base n holds
ex l being Linear_Combination of B st x0 = Sum l
let B be Subset of (REAL-US n); ( B = RN_Base n implies ex l being Linear_Combination of B st x0 = Sum l )
reconsider x1 = x0 as Element of REAL n by REAL_NS1:def 6;
A1:
REAL n = the carrier of (REAL-US n)
by REAL_NS1:def 6;
assume A2:
B = RN_Base n
; ex l being Linear_Combination of B st x0 = Sum l
A3:
{ x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) ) } c= B
B c= { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) ) }
then A4:
B = { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) ) }
by A3, XBOOLE_0:def 10;
A5:
{ x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) & |(x1,x)| <> 0 ) } c= B
then reconsider B0 = { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) & |(x1,x)| <> 0 ) } as Subset of (REAL-US n) by XBOOLE_1:1;
defpred S1[ object , object ] means ( $1 in B0 implies ex i being Element of NAT st
( $2 = i & 1 <= i & i <= n & $1 = Base_FinSeq (n,i) ) );
A6:
for x being object st x in B0 holds
ex y being object st
( y in Seg n & S1[x,y] )
proof
let x be
object ;
( x in B0 implies ex y being object st
( y in Seg n & S1[x,y] ) )
assume
x in B0
;
ex y being object st
( y in Seg n & S1[x,y] )
then consider x2 being
Element of
REAL n such that A7:
x = x2
and A8:
ex
i being
Element of
NAT st
( 1
<= i &
i <= n &
x2 = Base_FinSeq (
n,
i) &
|(x1,x2)| <> 0 )
;
consider i0 being
Element of
NAT such that A9:
1
<= i0
and A10:
i0 <= n
and A11:
x2 = Base_FinSeq (
n,
i0)
and
|(x1,x2)| <> 0
by A8;
i0 in Seg n
by A9, A10, FINSEQ_1:1;
hence
ex
y being
object st
(
y in Seg n &
S1[
x,
y] )
by A7, A9, A10, A11;
verum
end;
consider f being Function of B0,(Seg n) such that
A12:
for x being object st x in B0 holds
S1[x,f . x]
from FUNCT_2:sch 1(A6);
defpred S2[ object , object ] means ( ( $1 in B0 implies for i being Element of NAT st 1 <= i & i <= n & $1 = Base_FinSeq (n,i) holds
$2 = |(x1,(Base_FinSeq (n,i)))| ) & ( not $1 in B0 implies $2 = 0 ) );
A13:
for x being object st x in the carrier of (REAL-US n) holds
ex y being object st
( y in REAL & S2[x,y] )
consider l2 being Function of the carrier of (REAL-US n),REAL such that
A16:
for x being object st x in the carrier of (REAL-US n) holds
S2[x,l2 . x]
from FUNCT_2:sch 1(A13);
A17:
l2 is Element of Funcs ( the carrier of (REAL-US n),REAL)
by FUNCT_2:8;
for v being Element of (REAL-US n) st not v in B0 holds
l2 . v = 0
by A16;
then reconsider l3 = l2 as Linear_Combination of REAL-US n by A2, A5, A17, RLVECT_2:def 3;
Carrier l3 c= B0
then reconsider l0 = l3 as Linear_Combination of B0 by RLVECT_2:def 6;
A18:
Carrier l0 c= B0
by RLVECT_2:def 6;
then
Carrier l0 c= B
by A5;
then reconsider l2 = l0 as Linear_Combination of B by RLVECT_2:def 6;
A19:
B0 c= Carrier l0
proof
let x be
object ;
TARSKI:def 3 ( not x in B0 or x in Carrier l0 )
assume A20:
x in B0
;
x in Carrier l0
then consider x6 being
Element of
REAL n such that A21:
x = x6
and A22:
ex
i being
Element of
NAT st
( 1
<= i &
i <= n &
x6 = Base_FinSeq (
n,
i) &
|(x1,x6)| <> 0 )
;
reconsider x66 =
x6 as
Element of
(REAL-US n) by REAL_NS1:def 6;
consider i8 being
Element of
NAT such that
1
<= i8
and
i8 <= n
and A23:
x6 = Base_FinSeq (
n,
i8)
and
|(x1,x6)| <> 0
by A22;
l0 . x66 = |(x1,(Base_FinSeq (n,i8)))|
by A16, A20, A21, A22, A23;
then
x in { v where v is Element of (REAL-US n) : l0 . v <> 0 }
by A21, A22, A23;
hence
x in Carrier l0
by RLVECT_2:def 4;
verum
end;
A24:
dom (Sgm (rng f)) = Seg (len (Sgm (rng f)))
by FINSEQ_1:def 3;
A25:
rng ((f ") * (Sgm (rng f))) c= rng (f ")
by RELAT_1:26;
A26:
dom (Sgm (rng f)) = Seg (len (Sgm (rng f)))
by FINSEQ_1:def 3;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
then A31:
f is one-to-one
by FUNCT_1:def 4;
A32:
( Seg n = {} implies B0 = {} )
A34:
for i3 being Element of NAT st i3 in dom (ProjFinSeq x1) & not i3 in rng (Sgm (rng f)) holds
(ProjFinSeq x1) . i3 = 0* n
proof
let i3 be
Element of
NAT ;
( i3 in dom (ProjFinSeq x1) & not i3 in rng (Sgm (rng f)) implies (ProjFinSeq x1) . i3 = 0* n )
assume that A35:
i3 in dom (ProjFinSeq x1)
and A36:
not
i3 in rng (Sgm (rng f))
;
(ProjFinSeq x1) . i3 = 0* n
A37:
i3 in Seg (len (ProjFinSeq x1))
by A35, FINSEQ_1:def 3;
then A38:
1
<= i3
by FINSEQ_1:1;
len (ProjFinSeq x1) = n
by Def12;
then A39:
i3 <= n
by A37, FINSEQ_1:1;
A40:
not
i3 in rng f
by A36, FINSEQ_1:def 13;
A41:
now not |(x1,(Base_FinSeq (n,i3)))| <> 0 assume
|(x1,(Base_FinSeq (n,i3)))| <> 0
;
contradictionthen A42:
Base_FinSeq (
n,
i3)
in B0
by A38, A39;
then consider i5 being
Element of
NAT such that A43:
f . (Base_FinSeq (n,i3)) = i5
and
1
<= i5
and
i5 <= n
and A44:
Base_FinSeq (
n,
i3)
= Base_FinSeq (
n,
i5)
by A12;
A45:
Base_FinSeq (
n,
i3)
in dom f
by A32, A42, FUNCT_2:def 1;
i3 = i5
by A38, A39, A44, Th24;
hence
contradiction
by A40, A43, A45, FUNCT_1:def 3;
verum end;
(ProjFinSeq x1) . i3 = |(x1,(Base_FinSeq (n,i3)))| * (Base_FinSeq (n,i3))
by A38, A39, Def12;
hence
(ProjFinSeq x1) . i3 = 0* n
by A41, EUCLID_4:3;
verum
end;
A46:
rng ((ProjFinSeq x1) * (Sgm (rng f))) c= REAL n
;
A47:
rng (Sgm (rng f)) = rng f
by FINSEQ_1:def 13;
A48:
dom f = B0
by A32, FUNCT_2:def 1;
then
rng (f ") = B0
by A31, FUNCT_1:33;
then A49:
rng ((f ") * (Sgm (rng f))) c= the carrier of (REAL-US n)
by A25, XBOOLE_1:1;
dom ((f ") * (Sgm (rng f))) =
(Sgm (rng f)) " (dom (f "))
by RELAT_1:147
.=
(Sgm (rng f)) " (rng f)
by A31, FUNCT_1:33
.=
dom (Sgm (rng f))
by A47, Th1
;
then
(f ") * (Sgm (rng f)) is FinSequence
by A26, FINSEQ_1:def 2;
then reconsider F0 = (f ") * (Sgm (rng f)) as FinSequence of the carrier of (REAL-US n) by A49, FINSEQ_1:def 4;
dom F0 =
(Sgm (rng f)) " (dom (f "))
by RELAT_1:147
.=
(Sgm (rng f)) " (rng f)
by A31, FUNCT_1:33
.=
dom (Sgm (rng f))
by A47, Th1
;
then A50:
dom F0 = Seg (len (Sgm (rng f)))
by FINSEQ_1:def 3;
A51: dom (ProjFinSeq x1) =
Seg (len (ProjFinSeq x1))
by FINSEQ_1:def 3
.=
Seg n
by Def12
;
then dom ((ProjFinSeq x1) * (Sgm (rng f))) =
(Sgm (rng f)) " (Seg n)
by RELAT_1:147
.=
dom (Sgm (rng f))
by A47, Th1
;
then
(ProjFinSeq x1) * (Sgm (rng f)) is FinSequence
by A24, FINSEQ_1:def 2;
then reconsider F2 = (ProjFinSeq x1) * (Sgm (rng f)) as FinSequence of the carrier of (REAL-US n) by A1, A46, FINSEQ_1:def 4;
dom F2 =
(Sgm (rng f)) " (Seg n)
by A51, RELAT_1:147
.=
dom (Sgm (rng f))
by A47, Th1
;
then A52:
dom F2 = Seg (len (Sgm (rng f)))
by FINSEQ_1:def 3;
then A53:
Seg (len F2) = Seg (len (Sgm (rng f)))
by FINSEQ_1:def 3;
A54:
len F2 = len (Sgm (rng f))
by A52, FINSEQ_1:def 3;
dom (f ") = rng f
by A31, FUNCT_1:33;
then rng F0 =
rng (f ")
by A47, RELAT_1:28
.=
dom f
by A31, FUNCT_1:33
;
then A55:
rng F0 = Carrier l0
by A48, A18, A19, XBOOLE_0:def 10;
A56:
for i being Nat st i in dom F2 holds
F2 . i = (l0 . (F0 /. i)) * (F0 /. i)
proof
let i be
Nat;
( i in dom F2 implies F2 . i = (l0 . (F0 /. i)) * (F0 /. i) )
A57:
Sgm (rng f) is
one-to-one
by FINSEQ_3:92;
assume
i in dom F2
;
F2 . i = (l0 . (F0 /. i)) * (F0 /. i)
then A58:
i in Seg (len F2)
by FINSEQ_1:def 3;
then A59:
i in dom (Sgm (rng f))
by A54, FINSEQ_1:def 3;
then
(Sgm (rng f)) . i in rng (Sgm (rng f))
by FUNCT_1:def 3;
then reconsider i2 =
(Sgm (rng f)) . i as
Element of
NAT ;
reconsider r =
Base_FinSeq (
n,
i2) as
Element of
(REAL-US n) by REAL_NS1:def 6;
i2 in rng (Sgm (rng f))
by A59, FUNCT_1:def 3;
then consider x2 being
object such that A60:
x2 in dom f
and A61:
f . x2 = i2
by A47, FUNCT_1:def 3;
dom f = B0
by A32, FUNCT_2:def 1;
then reconsider r2 =
x2 as
Element of
(REAL-US n) by A60;
A62:
ex
i22 being
Element of
NAT st
(
f . r2 = i22 & 1
<= i22 &
i22 <= n &
r2 = Base_FinSeq (
n,
i22) )
by A12, A60;
then consider i4 being
Element of
NAT such that A63:
f . r = i4
and
1
<= i4
and
i4 <= n
and A64:
r = Base_FinSeq (
n,
i4)
by A61;
A65:
dom f = B0
by A32, FUNCT_2:def 1;
F0 . i =
(f ") . ((Sgm (rng f)) . i)
by A59, FUNCT_1:13
.=
Base_FinSeq (
n,
i2)
by A31, A60, A61, A62, FUNCT_1:32
;
then
Base_FinSeq (
n,
i2)
in rng F0
by A50, A53, A58, FUNCT_1:def 3;
then
Base_FinSeq (
n,
i2)
in { v where v is Element of (REAL-US n) : l0 . v <> 0 }
by A55, RLVECT_2:def 4;
then A66:
ex
v0 being
Element of
(REAL-US n) st
(
Base_FinSeq (
n,
i2)
= v0 &
l0 . v0 <> 0 )
;
then
Base_FinSeq (
n,
i2)
in B0
by A16;
then A67:
(f ") . (f . (Base_FinSeq (n,i2))) = Base_FinSeq (
n,
i2)
by A31, A65, FUNCT_1:34;
then A68:
((f ") * (Sgm (rng f))) . i = Base_FinSeq (
n,
i2)
by A59, A61, A62, FUNCT_1:13;
A69:
i2 in rng f
by A47, A59, FUNCT_1:def 3;
then A70:
1
<= i2
by FINSEQ_1:1;
A71:
i2 <= n
by A69, FINSEQ_1:1;
then
i4 = i2
by A70, A64, Th24;
then A72:
((Sgm (rng f)) ") . (f . (Base_FinSeq (n,i2))) = i
by A59, A63, A57, FUNCT_1:32;
A73:
f . (Base_FinSeq (n,i2)) in rng (Sgm (rng f))
by A47, A60, A61, A62, FUNCT_1:def 3;
then A74:
(f ") . ((Sgm (rng f)) . (((Sgm (rng f)) ") . (f . (Base_FinSeq (n,i2))))) = Base_FinSeq (
n,
i2)
by A57, A67, FUNCT_1:35;
dom ((Sgm (rng f)) ") = rng (Sgm (rng f))
by A57, FUNCT_1:33;
then
((Sgm (rng f)) ") . (f . (Base_FinSeq (n,i2))) in rng ((Sgm (rng f)) ")
by A73, FUNCT_1:def 3;
then A75:
((Sgm (rng f)) ") . (f . (Base_FinSeq (n,i2))) in dom (Sgm (rng f))
by A57, FUNCT_1:33;
l0 . (F0 /. i) =
l0 . (((f ") * (Sgm (rng f))) . i)
by A50, A54, A58, PARTFUN1:def 6
.=
l0 . (Base_FinSeq (n,i2))
by A72, A75, A74, FUNCT_1:13
.=
|(x1,(Base_FinSeq (n,i2)))|
by A16, A70, A71, A66
;
then (l0 . (F0 /. i)) * (F0 /. i) =
|(x1,(Base_FinSeq (n,i2)))| * (Base_FinSeq (n,i2))
by A50, A54, A58, A68, PARTFUN1:def 6
.=
(ProjFinSeq x1) . ((Sgm (rng f)) . i)
by A70, A71, Def12
.=
((ProjFinSeq x1) * (Sgm (rng f))) . i
by A59, FUNCT_1:13
;
hence
F2 . i = (l0 . (F0 /. i)) * (F0 /. i)
;
verum
end;
A76:
Sgm (rng f) is one-to-one
by FINSEQ_3:92;
reconsider F3 = F2 as FinSequence of REAL n by REAL_NS1:def 6;
A77: x0 =
Sum (ProjFinSeq x1)
by Th30
.=
Sum F3
by A47, A51, A34, Th23, FINSEQ_3:92
.=
Sum F2
by Th33
;
len F2 = len F0
by A50, A53, FINSEQ_1:def 3;
then
x1 = Sum (l0 (#) F0)
by A77, A56, RLVECT_2:def 7;
then
x1 = Sum l2
by A31, A76, A55, RLVECT_2:def 8;
hence
ex l being Linear_Combination of B st x0 = Sum l
; verum