let i be Nat; :: thesis: for K being Field
for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1 st i in dom R holds
Sum (lmlt (Line (1. K,(len R)),i),R) = R /. i
let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1 st i in dom R holds
Sum (lmlt (Line (1. K,(len R)),i),R) = R /. i
let V1 be finite-dimensional VectSp of K; :: thesis: for R being FinSequence of V1 st i in dom R holds
Sum (lmlt (Line (1. K,(len R)),i),R) = R /. i
let R be FinSequence of V1; :: thesis: ( i in dom R implies Sum (lmlt (Line (1. K,(len R)),i),R) = R /. i )
assume A1:
i in dom R
; :: thesis: Sum (lmlt (Line (1. K,(len R)),i),R) = R /. i
set ONE = 1. K,(len R);
set L = Line (1. K,(len R)),i;
set M = lmlt (Line (1. K,(len R)),i),R;
A2:
( len (Line (1. K,(len R)),i) = width (1. K,(len R)) & width (1. K,(len R)) = len R & len (1. K,(len R)) = len R )
by FINSEQ_2:109, MATRIX_1:25;
then A3:
( dom (Line (1. K,(len R)),i) = dom R & dom R = dom (1. K,(len R)) )
by FINSEQ_3:31;
then A4:
dom (lmlt (Line (1. K,(len R)),i),R) = dom R
by MATRLIN:16;
then A5:
( 1 <= i & i <= len (lmlt (Line (1. K,(len R)),i),R) & len (lmlt (Line (1. K,(len R)),i),R) = len R )
by A1, FINSEQ_3:27, FINSEQ_3:31;
consider f being Function of NAT ,the carrier of V1 such that
A6:
Sum (lmlt (Line (1. K,(len R)),i),R) = f . (len (lmlt (Line (1. K,(len R)),i),R))
and
A7:
f . 0 = 0. V1
and
A8:
for j being Element of NAT
for v1 being Element of V1 st j < len (lmlt (Line (1. K,(len R)),i),R) & v1 = (lmlt (Line (1. K,(len R)),i),R) . (j + 1) holds
f . (j + 1) = (f . j) + v1
by RLVECT_1:def 13;
defpred S1[ Nat] means ( $1 < i implies f . $1 = 0. V1 );
A9:
S1[ 0 ]
by A7;
A10:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A11:
S1[
n]
;
:: thesis: S1[n + 1]
set n1 =
n + 1;
reconsider N =
n as
Element of
NAT by ORDINAL1:def 13;
assume A12:
n + 1
< i
;
:: thesis: f . (n + 1) = 0. V1
then
n + 1
< len (lmlt (Line (1. K,(len R)),i),R)
by A5, XXREAL_0:2;
then A13:
n < len (lmlt (Line (1. K,(len R)),i),R)
by NAT_1:13;
( 1
<= n + 1 &
n + 1
<= len R )
by A5, A12, NAT_1:11, XXREAL_0:2;
then A14:
(
n + 1
in Seg (len R) &
n + 1
in dom R )
by FINSEQ_3:27;
then A15:
(
(Line (1. K,(len R)),i) . (n + 1) = (1. K,(len R)) * i,
(n + 1) &
[i,(n + 1)] in Indices (1. K,(len R)) &
R . (n + 1) = R /. (n + 1) )
by A1, A2, A3, MATRIX_1:def 8, PARTFUN1:def 8, ZFMISC_1:106;
then
(Line (1. K,(len R)),i) . (n + 1) = 0. K
by A12, MATRIX_1:def 12;
then (lmlt (Line (1. K,(len R)),i),R) . (n + 1) =
(0. K) * (R /. (n + 1))
by A4, A14, A15, FUNCOP_1:28
.=
0. V1
by VECTSP_1:59
;
hence f . (n + 1) =
(f . N) + (0. V1)
by A13, A8
.=
0. V1
by A12, A11, NAT_1:13, RLVECT_1:def 7
;
:: thesis: verum
end;
A16:
for n being Nat holds S1[n]
from NAT_1:sch 2(A9, A10);
defpred S2[ Nat] means ( $1 <= len (lmlt (Line (1. K,(len R)),i),R) implies f . $1 = R /. i );
A17:
S2[i]
proof
assume A18:
i <= len (lmlt (Line (1. K,(len R)),i),R)
;
:: thesis: f . i = R /. i
reconsider i1 =
i - 1 as
Element of
NAT by A5, NAT_1:21;
i in Seg (len R)
by A5, A1;
then A19:
(
(Line (1. K,(len R)),i) . i = (1. K,(len R)) * i,
i &
[i,i] in Indices (1. K,(len R)) &
R . i = R /. i )
by A1, A2, A3, MATRIX_1:def 8, PARTFUN1:def 8, ZFMISC_1:106;
then
(Line (1. K,(len R)),i) . i = 1_ K
by MATRIX_1:def 12;
then A20:
(lmlt (Line (1. K,(len R)),i),R) . i =
(1_ K) * (R /. i)
by A1, A4, A19, FUNCOP_1:28
.=
R /. i
by VECTSP_1:def 26
;
i1 + 1
= i
;
then
(
i1 < len (lmlt (Line (1. K,(len R)),i),R) &
i1 < i )
by A18, NAT_1:13;
then
(
f . (i1 + 1) = (f . i1) + (R /. i) &
f . i1 = 0. V1 )
by A16, A8, A20;
hence
f . i = R /. i
by RLVECT_1:def 7;
:: thesis: verum
end;
A21:
for n being Nat st i <= n & S2[n] holds
S2[n + 1]
proof
let n be
Nat;
:: thesis: ( i <= n & S2[n] implies S2[n + 1] )
assume A22:
i <= n
;
:: thesis: ( not S2[n] or S2[n + 1] )
reconsider N =
n as
Element of
NAT by ORDINAL1:def 13;
assume A23:
S2[
n]
;
:: thesis: S2[n + 1]
set n1 =
n + 1;
assume A24:
n + 1
<= len (lmlt (Line (1. K,(len R)),i),R)
;
:: thesis: f . (n + 1) = R /. i
then A25:
n < len (lmlt (Line (1. K,(len R)),i),R)
by NAT_1:13;
A26:
( 1
<= n + 1 &
i < n + 1 )
by A22, NAT_1:11, NAT_1:13;
then A27:
(
n + 1
in Seg (len R) &
n + 1
in dom R )
by A5, A24, FINSEQ_3:27;
then A28:
(
(Line (1. K,(len R)),i) . (n + 1) = (1. K,(len R)) * i,
(n + 1) &
[i,(n + 1)] in Indices (1. K,(len R)) &
R . (n + 1) = R /. (n + 1) )
by A1, A2, A3, MATRIX_1:def 8, PARTFUN1:def 8, ZFMISC_1:106;
then
(Line (1. K,(len R)),i) . (n + 1) = 0. K
by A26, MATRIX_1:def 12;
then (lmlt (Line (1. K,(len R)),i),R) . (n + 1) =
(0. K) * (R /. (n + 1))
by A4, A27, A28, FUNCOP_1:28
.=
0. V1
by VECTSP_1:59
;
hence f . (n + 1) =
(f . N) + (0. V1)
by A25, A8
.=
R /. i
by A24, A23, NAT_1:13, RLVECT_1:def 7
;
:: thesis: verum
end;
for n being Nat st i <= n holds
S2[n]
from NAT_1:sch 8(A17, A21);
hence
Sum (lmlt (Line (1. K,(len R)),i),R) = R /. i
by A5, A6; :: thesis: verum