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) holds
( Mx2Tran M,b1,b1 is nilpotent iff ( len b1 = 0 or L = 0. K ) )
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) holds
( Mx2Tran M,b1,b1 is nilpotent iff ( len b1 = 0 or L = 0. K ) )
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) holds
( Mx2Tran M,b1,b1 is nilpotent iff ( len b1 = 0 or L = 0. K ) )
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) holds
( Mx2Tran M,b1,b1 is nilpotent iff ( len b1 = 0 or L = 0. K ) )
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) holds
( Mx2Tran M,b1,b1 is nilpotent iff ( len b1 = 0 or L = 0. K ) )
let M be Matrix of len b1, len b1,K; :: thesis: ( M = block_diagonal J,(0. K) implies ( Mx2Tran M,b1,b1 is nilpotent iff ( len b1 = 0 or L = 0. K ) ) )
assume A1: M = block_diagonal J,(0. K) ; :: thesis: ( Mx2Tran M,b1,b1 is nilpotent iff ( len b1 = 0 or L = 0. K ) )
set MT = Mx2Tran M,b1,b1;
thus ( not Mx2Tran M,b1,b1 is nilpotent or len b1 = 0 or L = 0. K ) :: thesis: ( ( len b1 = 0 or L = 0. K ) implies Mx2Tran M,b1,b1 is nilpotent )

proof

assume Mx2Tran M,b1,b1 is nilpotent ; :: thesis: ( len b1 = 0 or L = 0. K )
then reconsider MT = Mx2Tran M,b1,b1 as nilpotent linear-transformation of V1,V1 ;
set B = len b1;
set m = min (Len J),(len b1);
set S = Sum (Len (J | (min (Len J),(len b1))));
assume A2: len b1 <> 0 ; :: thesis: L = 0. K
then A3: ((power K) . L,(deg MT)) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = (MT |^ (deg MT)) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) by A1, Lm3
.= (ZeroMap V1,V1) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) by Def5
.= (the carrier of V1 --> (0. V1)) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) by GRCAT_1:def 12
.= 0. V1 by FUNCOP_1:13
.= (0. K) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) by VECTSP_1:59 ;
( rng b1 is Basis of V1 & Sum (Len (J | (min (Len J),(len b1)))) in dom b1 ) by A1, A2, Lm3, MATRLIN:def 4;
then ( b1 . (Sum (Len (J | (min (Len J),(len b1))))) in rng b1 & b1 /. (Sum (Len (J | (min (Len J),(len b1))))) = b1 . (Sum (Len (J | (min (Len J),(len b1))))) & rng b1 is linearly-independent Subset of V1 ) by FUNCT_1:def 5, PARTFUN1:def 8, VECTSP_7:def 3;
then b1 /. (Sum (Len (J | (min (Len J),(len b1))))) <> 0. V1 by VECTSP_7:3;
then 0. K = (power K) . L,(deg MT) by A3, VECTSP10:5
.= Product ((deg MT) |-> L) by MATRIXJ1:5 ;
then consider k being Element of NAT such that
A4: ( k in dom ((deg MT) |-> L) & ((deg MT) |-> L) . k = 0. K ) by FVSUM_1:107;
dom ((deg MT) |-> L) = Seg (deg MT) by FINSEQ_2:144;
hence L = 0. K by A4, FINSEQ_2:71; :: thesis: verum

end;

assume A5: ( len b1 = 0 or L = 0. K ) ; :: thesis: Mx2Tran M,b1,b1 is nilpotent

per cases ( len b1 = 0 or L = 0. K ) by A5;

suppose len b1 = 0 ; :: thesis: Mx2Tran M,b1,b1 is nilpotent

then dim V1 = 0 by MATRLIN2:21;
then (Omega). V1 = (0). V1 by VECTSP_9:33;
then A6: the carrier of V1 = {(0. V1)} by VECTSP_4:def 3;
rng ((Mx2Tran M,b1,b1) |^ 1) c= the carrier of V1 by RELAT_1:def 19;
then rng ((Mx2Tran M,b1,b1) |^ 1) = {(0. V1)} by A6, ZFMISC_1:39;
then (Mx2Tran M,b1,b1) |^ 1 = (dom ((Mx2Tran M,b1,b1) |^ 1)) --> (0. V1) by FUNCOP_1:15
.= the carrier of V1 --> (0. V1) by FUNCT_2:def 1
.= ZeroMap V1,V1 by GRCAT_1:def 12 ;
hence Mx2Tran M,b1,b1 is nilpotent by Th13; :: thesis: verum

end;

suppose A7: L = 0. K ; :: thesis: Mx2Tran M,b1,b1 is nilpotent

now

let i be Nat; :: thesis: ( i in dom J implies len (J . i) <= Sum (Len J) )
assume A8: i in dom J ; :: thesis: len (J . i) <= Sum (Len J)
A9: dom J = dom (Len J) by MATRIXJ1:def 3;
then len (J . i) = (Len J) . i by A8, MATRIXJ1:def 3;
hence len (J . i) <= Sum (Len J) by A8, A9, POLYNOM3:4; :: thesis: verum

end;

then (Mx2Tran M,b1,b1) |^ (Sum (Len J)) = ZeroMap V1,V1 by A1, A7, Th25;
hence Mx2Tran M,b1,b1 is nilpotent by Th13; :: thesis: verum

end;

end;