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_1:def 3;
then A3:
dom (1. K,(len b1)) = dom b1
by FINSEQ_3:31;
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:27;
then A7:
len M = len b1
by MATRIX_1:24;
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 FINSEQ_1:def 18;
set Wm = Sum ((Width F) | m);
Width F = ((Width F) | m) ^ ((Width F) /^ m)
by RFINSEQ:21;
then A9:
Sum (Width F) = (Sum ((Width F) | m)) + (Sum ((Width F) /^ m))
by RVSUM_1:105;
then A10: (Sum (Width F)) -' (Sum ((Width F) | m)) =
(Sum (Width F)) - (Sum ((Width F) | m))
by NAT_1:11, XREAL_1:235
.=
Sum ((Width F) /^ m)
by A9
;
then A11:
len (((Sum (Width F)) -' (Sum ((Width F) | m))) |-> (0. K)) = Sum ((Width F) /^ m)
by FINSEQ_1:def 18;
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:27;
( 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:27, MATRIXJ1:def 4;
then
Width F = (((Width F) | (m -' 1)) ^ <*(width (F . m))*>) ^ ((Width F) /^ m)
by A5, A14, POLYNOM4:3;
then A15: Sum (Width F) =
(Sum (((Width F) | (m -' 1)) ^ <*(width (F . m))*>)) + (Sum ((Width F) /^ m))
by RVSUM_1:105
.=
((Sum ((Width F) | (m -' 1))) + (width (F . m))) + (Sum ((Width F) /^ m))
by RVSUM_1:104
;
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, FINSEQ_1:def 18;
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_1:24;
then A19:
len (B2 | (Sum ((Width F) | m))) = Sum ((Width F) | m)
by A2, A9, FINSEQ_1:80, 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:80, 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:7;
then
(B2 | (Sum ((Width F) | m))) | (Sum ((Width F) | (m -' 1))) = B2 | (Sum ((Width F) | (m -' 1)))
by RELAT_1:103;
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:21;
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:35;
A23:
B2 = (B2 | (Sum ((Width F) | m))) ^ (B2 /^ (Sum ((Width F) | m)))
by RFINSEQ:21;
then A24:
len B2 = (len (B2 | (Sum ((Width F) | m)))) + (len (B2 /^ (Sum ((Width F) | m))))
by FINSEQ_1:35;
(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_1:24, 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:58
.=
(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:59
.=
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 7
.=
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:58
.=
((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:59
.=
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 7
;
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
set B = block_diagonal F,(0. K);