let m, i, n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 & Carrier L c= lines M )
and
A2:
i in Seg n
; :: thesis: (Sum L) . i = Sum (Col (FinS2MX (L (#) (MX2FinS M))),i)
set V = n -VectSp_over K;
set MX = MX2FinS M;
set LM = L (#) (MX2FinS M);
set FLM = FinS2MX (L (#) (MX2FinS M));
set C = Col (FinS2MX (L (#) (MX2FinS M))),i;
A3:
( Sum L = Sum (L (#) (MX2FinS M)) & len (L (#) (MX2FinS M)) = len M )
by A1, VECTSP_6:def 8, VECTSP_9:7;
then consider f being Function of NAT ,the carrier of (n -VectSp_over K) such that
A4:
Sum L = f . (len M)
and
A5:
f . 0 = 0. (n -VectSp_over K)
and
A6:
for j being Element of 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 RLVECT_1:def 13;
A7:
( len (L (#) (MX2FinS M)) = len (Col (FinS2MX (L (#) (MX2FinS M))),i) & len M = m )
by MATRIX_1:def 3, MATRIX_1:def 9;
then consider g being Function of NAT ,the carrier of K such that
A8:
Sum (Col (FinS2MX (L (#) (MX2FinS M))),i) = g . (len M)
and
A9:
g . 0 = 0. K
and
A10:
for j being Element of 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 A3, RLVECT_1:def 13;
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:
S1[ 0 ]
A13:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A14:
S1[
k]
;
:: thesis: S1[k + 1]
reconsider kk =
k as
Element of
NAT by ORDINAL1:def 13;
set k1 =
k + 1;
assume A15:
k + 1
<= len M
;
:: thesis: for v being Element of (n -VectSp_over K) st v = f . (k + 1) holds
v . i = g . (k + 1)
let v be
Vector of
(n -VectSp_over K);
:: thesis: ( v = f . (k + 1) implies v . i = g . (k + 1) )
assume A16:
v = f . (k + 1)
;
:: thesis: v . i = g . (k + 1)
1
<= k + 1
by NAT_1:14;
then A17:
k + 1
in Seg (len M)
by A15;
then A18:
(
k + 1
in dom (MX2FinS M) &
k + 1
in dom (FinS2MX (L (#) (MX2FinS M))) )
by A3, FINSEQ_1:def 3;
A19:
(
(MX2FinS M) . (k + 1) = Line M,
(k + 1) &
width (FinS2MX (L (#) (MX2FinS M))) = n )
by A3, A7, A17, Th1, FINSEQ_1:4, MATRIX_2:10;
then
(MX2FinS M) . (k + 1) in lines M
by A7, A17, Th103;
then reconsider MXK1 =
(MX2FinS M) . (k + 1) as
Element of
(n -VectSp_over K) ;
(MX2FinS M) /. (k + 1) = (MX2FinS M) . (k + 1)
by A18, PARTFUN1:def 8;
then A20:
(L (#) (MX2FinS M)) . (k + 1) = (L . MXK1) * MXK1
by A18, VECTSP_6:def 8;
then reconsider LMK1 =
(L (#) (MX2FinS M)) . (k + 1) as
Element of
(n -VectSp_over K) ;
reconsider N =
n as
Element of
NAT by ORDINAL1:def 13;
reconsider lmk1 =
LMK1,
mxk1 =
MXK1,
fk =
f . kk as
Element of
N -tuples_on the
carrier of
K by Th102;
dom lmk1 = Seg n
by FINSEQ_2:144;
then
(
lmk1 . i in rng lmk1 &
rng lmk1 c= the
carrier of
K )
by A2, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider lmk1i =
lmk1 . i as
Element of
K ;
LMK1 =
(L . MXK1) * mxk1
by A20, Th102
.=
Line (FinS2MX (L (#) (MX2FinS M))),
(k + 1)
by A17, A19, Th106
;
then
(
LMK1 . i = (FinS2MX (L (#) (MX2FinS M))) * (k + 1),
i &
(Col (FinS2MX (L (#) (MX2FinS M))),i) . (k + 1) = (FinS2MX (L (#) (MX2FinS M))) * (k + 1),
i &
k < len M )
by A2, A15, A18, A19, MATRIX_1:def 8, MATRIX_1:def 9, NAT_1:13;
then
(
g . (k + 1) = lmk1i + (g . kk) &
v = LMK1 + (f . kk) &
fk . i = g . kk &
LMK1 + (f . kk) = lmk1 + fk )
by A6, A10, A14, A16, Th102;
hence
v . i = g . (k + 1)
by A2, FVSUM_1:22;
:: thesis: verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A11, A13);
hence
(Sum L) . i = Sum (Col (FinS2MX (L (#) (MX2FinS M))),i)
by A4, A8; :: thesis: verum