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_0:24;
len (Line ((1. (K,(len R))),i)) = width (1. (K,(len R)))
by CARD_1:def 7;
then
dom (Line ((1. (K,(len R))),i)) = dom R
by A1, FINSEQ_3:29;
then A2:
dom (lmlt ((Line ((1. (K,(len R))),i)),R)) = dom R
by MATRLIN:12;
then A3:
len (lmlt ((Line ((1. (K,(len R))),i)),R)) = len R
by FINSEQ_3:29;
consider f being sequence of 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 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 12;
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:25;
len (1. (K,(len R))) = len R
by MATRIX_0:24;
then A9:
dom R = dom (1. (K,(len R)))
by FINSEQ_3:29;
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 12;
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_0:def 7, ZFMISC_1:87;
then A17:
(Line ((1. (K,(len R))),i)) . (n + 1) = 0. K
by A12, MATRIX_1:def 3;
A18:
n + 1
in dom R
by A2, A14, A16, FINSEQ_3:25;
then
R . (n + 1) = R /. (n + 1)
by PARTFUN1:def 6;
then (lmlt ((Line ((1. (K,(len R))),i)),R)) . (n + 1) =
(0. K) * (R /. (n + 1))
by A2, A18, A17, FUNCOP_1:22
.=
0. V1
by VECTSP_1:14
;
hence f . (n + 1) =
(f . N) + (0. V1)
by A6, A15
.=
R /. i
by A13, A14, NAT_1:13, RLVECT_1:def 4
;
verum
end;
A19:
i <= len (lmlt ((Line ((1. (K,(len R))),i)),R))
by A7, A2, FINSEQ_3:25;
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 12;
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_0:def 7, ZFMISC_1:87;
then A25:
(Line ((1. (K,(len R))),i)) . (n + 1) = 0. K
by A22, MATRIX_1:def 3;
A26:
n + 1
in dom R
by A24, FINSEQ_3:25;
then
R . (n + 1) = R /. (n + 1)
by PARTFUN1:def 6;
then (lmlt ((Line ((1. (K,(len R))),i)),R)) . (n + 1) =
(0. K) * (R /. (n + 1))
by A2, A26, A25, FUNCOP_1:22
.=
0. V1
by VECTSP_1:14
;
hence f . (n + 1) =
(f . N) + (0. V1)
by A6, A23
.=
0. V1
by A21, A22, NAT_1:13, RLVECT_1:def 4
;
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 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_0:def 7, ZFMISC_1:87;
then A30:
(Line ((1. (K,(len R))),i)) . i = 1_ K
by MATRIX_1:def 3;
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 6;
then (lmlt ((Line ((1. (K,(len R))),i)),R)) . i =
(1_ K) * (R /. i)
by A7, A2, A30, FUNCOP_1:22
.=
R /. i
by VECTSP_1:def 17
;
then
f . (i1 + 1) = (f . i1) + (R /. i)
by A6, A33;
hence
f . i = R /. i
by A32, RLVECT_1:def 4;
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