let i, m, n be Nat; for K being Field
for L being Linear_Combination of n -VectSp_over K
for M being Matrix of m,n,K st M is without_repeated_line & Carrier L c= lines M & i in Seg n holds
(Sum L) . i = Sum (Col ((FinS2MX (L (#) (MX2FinS M))),i))
let K be Field; for L being Linear_Combination of n -VectSp_over K
for M being Matrix of m,n,K st M is without_repeated_line & Carrier L c= lines M & i in Seg n holds
(Sum L) . i = Sum (Col ((FinS2MX (L (#) (MX2FinS M))),i))
let L be Linear_Combination of n -VectSp_over K; for M being Matrix of m,n,K st M is without_repeated_line & Carrier L c= lines M & i in Seg n holds
(Sum L) . i = Sum (Col ((FinS2MX (L (#) (MX2FinS M))),i))
let M be Matrix of m,n,K; ( M is without_repeated_line & Carrier L c= lines M & i in Seg n implies (Sum L) . i = Sum (Col ((FinS2MX (L (#) (MX2FinS M))),i)) )
assume that
A1:
M is without_repeated_line
and
A2:
Carrier L c= lines M
and
A3:
i in Seg n
; (Sum L) . i = Sum (Col ((FinS2MX (L (#) (MX2FinS M))),i))
set MX = MX2FinS M;
set V = n -VectSp_over K;
set LM = L (#) (MX2FinS M);
A4:
len (L (#) (MX2FinS M)) = len M
by VECTSP_6:def 5;
set FLM = FinS2MX (L (#) (MX2FinS M));
set C = Col ((FinS2MX (L (#) (MX2FinS M))),i);
len (L (#) (MX2FinS M)) = len (Col ((FinS2MX (L (#) (MX2FinS M))),i))
by MATRIX_0:def 8;
then consider g being sequence of the carrier of K such that
A5:
Sum (Col ((FinS2MX (L (#) (MX2FinS M))),i)) = g . (len M)
and
A6:
g . 0 = 0. K
and
A7:
for j being Nat
for a being Element of K st j < len M & a = (Col ((FinS2MX (L (#) (MX2FinS M))),i)) . (j + 1) holds
g . (j + 1) = (g . j) + a
by A4, RLVECT_1:def 12;
Sum L = Sum (L (#) (MX2FinS M))
by A1, A2, VECTSP_9:3;
then consider f being sequence of the carrier of (n -VectSp_over K) such that
A8:
Sum L = f . (len M)
and
A9:
f . 0 = 0. (n -VectSp_over K)
and
A10:
for j being Nat
for v being Vector of (n -VectSp_over K) st j < len M & v = (L (#) (MX2FinS M)) . (j + 1) holds
f . (j + 1) = (f . j) + v
by A4, RLVECT_1:def 12;
defpred S1[ Nat] means ( $1 <= len M implies for v being Element of (n -VectSp_over K) st v = f . $1 holds
v . i = g . $1 );
A11:
len M = m
by MATRIX_0:def 2;
A12:
for k being Nat st S1[k] holds
S1[k + 1]
proof
reconsider N =
n as
Element of
NAT by ORDINAL1:def 12;
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A13:
S1[
k]
;
S1[k + 1]
set k1 =
k + 1;
reconsider kk =
k as
Element of
NAT by ORDINAL1:def 12;
assume A14:
k + 1
<= len M
;
for v being Element of (n -VectSp_over K) st v = f . (k + 1) holds
v . i = g . (k + 1)
then A15:
k < len M
by NAT_1:13;
A16:
width (FinS2MX (L (#) (MX2FinS M))) = n
by A4, A14, Th1;
1
<= k + 1
by NAT_1:14;
then A17:
k + 1
in Seg (len M)
by A14;
then A18:
k + 1
in dom (FinS2MX (L (#) (MX2FinS M)))
by A4, FINSEQ_1:def 3;
A19:
(MX2FinS M) . (k + 1) = Line (
M,
(k + 1))
by A11, A17, MATRIX_0:52;
then
(MX2FinS M) . (k + 1) in lines M
by A11, A17, Th103;
then reconsider MXK1 =
(MX2FinS M) . (k + 1) as
Element of
(n -VectSp_over K) ;
k + 1
in dom (MX2FinS M)
by A17, FINSEQ_1:def 3;
then
(MX2FinS M) /. (k + 1) = (MX2FinS M) . (k + 1)
by PARTFUN1:def 6;
then A20:
(L (#) (MX2FinS M)) . (k + 1) = (L . MXK1) * MXK1
by A18, VECTSP_6:def 5;
then reconsider LMK1 =
(L (#) (MX2FinS M)) . (k + 1) as
Element of
(n -VectSp_over K) ;
let v be
Vector of
(n -VectSp_over K);
( v = f . (k + 1) implies v . i = g . (k + 1) )
assume
v = f . (k + 1)
;
v . i = g . (k + 1)
then A21:
v = LMK1 + (f . kk)
by A10, A15;
reconsider lmk1 =
LMK1,
mxk1 =
MXK1,
fk =
f . kk as
Element of
N -tuples_on the
carrier of
K by Th102;
LMK1 =
(L . MXK1) * mxk1
by A20, Th102
.=
Line (
(FinS2MX (L (#) (MX2FinS M))),
(k + 1))
by A17, A19, Th106
;
then A22:
LMK1 . i = (FinS2MX (L (#) (MX2FinS M))) * (
(k + 1),
i)
by A3, A16, MATRIX_0:def 7;
dom lmk1 = Seg n
by FINSEQ_2:124;
then A23:
lmk1 . i in rng lmk1
by A3, FUNCT_1:def 3;
rng lmk1 c= the
carrier of
K
by FINSEQ_1:def 4;
then reconsider lmk1i =
lmk1 . i as
Element of
K by A23;
(Col ((FinS2MX (L (#) (MX2FinS M))),i)) . (k + 1) = (FinS2MX (L (#) (MX2FinS M))) * (
(k + 1),
i)
by A18, MATRIX_0:def 8;
then A24:
g . (k + 1) = lmk1i + (g . kk)
by A7, A22, A15;
A25:
LMK1 + (f . kk) = lmk1 + fk
by Th102;
fk . i = g . kk
by A13, A14, NAT_1:13;
hence
v . i = g . (k + 1)
by A3, A24, A21, A25, FVSUM_1:18;
verum
end;
A26:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(A26, A12);
hence
(Sum L) . i = Sum (Col ((FinS2MX (L (#) (MX2FinS M))),i))
by A8, A5; verum