let K be Field; :: thesis: for L being Element of K
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len B2,K st M = block_diagonal (J,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len J),i) holds
( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
let L be Element of K; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len B2,K st M = block_diagonal (J,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len J),i) holds
( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len B2,K st M = block_diagonal (J,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len J),i) holds
( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
let b1 be OrdBasis of V1; :: thesis: for B2 being FinSequence of V2
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len B2,K st M = block_diagonal (J,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len J),i) holds
( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
let B2 be FinSequence of V2; :: thesis: for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len B2,K st M = block_diagonal (J,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len J),i) holds
( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
let J be FinSequence_of_Jordan_block of L,K; :: thesis: for M being Matrix of len b1, len B2,K st M = block_diagonal (J,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len J),i) holds
( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
let M be Matrix of len b1, len B2,K; :: thesis: ( M = block_diagonal (J,(0. K)) implies for i, m being Nat st i in dom b1 & m = min ((Len J),i) holds
( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) ) )
assume A1: M = block_diagonal (J,(0. K)) ; :: thesis: for i, m being Nat st i in dom b1 & m = min ((Len J),i) holds
( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
A2: ( dom b1 = Seg (len b1) & len M = Sum (Len J) ) by A1, FINSEQ_1:def 3, MATRIXJ1:def 5;
let i, m be Nat; :: thesis: ( i in dom b1 & m = min ((Len J),i) implies ( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) ) )
assume that
A3: i in dom b1 and
A4: m = min ((Len J),i) ; :: thesis: ( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
set Sm = Sum (Len (J | m));
A5: 1 <= i by A3, FINSEQ_3:25;
A6: i <= len b1 by A3, FINSEQ_3:25;
then A7: len M = len b1 by A5, MATRIX_0:23;
then A8: m in dom (Len J) by A3, A4, A2, MATRIXJ1:def 1;
then A9: (Len J) . m = len (J . m) by MATRIXJ1:def 3;
set S = Sum (Len (J | (m -' 1)));
set iS = i -' (Sum (Len (J | (m -' 1))));
set BBB = (B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))));
A10: (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((J . m),(i -' (Sum (Len (J | (m -' 1))))))),((B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))))))) by A1, A3, A4, Th20;
A11: width M = Sum (Width J) by A1, MATRIXJ1:def 5;
A12: len ((B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))))) = width (J . m) by A1, A3, A4, Th20;
A13: (Len J) | m = Len (J | m) by MATRIXJ1:17;
then A14: i <= Sum (Len (J | m)) by A3, A4, A7, A2, MATRIXJ1:def 1;
A15: (Len J) | (m -' 1) = Len (J | (m -' 1)) by MATRIXJ1:17;
then Sum (Len (J | (m -' 1))) < i by A3, A4, A7, A2, MATRIXJ1:7;
then A16: i -' (Sum (Len (J | (m -' 1)))) = i - (Sum (Len (J | (m -' 1)))) by XREAL_1:233;
A17: m -' 1 = m - 1 by A3, A4, A7, A2, MATRIXJ1:7;
then (Len J) | ((m -' 1) + 1) = (Len (J | (m -' 1))) ^ <*((Len J) . m)*> by A15, A8, FINSEQ_5:10;
then A18: Sum (Len (J | m)) = (Sum (Len (J | (m -' 1)))) + (len (J . m)) by A13, A17, A9, RVSUM_1:74;
then (Sum (Len (J | (m -' 1)))) + (i -' (Sum (Len (J | (m -' 1))))) <= (Sum (Len (J | (m -' 1)))) + (len (J . m)) by A3, A4, A13, A7, A2, A16, MATRIXJ1:def 1;
then A19: i -' (Sum (Len (J | (m -' 1)))) <= len (J . m) by XREAL_1:6;
dom (Len J) = dom J by MATRIXJ1:def 3;
then consider n being Nat such that
A20: J . m = Jordan_block (L,n) by A8, Def3;
( m in NAT & m <= len (Len J) ) by A8, FINSEQ_3:25;
then Sum (Len (J | m)) <= Sum ((Len J) | (len (Len J))) by A13, POLYNOM3:18;
then A21: Sum (Len (J | m)) <= Sum (Len J) by FINSEQ_1:58;
A22: Width J = Len J by MATRIXJ1:46;
then A23: (Len J) . m = width (J . m) by A8, MATRIXJ1:def 4;
width M = len B2 by A5, A6, MATRIX_0:23;
then A24: len (B2 | (Sum (Len (J | m)))) = Sum (Len (J | m)) by A22, A11, A21, FINSEQ_1:59;
then A25: i in dom (B2 | (Sum (Len (J | m)))) by A5, A14, FINSEQ_3:25;
A26: len (J . m) = n by A20, MATRIX_0:24;
i -' (Sum (Len (J | (m -' 1)))) <> 0 by A3, A4, A15, A7, A2, A16, MATRIXJ1:7;
then 1 <= i -' (Sum (Len (J | (m -' 1)))) by NAT_1:14;
then A27: i -' (Sum (Len (J | (m -' 1)))) in dom ((B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))))) by A12, A9, A23, A19, FINSEQ_3:25;
then A28: ((B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))))) /. (i -' (Sum (Len (J | (m -' 1))))) = (B2 | (Sum (Width (J | m)))) /. ((Sum (Width (J | (m -' 1)))) + (i -' (Sum (Len (J | (m -' 1)))))) by FINSEQ_5:27
.= (B2 | (Sum (Width (J | m)))) /. ((Sum (Len (J | (m -' 1)))) + (i -' (Sum (Len (J | (m -' 1)))))) by MATRIXJ1:46
.= (B2 | (Sum ((Len J) | m))) /. i by A22, A16, MATRIXJ1:21
.= B2 /. i by A13, A25, FINSEQ_4:70 ;
hence ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) by A10, A12, A9, A16, A23, A18, A27, A20, A26, Th21; :: thesis: ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) )
assume A29: i <> Sum (Len (J | m)) ; :: thesis: (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1))
then i < Sum (Len (J | m)) by A14, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= Sum (Len (J | m)) ) by NAT_1:11, NAT_1:13;
then A30: i + 1 in dom (B2 | (Sum (Len (J | m)))) by A24, FINSEQ_3:25;
A31: i -' (Sum (Len (J | (m -' 1)))) <> len (J . m) by A16, A18, A29;
then i -' (Sum (Len (J | (m -' 1)))) < len (J . m) by A19, XXREAL_0:1;
then ( 1 <= (i -' (Sum (Len (J | (m -' 1))))) + 1 & (i -' (Sum (Len (J | (m -' 1))))) + 1 <= len (J . m) ) by NAT_1:11, NAT_1:13;
then (i -' (Sum (Len (J | (m -' 1))))) + 1 in dom ((B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))))) by A12, A9, A23, FINSEQ_3:25;
then ((B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))))) /. ((i -' (Sum (Len (J | (m -' 1))))) + 1) = (B2 | (Sum (Width (J | m)))) /. ((Sum (Width (J | (m -' 1)))) + ((i -' (Sum (Len (J | (m -' 1))))) + 1)) by FINSEQ_5:27
.= (B2 | (Sum (Width (J | m)))) /. ((Sum ((Len J) | (m -' 1))) + ((i -' (Sum (Len (J | (m -' 1))))) + 1)) by A22, MATRIXJ1:21
.= (B2 | (Sum ((Len J) | m))) /. (i + 1) by A15, A22, A16, MATRIXJ1:21
.= B2 /. (i + 1) by A13, A30, FINSEQ_4:70 ;
hence (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) by A10, A12, A9, A23, A27, A20, A26, A28, A31, Th22; :: thesis: verum