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