let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of 0. K,K
for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) & len b1 > 0 holds
for F being nilpotent Function of V1,V1 st F = Mx2Tran (M,b1,b1) holds
( ex i being Nat st
( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) )
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of 0. K,K
for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) & len b1 > 0 holds
for F being nilpotent Function of V1,V1 st F = Mx2Tran (M,b1,b1) holds
( ex i being Nat st
( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) )
let b1 be OrdBasis of V1; :: thesis: for J being FinSequence_of_Jordan_block of 0. K,K
for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) & len b1 > 0 holds
for F being nilpotent Function of V1,V1 st F = Mx2Tran (M,b1,b1) holds
( ex i being Nat st
( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) )
let J be FinSequence_of_Jordan_block of 0. K,K; :: thesis: for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) & len b1 > 0 holds
for F being nilpotent Function of V1,V1 st F = Mx2Tran (M,b1,b1) holds
( ex i being Nat st
( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) )
let M be Matrix of len b1, len b1,K; :: thesis: ( M = block_diagonal (J,(0. K)) & len b1 > 0 implies for F being nilpotent Function of V1,V1 st F = Mx2Tran (M,b1,b1) holds
( ex i being Nat st
( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) ) )
assume that
A1: M = block_diagonal (J,(0. K)) and
A2: len b1 > 0 ; :: thesis: for F being nilpotent Function of V1,V1 st F = Mx2Tran (M,b1,b1) holds
( ex i being Nat st
( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) )
A3: ( len M = len b1 & len M = Sum (Len J) ) by A1, MATRIX_0:def 2;
defpred S1[ Nat] means for i being Nat st i in dom J holds
len (J . i) <= $1;
set mm = min ((Len J),(len b1));
A4: dom J = dom (Len J) by MATRIXJ1:def 3;
now :: thesis: for i being Nat st i in dom J holds
len (J . i) <= Sum (Len J)
let i be Nat; :: thesis: ( i in dom J implies len (J . i) <= Sum (Len J) )
assume A5: i in dom J ; :: thesis: len (J . i) <= Sum (Len J)
len (J . i) = (Len J) . i by A4, A5, MATRIXJ1:def 3;
hence len (J . i) <= Sum (Len J) by A4, A5, POLYNOM3:4; :: thesis: verum
end;
then A6: ex k being Nat st S1[k] ;
consider MIN being Nat such that
A7: S1[MIN] and
A8: for m being Nat st S1[m] holds
MIN <= m from NAT_1:sch 5(A6);
 len b1 in Seg (len b1) by A2, FINSEQ_1:3;
