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)) ) )
set ONE = 1. K,(len b1);
set J = Jordan_block L,n;
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)) ) )
A2: len M = n by A1, MATRIX_1:25;
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;
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 A4: 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)) ) )
A5: len M = len b1 by MATRIX_1:26;
A6: (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, A3, A5, MATRIX_1:25, MATRLIN2:35
.= Sum (lmlt (Line (LineVec2Mx (Line M,i)),1),B2) by A5, MATRIXR2:68
.= Sum (lmlt (Line M,i),B2) by MATRIX15:25 ;
dom b1 = Seg (len b1) by FINSEQ_1:def 3;
then n <> 0 by A4, A5, A2;
then A7: ( width (Jordan_block L,n) = n & width (Jordan_block L,n) = len B2 ) by A1, A5, A2, MATRIX_1:20;
then dom B2 = dom b1 by A5, A2, FINSEQ_3:31;
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 A1, A4, A5, A2, A7, A6, Th21, Th22; :: thesis: verum