let n be Nat; :: thesis: for K being Field
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 M being Matrix of len b1, len B2,K st M = Jordan_block L,n holds
for i being Nat st i in dom b1 holds
( ( i = len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
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 M being Matrix of len b1, len B2,K st M = Jordan_block L,n holds
for i being Nat st i in dom b1 holds
( ( i = len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 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 M being Matrix of len b1, len B2,K st M = Jordan_block L,n holds
for i being Nat st i in dom b1 holds
( ( i = len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 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 M being Matrix of len b1, len B2,K st M = Jordan_block L,n holds
for i being Nat st i in dom b1 holds
( ( i = len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 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 M being Matrix of len b1, len B2,K st M = Jordan_block L,n holds
for i being Nat st i in dom b1 holds
( ( i = len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
let B2 be FinSequence of V2; :: thesis: for M being Matrix of len b1, len B2,K st M = Jordan_block L,n holds
for i being Nat st i in dom b1 holds
( ( i = len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 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 = Jordan_block L,n implies for i being Nat st i in dom b1 holds
( ( i = len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) ) )
assume A1: M = Jordan_block L,n ; :: thesis: for i being Nat st i in dom b1 holds
( ( i = len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
let i be Nat; :: thesis: ( i in dom b1 implies ( ( i = len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) ) )
assume A2: i in dom b1 ; :: thesis: ( ( i = len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
set ONE = 1. K,(len b1);
set J = Jordan_block L,n;
len (1. K,(len b1)) = len b1 by MATRIX_1:def 3;
then A3: ( dom (1. K,(len b1)) = dom b1 & width (1. K,(len b1)) = len b1 & width (Jordan_block L,n) = n & len M = len b1 & len M = n & dom b1 = Seg (len b1) ) by A1, FINSEQ_1:def 3, FINSEQ_3:31, MATRIX_1:25, MATRIX_1:26;
then n <> 0 by A2;
then A4: width (Jordan_block L,n) = len B2 by A1, A3, MATRIX_1:20;
then A5: dom B2 = dom b1 by A3, FINSEQ_3:31;
(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 A2, MATRLIN2:19
.= Sum (lmlt (Line (LineVec2Mx (Line ((1. K,(len b1)) * M),i)),1),B2) by A2, A3, MATRLIN2:35
.= Sum (lmlt (Line (LineVec2Mx (Line M,i)),1),B2) by A3, MATRIXR2:68
.= Sum (lmlt (Line M,i),B2) by MATRIX15:25 ;
hence ( ( i = len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 implies (Mx2Tran M,b1,B2) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) ) by Th21, Th22, A1, A2, A3, A4, A5; :: thesis: verum