let K be Field; for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for d being FinSequence of K st len d = len b1 holds
d = (Sum (lmlt (d,b1))) |-- b1
let V1 be finite-dimensional VectSp of K; for b1 being OrdBasis of V1
for d being FinSequence of K st len d = len b1 holds
d = (Sum (lmlt (d,b1))) |-- b1
let b1 be OrdBasis of V1; for d being FinSequence of K st len d = len b1 holds
d = (Sum (lmlt (d,b1))) |-- b1
let d be FinSequence of K; ( len d = len b1 implies d = (Sum (lmlt (d,b1))) |-- b1 )
reconsider T = rng b1 as finite Subset of V1 by Def2;
defpred S1[ Element of V1, Element of K] means ( ( $1 in rng b1 implies for k being Nat st k in dom b1 & b1 /. k = $1 holds
$2 = d /. k ) & ( not $1 in rng b1 implies $2 = 0. K ) );
A1:
for v being Element of V1 ex u being Element of K st S1[v,u]
consider KL being Function of V1,K such that
A9:
for v being Element of V1 holds S1[v,KL . v]
from FUNCT_2:sch 3(A1);
then
KL in Funcs ( the carrier of V1, the carrier of K)
by FUNCT_2:def 2;
then reconsider KL1 = KL as Linear_Combination of V1 by A10, VECTSP_6:def 1;
assume A11:
len d = len b1
; d = (Sum (lmlt (d,b1))) |-- b1
now ex KL1 being Linear_Combination of V1 st
( ( for k being Nat st 1 <= k & k <= len d holds
d /. k = KL1 . (b1 /. k) ) & Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )take KL1 =
KL1;
( ( for k being Nat st 1 <= k & k <= len d holds
d /. k = KL1 . (b1 /. k) ) & Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )A12:
b1 is
one-to-one
by Def2;
thus A13:
for
k being
Nat st 1
<= k &
k <= len d holds
d /. k = KL1 . (b1 /. k)
( Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )
for
x being
object st
x in Carrier KL1 holds
x in rng b1
hence A16:
Carrier KL1 c= rng b1
;
Sum (lmlt (d,b1)) = Sum KL1A17:
dom d = dom b1
by A11, FINSEQ_3:29;
then A18:
dom (lmlt (d,b1)) = dom b1
by Th12;
then A19:
len (lmlt (d,b1)) =
len b1
by FINSEQ_3:29
.=
len (KL1 (#) b1)
by VECTSP_6:def 5
;
now for k being Nat st k in dom (lmlt (d,b1)) holds
(lmlt (d,b1)) . k = (KL1 (#) b1) . klet k be
Nat;
( k in dom (lmlt (d,b1)) implies (lmlt (d,b1)) . k = (KL1 (#) b1) . k )assume A20:
k in dom (lmlt (d,b1))
;
(lmlt (d,b1)) . k = (KL1 (#) b1) . kthen A21:
k in dom (KL1 (#) b1)
by A19, FINSEQ_3:29;
A22:
( 1
<= k &
k <= len d )
by A11, A18, A20, FINSEQ_3:25;
A23:
(
d /. k = d . k &
b1 /. k = b1 . k )
by A17, A18, A20, PARTFUN1:def 6;
thus (lmlt (d,b1)) . k =
the
lmult of
V1 . (
(d . k),
(b1 . k))
by A20, FUNCOP_1:22
.=
(d /. k) * (b1 /. k)
by A23, VECTSP_1:def 12
.=
(KL1 . (b1 /. k)) * (b1 /. k)
by A13, A22
.=
(KL1 (#) b1) . k
by A21, VECTSP_6:def 5
;
verum end; hence Sum (lmlt (d,b1)) =
Sum (KL1 (#) b1)
by A19, FINSEQ_2:9
.=
Sum KL1
by A16, A12, Th20
;
verum end;
hence
d = (Sum (lmlt (d,b1))) |-- b1
by A11, Def7; verum