let n be Nat; :: thesis: for K being Field
for L being Element of K
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len b1,K st M = block_diagonal J,(0. K) & len b1 <> 0 holds
( ((Mx2Tran M,b1,b1) |^ n) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) & Sum (Len (J | (min (Len J),(len b1)))) in dom b1 )
let K be Field; :: thesis: for L being Element of K
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len b1,K st M = block_diagonal J,(0. K) & len b1 <> 0 holds
( ((Mx2Tran M,b1,b1) |^ n) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) & Sum (Len (J | (min (Len J),(len b1)))) in dom b1 )
let L be Element of K; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len b1,K st M = block_diagonal J,(0. K) & len b1 <> 0 holds
( ((Mx2Tran M,b1,b1) |^ n) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) & Sum (Len (J | (min (Len J),(len b1)))) in dom b1 )
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len b1,K st M = block_diagonal J,(0. K) & len b1 <> 0 holds
( ((Mx2Tran M,b1,b1) |^ n) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) & Sum (Len (J | (min (Len J),(len b1)))) in dom b1 )
let b1 be OrdBasis of V1; :: thesis: for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len b1,K st M = block_diagonal J,(0. K) & len b1 <> 0 holds
( ((Mx2Tran M,b1,b1) |^ n) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) & Sum (Len (J | (min (Len J),(len b1)))) in dom b1 )
let J be FinSequence_of_Jordan_block of L,K; :: thesis: for M being Matrix of len b1, len b1,K st M = block_diagonal J,(0. K) & len b1 <> 0 holds
( ((Mx2Tran M,b1,b1) |^ n) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) & Sum (Len (J | (min (Len J),(len b1)))) in dom b1 )
let M be Matrix of len b1, len b1,K; :: thesis: ( M = block_diagonal J,(0. K) & len b1 <> 0 implies ( ((Mx2Tran M,b1,b1) |^ n) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) & Sum (Len (J | (min (Len J),(len b1)))) in dom b1 ) )
assume A1:
M = block_diagonal J,(0. K)
; :: thesis: ( not len b1 <> 0 or ( ((Mx2Tran M,b1,b1) |^ n) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) & Sum (Len (J | (min (Len J),(len b1)))) in dom b1 ) )
set MT = Mx2Tran M,b1,b1;
A2:
( len b1 = len M & len M = Sum (Len J) )
by A1, MATRIX_1:25;
set B = len b1;
set m = min (Len J),(len b1);
set S = Sum (Len (J | (min (Len J),(len b1))));
assume
len b1 <> 0
; :: thesis: ( ((Mx2Tran M,b1,b1) |^ n) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) & Sum (Len (J | (min (Len J),(len b1)))) in dom b1 )
then A3:
( len b1 in Seg (len b1) & Seg (len b1) = dom b1 )
by FINSEQ_1:5, FINSEQ_1:def 3;
then A4:
( len b1 <= Sum ((Len J) | (min (Len J),(len b1))) & Sum ((Len J) | (min (Len J),(len b1))) = Sum (Len (J | (min (Len J),(len b1)))) & min (Len J),(len b1) in dom (Len J) )
by A2, MATRIXJ1:17, MATRIXJ1:def 1;
then
min (Len J),(len b1) <= len (Len J)
by FINSEQ_3:27;
then A5:
( Sum ((Len J) | (min (Len J),(len b1))) <= Sum ((Len J) | (len (Len J))) & (Len J) | (len (Len J)) = Len J )
by FINSEQ_1:79, POLYNOM3:18;
then
len b1 = Sum (Len (J | (min (Len J),(len b1))))
by A2, A4, XXREAL_0:1;
then A6:
(Mx2Tran M,b1,b1) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = L * (b1 /. (Sum (Len (J | (min (Len J),(len b1))))))
by A1, A3, Th24;
defpred S1[ Nat] means ((Mx2Tran M,b1,b1) |^ $1) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,$1) * (b1 /. (Sum (Len (J | (min (Len J),(len b1))))));
A7:
S1[ 0 ]
A8:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A9:
S1[
n]
;
:: thesis: S1[n + 1]
A10:
dom ((Mx2Tran M,b1,b1) |^ n) = the
carrier of
V1
by FUNCT_2:def 1;
A11:
n in NAT
by ORDINAL1:def 13;
thus ((Mx2Tran M,b1,b1) |^ (n + 1)) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) =
(((Mx2Tran M,b1,b1) |^ 1) * ((Mx2Tran M,b1,b1) |^ n)) . (b1 /. (Sum (Len (J | (min (Len J),(len b1))))))
by VECTSP11:20
.=
((Mx2Tran M,b1,b1) * ((Mx2Tran M,b1,b1) |^ n)) . (b1 /. (Sum (Len (J | (min (Len J),(len b1))))))
by VECTSP11:19
.=
(Mx2Tran M,b1,b1) . (((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))))
by A9, A10, FUNCT_1:23
.=
((power K) . L,n) * (L * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))))
by A6, MOD_2:def 5
.=
(((power K) . L,n) * L) * (b1 /. (Sum (Len (J | (min (Len J),(len b1))))))
by VECTSP_1:def 26
.=
((power K) . L,(n + 1)) * (b1 /. (Sum (Len (J | (min (Len J),(len b1))))))
by A11, GROUP_1:def 8
;
:: thesis: verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A7, A8);
hence
( ((Mx2Tran M,b1,b1) |^ n) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) & Sum (Len (J | (min (Len J),(len b1)))) in dom b1 )
by A3, A5, A2, A4, XXREAL_0:1; :: thesis: verum