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

set B = len b1;
set m = min ((Len J),(len b1));
set S = Sum (Len (J | (min ((Len J),(len b1)))));
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 ;
rng b1 is Basis of V1 by MATRLIN:def 2;
then A2: rng b1 is linearly-independent Subset of V1 by VECTSP_7:def 3;
assume A3: len b1 <> 0 ; :: thesis: L = 0. K
then Sum (Len (J | (min ((Len J),(len b1))))) in dom b1 by A1, Lm3;
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)))))) ) by FUNCT_1:def 3, PARTFUN1:def 6;
then A4: b1 /. (Sum (Len (J | (min ((Len J),(len b1)))))) <> 0. V1 by A2, VECTSP_7:2;
((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, A3, 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 7
.= 0. V1
.= (0. K) * (b1 /. (Sum (Len (J | (min ((Len J),(len b1))))))) by VECTSP_1:14 ;
then 0. K = (power K) . (L,(deg MT)) by A4, VECTSP10:4
.= Product ((deg MT) |-> L) by MATRIXJ1:5 ;
then A5: ex k being Nat st
( k in dom ((deg MT) |-> L) & ((deg MT) |-> L) . k = 0. K ) by FVSUM_1:82;
dom ((deg MT) |-> L) = Seg (deg MT) by FINSEQ_2:124;
hence L = 0. K by A5, FINSEQ_2:57; :: thesis: verum

end;

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

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

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:29;
then A7: 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 A7, ZFMISC_1:33;
then (Mx2Tran (M,b1,b1)) |^ 1 = (dom ((Mx2Tran (M,b1,b1)) |^ 1)) --> (0. V1) by FUNCOP_1:9
.= the carrier of V1 --> (0. V1) by FUNCT_2:def 1
.= ZeroMap (V1,V1) by GRCAT_1:def 7 ;
hence Mx2Tran (M,b1,b1) is nilpotent by Th13; :: thesis: verum

end;

suppose A8: L = 0. K ; :: thesis: Mx2Tran (M,b1,b1) is nilpotent

now :: thesis: for i being Nat st i in dom J holds
len (J . i) <= Sum (Len J)

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

end;

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

end;

end;