then A9: min ((Len J),(len b1)) in dom (Len J) by A3, MATRIXJ1:def 1;
A10: ex i being Nat st
( i in dom J & len (J . i) = MIN )
proof
assume A11: for i being Nat st i in dom J holds
len (J . i) <> MIN ; :: thesis: contradiction
len (J . (min ((Len J),(len b1)))) <= MIN by A9, A4, A7;
then len (J . (min ((Len J),(len b1)))) < MIN by A9, A4, A11, XXREAL_0:1;
then reconsider M1 = MIN - 1 as Element of NAT by NAT_1:20;
now :: thesis: for i being Nat st i in dom J holds
len (J . i) <= M1
let i be Nat; :: thesis: ( i in dom J implies len (J . i) <= M1 )
assume A12: i in dom J ; :: thesis: len (J . i) <= M1
len (J . i) <= MIN by A7, A12;
then len (J . i) < M1 + 1 by A11, A12, XXREAL_0:1;
hence len (J . i) <= M1 by NAT_1:13; :: thesis: verum
end;
then M1 + 1 <= M1 by A8;
hence contradiction by NAT_1:13; :: thesis: verum
end;
A13: (Len J) | (len (Len J)) = Len J by FINSEQ_1:58;
let F be nilpotent Function of V1,V1; :: thesis: ( F = Mx2Tran (M,b1,b1) implies ( ex i being Nat st
( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) ) )
assume A14: F = Mx2Tran (M,b1,b1) ; :: thesis: ( ex i being Nat st
( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) )
consider i being Nat such that
A15: i in dom J and
A16: len (J . i) = MIN by A10;
A17: (Len J) . i = (Len J) /. i by A4, A15, PARTFUN1:def 6;
set S = Sum ((Len J) | (i -' 1));
defpred S2[ Nat] means ( $1 in Seg MIN & $1 <> MIN implies (F |^ $1) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) = b1 /. (((Sum ((Len J) | (i -' 1))) + $1) + 1) );
A18: len (J . i) = (Len J) . i by A4, A15, MATRIXJ1:def 3;
i <= len (Len J) by A4, A15, FINSEQ_3:25;
then Sum ((Len J) | i) <= Sum ((Len J) | (len (Len J))) by POLYNOM3:18;
then A19: ( dom b1 = Seg (len b1) & Seg (Sum ((Len J) | i)) c= Seg (Sum (Len J)) ) by A13, FINSEQ_1:5, FINSEQ_1:def 3;
1 <= i by A15, FINSEQ_3:25;
then i -' 1 = i - 1 by XREAL_1:233;
then A20: i = (i -' 1) + 1 ;
A21: for n being Nat st S2[n] holds
S2[n + 1]
proof
(Len J) | i = ((Len J) | (i -' 1)) ^ <*MIN*> by A4, A15, A16, A18, A20, FINSEQ_5:10;
then A22: Sum ((Len J) | i) = (Sum ((Len J) | (i -' 1))) + MIN by RVSUM_1:74;
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A23: S2[n] ; :: thesis: S2[n + 1]
A24: (Len J) | i = Len (J | i) by MATRIXJ1:17;
set n1 = n + 1;
assume that
A25: n + 1 in Seg MIN and
A26: n + 1 <> MIN ; :: thesis: (F |^ (n + 1)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) = b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1)
A27: n + 1 <= MIN by A25, FINSEQ_1:1;
then n + 1 < MIN by A26, XXREAL_0:1;
then A28: (Sum ((Len J) | (i -' 1))) + (n + 1) < Sum ((Len J) | i) by A22, XREAL_1:6;
( (Sum ((Len J) | (i -' 1))) + (n + 1) in Seg (Sum ((Len J) | i)) & min ((Len J),((Sum ((Len J) | (i -' 1))) + (n + 1))) = i ) by A4, A15, A16, A18, A17, A25, MATRIXJ1:10;
then A29: F . (b1 /. ((Sum ((Len J) | (i -' 1))) + (n + 1))) = ((0. K) * (b1 /. ((Sum ((Len J) | (i -' 1))) + (n + 1)))) + (b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1)) by A1, A3, A14, A19, A28, A24, Th24
.= (0. V1) + (b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1)) by VECTSP_1:14
.= b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1) by RLVECT_1:def 4 ;
A30: n < MIN by A27, NAT_1:13;
now :: thesis: (F |^ (n + 1)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) = b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1)
per cases ( n = 0 or n >= 1 ) by NAT_1:14;
suppose n = 0 ; :: thesis: (F |^ (n + 1)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) = b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1)
hence (F |^ (n + 1)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) = b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1) by A29, VECTSP11:19; :: thesis: verum
end;
suppose A31: n >= 1 ; :: thesis: (F |^ (n + 1)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) = b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1)
A32: dom (F |^ n) = the carrier of V1 by FUNCT_2:def 1;
thus (F |^ (n + 1)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) = ((F |^ 1) * (F |^ n)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) by VECTSP11:20
.= (F |^ 1) . ((F |^ n) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1))) by A32, FUNCT_1:13
.= b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1) by A23, A30, A29, A31, VECTSP11:19 ; :: thesis: verum
end;
end;
end;
hence (F |^ (n + 1)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) = b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1) ; :: thesis: verum
end;
A33: S2[ 0 ] ;
A34: for n being Nat holds S2[n] from NAT_1:sch 2(A33, A21);
 A35: deg F >= MIN
proof
set D = deg F;
rng b1 is Basis of V1 by MATRLIN:def 2;
then A36: rng b1 is linearly-independent Subset of V1 by VECTSP_7:def 3;
assume A37: deg F < MIN ; :: thesis: contradiction
then ( 1 <= 1 + (deg F) & (deg F) + 1 <= MIN ) by NAT_1:11, NAT_1:13;
then (deg F) + 1 in Seg MIN ;
then (Sum ((Len J) | (i -' 1))) + ((deg F) + 1) in Seg (Sum ((Len J) | i)) by A4, A15, A16, A18, A17, MATRIXJ1:10;
then A38: ( b1 /. (((Sum ((Len J) | (i -' 1))) + (deg F)) + 1) = b1 . (((Sum ((Len J) | (i -' 1))) + (deg F)) + 1) & b1 . (((Sum ((Len J) | (i -' 1))) + (deg F)) + 1) in rng b1 ) by A3, A19, FUNCT_1:def 3, PARTFUN1:def 6;
deg F <> 0
proof
assume deg F = 0 ; :: thesis: contradiction
then [#] V1 = {(0. V1)} by Th15;
then (Omega). V1 = (0). V1 by VECTSP_4:def 3;
then dim V1 = 0 by VECTSP_9:29;
hence contradiction by A2, MATRLIN2:21; :: thesis: verum
end;
then deg F >= 1 by NAT_1:14;
then deg F in Seg MIN by A37;
then b1 /. (((Sum ((Len J) | (i -' 1))) + (deg F)) + 1) = (F |^ (deg F)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) by A34, A37
.= (ZeroMap (V1,V1)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) by Def5
.= ( the carrier of V1 --> (0. V1)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) by GRCAT_1:def 7
.= 0. V1 ;
hence contradiction by A38, A36, VECTSP_7:2; :: thesis: verum
end;
F |^ MIN = ZeroMap (V1,V1) by A1, A14, A7, Th25;
then deg F <= MIN by Def5;
then deg F = MIN by A35, XXREAL_0:1;
hence ( ex i being Nat st
( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) ) by A7, A10; :: thesis: verum