let K be Field; for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K
for F being FinSequence_of_Matrix of K st M = block_diagonal (F,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len F),i) holds
( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
let V1, V2 be finite-dimensional VectSp of K; for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K
for F being FinSequence_of_Matrix of K st M = block_diagonal (F,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len F),i) holds
( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
let b1 be OrdBasis of V1; for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K
for F being FinSequence_of_Matrix of K st M = block_diagonal (F,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len F),i) holds
( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
let B2 be FinSequence of V2; for M being Matrix of len b1, len B2,K
for F being FinSequence_of_Matrix of K st M = block_diagonal (F,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len F),i) holds
( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
set ONE = 1. (K,(len b1));
let M be Matrix of len b1, len B2,K; for F being FinSequence_of_Matrix of K st M = block_diagonal (F,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len F),i) holds
( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
let F be FinSequence_of_Matrix of K; ( M = block_diagonal (F,(0. K)) implies for i, m being Nat st i in dom b1 & m = min ((Len F),i) holds
( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) ) )
assume A1:
M = block_diagonal (F,(0. K))
; for i, m being Nat st i in dom b1 & m = min ((Len F),i) holds
( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
A2:
width M = Sum (Width F)
by A1, MATRIXJ1:def 5;
len (1. (K,(len b1))) = len b1
by MATRIX_0:def 2;
then A3:
dom (1. (K,(len b1))) = dom b1
by FINSEQ_3:29;
set L = Len F;
set W = Width F;
let i, m be Nat; ( i in dom b1 & m = min ((Len F),i) implies ( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) ) )
assume that
A4:
i in dom b1
and
A5:
m = min ((Len F),i)
; ( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
A6:
( 1 <= i & i <= len b1 )
by A4, FINSEQ_3:25;
then A7:
len M = len b1
by MATRIX_0:23;
set Fm = F . m;
set Wm1 = Sum ((Width F) | (m -' 1));
A8:
( len ((Sum ((Width F) | (m -' 1))) |-> (0. K)) = Sum ((Width F) | (m -' 1)) & len (Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))) = width (F . m) )
by CARD_1:def 7;
set Wm = Sum ((Width F) | m);
Width F = ((Width F) | m) ^ ((Width F) /^ m)
by RFINSEQ:8;
then A9:
Sum (Width F) = (Sum ((Width F) | m)) + (Sum ((Width F) /^ m))
by RVSUM_1:75;
then A10: (Sum (Width F)) -' (Sum ((Width F) | m)) =
(Sum (Width F)) - (Sum ((Width F) | m))
by NAT_1:11, XREAL_1:233
.=
Sum ((Width F) /^ m)
by A9
;
then A11:
len (((Sum (Width F)) -' (Sum ((Width F) | m))) |-> (0. K)) = Sum ((Width F) /^ m)
by CARD_1:def 7;
A12:
( dom b1 = Seg (len b1) & len M = Sum (Len F) )
by A1, FINSEQ_1:def 3, MATRIXJ1:def 5;
then A13:
m in dom (Len F)
by A4, A5, A7, MATRIXJ1:def 1;
then A14:
1 <= m
by FINSEQ_3:25;
reconsider wF = width (F . m) as Element of NAT by ORDINAL1:def 12;
( dom (Len F) = dom F & dom (Width F) = dom F )
by MATRIXJ1:def 3, MATRIXJ1:def 4;
then
( m <= len (Width F) & (Width F) . m = width (F . m) )
by A13, FINSEQ_3:25, MATRIXJ1:def 4;
then
Width F = (((Width F) | (m -' 1)) ^ <*(width (F . m))*>) ^ ((Width F) /^ m)
by A5, A14, POLYNOM4:1;
then A15: Sum (Width F) =
(Sum (((Width F) | (m -' 1)) ^ <*wF*>)) + (Sum ((Width F) /^ m))
by RVSUM_1:75
.=
((Sum ((Width F) | (m -' 1))) + (width (F . m))) + (Sum ((Width F) /^ m))
by RVSUM_1:74
;
then A16:
len (((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))) = Sum ((Width F) | m)
by A9, CARD_1:def 7;
set B2W = B2 | (Sum ((Width F) | m));
A17: (B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1))) =
(B2 | (Sum (Width (F | m)))) /^ (Sum ((Width F) | (m -' 1)))
by MATRIXJ1:21
.=
(B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))
by MATRIXJ1:21
;
A18:
width M = len B2
by A6, MATRIX_0:23;
then A19:
len (B2 | (Sum ((Width F) | m))) = Sum ((Width F) | m)
by A2, A9, FINSEQ_1:59, NAT_1:11;
Sum (Width F) = (Sum ((Width F) | (m -' 1))) + ((width (F . m)) + (Sum ((Width F) /^ m)))
by A15;
then A20:
len (B2 | (Sum ((Width F) | (m -' 1)))) = Sum ((Width F) | (m -' 1))
by A2, A18, FINSEQ_1:59, NAT_1:11;
Sum ((Width F) | m) >= Sum ((Width F) | (m -' 1))
by A9, A15, NAT_1:11;
then
Seg (Sum ((Width F) | (m -' 1))) c= Seg (Sum ((Width F) | m))
by FINSEQ_1:5;
then
(B2 | (Sum ((Width F) | m))) | (Sum ((Width F) | (m -' 1))) = B2 | (Sum ((Width F) | (m -' 1)))
by RELAT_1:74;
then A21:
B2 | (Sum ((Width F) | m)) = (B2 | (Sum ((Width F) | (m -' 1)))) ^ ((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1))))
by RFINSEQ:8;
then A22:
len (B2 | (Sum ((Width F) | m))) = (len (B2 | (Sum ((Width F) | (m -' 1))))) + (len ((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1)))))
by FINSEQ_1:22;
A23:
B2 = (B2 | (Sum ((Width F) | m))) ^ (B2 /^ (Sum ((Width F) | m)))
by RFINSEQ:8;
then A24:
len B2 = (len (B2 | (Sum ((Width F) | m)))) + (len (B2 /^ (Sum ((Width F) | m))))
by FINSEQ_1:22;
(Mx2Tran (M,b1,B2)) . (b1 /. i) =
Sum (lmlt ((Line (((LineVec2Mx ((b1 /. i) |-- b1)) * M),1)),B2))
by MATRLIN2:def 3
.=
Sum (lmlt ((Line (((LineVec2Mx (Line ((1. (K,(len b1))),i))) * M),1)),B2))
by A4, MATRLIN2:19
.=
Sum (lmlt ((Line ((LineVec2Mx (Line (((1. (K,(len b1))) * M),i))),1)),B2))
by A4, A6, A3, A7, MATRIX_0:23, MATRLIN2:35
.=
Sum (lmlt ((Line ((LineVec2Mx (Line (M,i))),1)),B2))
by A7, MATRIXR2:68
.=
Sum (lmlt ((Line (M,i)),B2))
by MATRIX15:25
.=
Sum (lmlt (((((Sum (Width (F | (m -' 1)))) |-> (0. K)) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))) ^ (((Sum (Width F)) -' (Sum (Width (F | m)))) |-> (0. K))),B2))
by A1, A4, A5, A7, A12, MATRIXJ1:37
.=
Sum (lmlt (((((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))) ^ (((Sum (Width F)) -' (Sum (Width (F | m)))) |-> (0. K))),B2))
by MATRIXJ1:21
.=
Sum (lmlt (((((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))) ^ (((Sum (Width F)) -' (Sum ((Width F) | m))) |-> (0. K))),B2))
by MATRIXJ1:21
.=
Sum ((lmlt ((((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))),(B2 | (Sum ((Width F) | m))))) ^ (lmlt ((((Sum (Width F)) -' (Sum ((Width F) | m))) |-> (0. K)),(B2 /^ (Sum ((Width F) | m))))))
by A2, A18, A9, A23, A24, A19, A11, A16, MATRLIN2:9
.=
(Sum (lmlt ((((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))),(B2 | (Sum ((Width F) | m)))))) + (Sum (lmlt ((((Sum (Width F)) -' (Sum ((Width F) | m))) |-> (0. K)),(B2 /^ (Sum ((Width F) | m))))))
by RLVECT_1:41
.=
(Sum (lmlt ((((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))),(B2 | (Sum ((Width F) | m)))))) + ((0. K) * (Sum (B2 /^ (Sum ((Width F) | m)))))
by A2, A18, A9, A10, A24, A19, MATRLIN2:11
.=
(Sum (lmlt ((((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))),(B2 | (Sum ((Width F) | m)))))) + (0. V2)
by VECTSP_1:14
.=
Sum (lmlt ((((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))),(B2 | (Sum ((Width F) | m)))))
by RLVECT_1:def 4
.=
Sum ((lmlt (((Sum ((Width F) | (m -' 1))) |-> (0. K)),(B2 | (Sum ((Width F) | (m -' 1)))))) ^ (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1)))))))
by A9, A15, A19, A21, A22, A20, A8, MATRLIN2:9
.=
(Sum (lmlt (((Sum ((Width F) | (m -' 1))) |-> (0. K)),(B2 | (Sum ((Width F) | (m -' 1))))))) + (Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1)))))))
by RLVECT_1:41
.=
((0. K) * (Sum (B2 | (Sum ((Width F) | (m -' 1)))))) + (Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1)))))))
by A20, MATRLIN2:11
.=
(0. V2) + (Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1)))))))
by VECTSP_1:14
.=
Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1))))))
by RLVECT_1:def 4
;
hence
( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
by A9, A15, A19, A22, A20, A17; verum