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)) holds
for m being Nat st ( for i being Nat st i in dom J holds
len (J . i) <= m ) holds
(Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1)
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)) holds
for m being Nat st ( for i being Nat st i in dom J holds
len (J . i) <= m ) holds
(Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1)
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)) holds
for m being Nat st ( for i being Nat st i in dom J holds
len (J . i) <= m ) holds
(Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1)
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)) holds
for m being Nat st ( for i being Nat st i in dom J holds
len (J . i) <= m ) holds
(Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1)
let M be Matrix of len b1, len b1,K; :: thesis: ( M = block_diagonal (J,(0. K)) implies for m being Nat st ( for i being Nat st i in dom J holds
len (J . i) <= m ) holds
(Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1) )
assume A1: M = block_diagonal (J,(0. K)) ; :: thesis: for m being Nat st ( for i being Nat st i in dom J holds
len (J . i) <= m ) holds
(Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1)
reconsider Z = ZeroMap (V1,V1) as linear-transformation of V1,V1 ;
set MT = Mx2Tran (M,b1,b1);
let m be Nat; :: thesis: ( ( for i being Nat st i in dom J holds
len (J . i) <= m ) implies (Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1) )
assume A2: for i being Nat st i in dom J holds
len (J . i) <= m ; :: thesis: (Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1)
A3: ( dom Z = the carrier of V1 & rng b1 c= the carrier of V1 ) by FUNCT_2:def 1, RELAT_1:def 19;
set MTm = (Mx2Tran (M,b1,b1)) |^ m;
A4: dom ((Mx2Tran (M,b1,b1)) |^ m) = the carrier of V1 by FUNCT_2:def 1;
per cases ( len b1 = 0 or len b1 > 0 ) ;
suppose len b1 = 0 ; :: thesis: (Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1)
then dim V1 = 0 by MATRLIN2:21;
then (Omega). V1 = (0). V1 by VECTSP_9:29;
then A5: the carrier of V1 = {(0. V1)} by VECTSP_4:def 3;
rng ((Mx2Tran (M,b1,b1)) |^ m) c= the carrier of V1 by RELAT_1:def 19;
then rng ((Mx2Tran (M,b1,b1)) |^ m) = {(0. V1)} by A5, ZFMISC_1:33;
then (Mx2Tran (M,b1,b1)) |^ m = the carrier of V1 --> (0. V1) by A4, FUNCOP_1:9
.= Z by GRCAT_1:def 7 ;
hence (Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1) ; :: thesis: verum
end;
suppose A6: len b1 > 0 ; :: thesis: (Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1)
A7: dom J = dom (Len J) by MATRIXJ1:def 3;
A8: ( len M = len b1 & len M = Sum (Len J) ) by A1, MATRIX_0:24;
A9: now :: thesis: for x being object st x in dom b1 holds
(Z * b1) . x = (((Mx2Tran (M,b1,b1)) |^ m) * b1) . x
let x be object ; :: thesis: ( x in dom b1 implies (Z * b1) . x = (((Mx2Tran (M,b1,b1)) |^ m) * b1) . x )
assume A10: x in dom b1 ; :: thesis: (Z * b1) . x = (((Mx2Tran (M,b1,b1)) |^ m) * b1) . x
reconsider n = x as Element of NAT by A10;
set mm = min ((Len J),n);
A11: n in Seg (Sum (Len J)) by A8, A10, FINSEQ_1:def 3;
then A12: min ((Len J),n) in dom (Len J) by MATRIXJ1:def 1;
then A13: (Len J) . (min ((Len J),n)) = len (J . (min ((Len J),n))) by MATRIXJ1:def 3;
A14: (Len J) | (min ((Len J),n)) = Len (J | (min ((Len J),n))) by MATRIXJ1:17;
A15: now :: thesis: for k being Nat st n + k <= Sum (Len (J | (min ((Len J),n)))) holds
n + k in dom b1
min ((Len J),n) <= len (Len J) by A12, FINSEQ_3:25;
then Sum (Len (J | (min ((Len J),n)))) <= Sum ((Len J) | (len (Len J))) by A14, POLYNOM3:18;
then A16: Sum (Len (J | (min ((Len J),n)))) <= len b1 by A8, FINSEQ_1:58;
let k be Nat; :: thesis: ( n + k <= Sum (Len (J | (min ((Len J),n)))) implies n + k in dom b1 )
assume n + k <= Sum (Len (J | (min ((Len J),n)))) ; :: thesis: n + k in dom b1
then A17: n + k <= len b1 by A16, XXREAL_0:2;
( 1 <= n & n <= n + k ) by A11, FINSEQ_1:1, NAT_1:11;
then 1 <= n + k by XXREAL_0:2;
hence n + k in dom b1 by A17, FINSEQ_3:25; :: thesis: verum
end;
defpred S1[ Nat] means ((Mx2Tran (M,b1,b1)) |^ ($1 + 1)) . (b1 /. n) = 0. V1;
defpred S2[ Nat] means ( n + $1 < Sum (Len (J | (min ((Len J),n)))) implies ((Mx2Tran (M,b1,b1)) |^ ($1 + 1)) . (b1 /. n) = b1 /. ((n + $1) + 1) );
set Sm = Sum ((Len J) | ((min ((Len J),n)) -' 1));
A18: (Len J) . (min ((Len J),n)) = (Len J) /. (min ((Len J),n)) by A12, PARTFUN1:def 6;
(min ((Len J),n)) -' 1 = (min ((Len J),n)) - 1 by A11, MATRIXJ1:7;
then ((min ((Len J),n)) -' 1) + 1 = min ((Len J),n) ;
then (Len J) | (min ((Len J),n)) = ((Len J) | ((min ((Len J),n)) -' 1)) ^ <*((Len J) . (min ((Len J),n)))*> by A12, FINSEQ_5:10;
then A19: Sum (Len (J | (min ((Len J),n)))) = (Sum ((Len J) | ((min ((Len J),n)) -' 1))) + (len (J . (min ((Len J),n)))) by A14, A13, RVSUM_1:74;
A20: Sum ((Len J) | ((min ((Len J),n)) -' 1)) < n by A11, MATRIXJ1:7;
then A21: n -' (Sum ((Len J) | ((min ((Len J),n)) -' 1))) = n - (Sum ((Len J) | ((min ((Len J),n)) -' 1))) by XREAL_1:233;
then A22: n -' (Sum ((Len J) | ((min ((Len J),n)) -' 1))) <> 0 by A11, MATRIXJ1:7;
A23: now :: thesis: for k being Nat st n + k <= Sum (Len (J | (min ((Len J),n)))) holds
min ((Len J),(n + k)) = min ((Len J),n)
let k be Nat; :: thesis: ( n + k <= Sum (Len (J | (min ((Len J),n)))) implies min ((Len J),(n + k)) = min ((Len J),n) )
assume n + k <= Sum (Len (J | (min ((Len J),n)))) ; :: thesis: min ((Len J),(n + k)) = min ((Len J),n)
then A24: (n + k) - (Sum ((Len J) | ((min ((Len J),n)) -' 1))) <= ((Sum ((Len J) | ((min ((Len J),n)) -' 1))) + (len (J . (min ((Len J),n))))) - (Sum ((Len J) | ((min ((Len J),n)) -' 1))) by A19, XREAL_1:9;
1 <= (n -' (Sum ((Len J) | ((min ((Len J),n)) -' 1)))) + k by A22, NAT_1:14;
then (n -' (Sum ((Len J) | ((min ((Len J),n)) -' 1)))) + k in Seg ((Len J) /. (min ((Len J),n))) by A18, A21, A13, A24;
then min ((Len J),(((n -' (Sum ((Len J) | ((min ((Len J),n)) -' 1)))) + k) + (Sum ((Len J) | ((min ((Len J),n)) -' 1))))) = min ((Len J),n) by A12, MATRIXJ1:10;
hence min ((Len J),(n + k)) = min ((Len J),n) by A21; :: thesis: verum
end;
A25: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A26: S2[k] ; :: thesis: S2[k + 1]
set k1 = k + 1;
A27: ( the carrier of V1 = dom ((Mx2Tran (M,b1,b1)) |^ (k + 1)) & n + (k + 1) = (n + k) + 1 ) by FUNCT_2:def 1;
assume A28: n + (k + 1) < Sum (Len (J | (min ((Len J),n)))) ; :: thesis: ((Mx2Tran (M,b1,b1)) |^ ((k + 1) + 1)) . (b1 /. n) = b1 /. ((n + (k + 1)) + 1)
then ( n + (k + 1) < Sum (Len (J | (min ((Len J),(n + (k + 1)))))) & n + (k + 1) in dom b1 ) by A15, A23;
then A29: (Mx2Tran (M,b1,b1)) . (b1 /. (n + (k + 1))) = ((0. K) * (b1 /. (n + (k + 1)))) + (b1 /. ((n + (k + 1)) + 1)) by A1, Th24
.= (0. V1) + (b1 /. ((n + (k + 1)) + 1)) by VECTSP_1:14
.= b1 /. ((n + (k + 1)) + 1) by RLVECT_1:def 4 ;
thus ((Mx2Tran (M,b1,b1)) |^ ((k + 1) + 1)) . (b1 /. n) = (((Mx2Tran (M,b1,b1)) |^ 1) * ((Mx2Tran (M,b1,b1)) |^ (k + 1))) . (b1 /. n) by VECTSP11:20
.= ((Mx2Tran (M,b1,b1)) |^ 1) . (b1 /. (n + (k + 1))) by A26, A28, A27, FUNCT_1:13, NAT_1:13
.= b1 /. ((n + (k + 1)) + 1) by A29, VECTSP11:19 ; :: thesis: verum
end;
n <= Sum ((Len J) | (min ((Len J),n))) by A11, MATRIXJ1:def 1;
then A30: (Sum (Len (J | (min ((Len J),n))))) -' n = (Sum (Len (J | (min ((Len J),n))))) - n by A14, XREAL_1:233;
A31: S2[ 0 ]
proof
assume n + 0 < Sum (Len (J | (min ((Len J),n)))) ; :: thesis: ((Mx2Tran (M,b1,b1)) |^ (0 + 1)) . (b1 /. n) = b1 /. ((n + 0) + 1)
then (Mx2Tran (M,b1,b1)) . (b1 /. n) = ((0. K) * (b1 /. n)) + (b1 /. (n + 1)) by A1, A10, Th24
.= (0. V1) + (b1 /. (n + 1)) by VECTSP_1:14
.= b1 /. (n + 1) by RLVECT_1:def 4 ;
hence ((Mx2Tran (M,b1,b1)) |^ (0 + 1)) . (b1 /. n) = b1 /. ((n + 0) + 1) by VECTSP11:19; :: thesis: verum
end;
A32: for k being Nat holds S2[k] from NAT_1:sch 2(A31, A25);
A33: S1[(Sum (Len (J | (min ((Len J),n))))) -' n]
proof
per cases ( (Sum (Len (J | (min ((Len J),n))))) -' n = 0 or (Sum (Len (J | (min ((Len J),n))))) -' n > 0 ) ;
suppose A34: (Sum (Len (J | (min ((Len J),n))))) -' n = 0 ; :: thesis: S1[(Sum (Len (J | (min ((Len J),n))))) -' n]
then (Mx2Tran (M,b1,b1)) . (b1 /. n) = (0. K) * (b1 /. n) by A1, A10, A30, Th24
.= 0. V1 by VECTSP_1:14 ;
hence S1[(Sum (Len (J | (min ((Len J),n))))) -' n] by A34, VECTSP11:19; :: thesis: verum
end;
suppose (Sum (Len (J | (min ((Len J),n))))) -' n > 0 ; :: thesis: S1[(Sum (Len (J | (min ((Len J),n))))) -' n]
then reconsider S1 = ((Sum (Len (J | (min ((Len J),n))))) -' n) - 1 as Element of NAT by NAT_1:20;
A35: the carrier of V1 = dom ((Mx2Tran (M,b1,b1)) |^ ((Sum (Len (J | (min ((Len J),n))))) -' n)) by FUNCT_2:def 1;
(Sum (Len (J | (min ((Len J),n))))) - 1 < (Sum (Len (J | (min ((Len J),n))))) - 0 by XREAL_1:10;
then A36: ((Mx2Tran (M,b1,b1)) |^ (S1 + 1)) . (b1 /. n) = b1 /. ((n + S1) + 1) by A30, A32
.= b1 /. (Sum (Len (J | (min ((Len J),n))))) by A30 ;
((Sum (Len (J | (min ((Len J),n))))) -' n) + n = Sum (Len (J | (min ((Len J),n)))) by A30;
then ( Sum (Len (J | (min ((Len J),n)))) in dom b1 & min ((Len J),(Sum (Len (J | (min ((Len J),n)))))) = min ((Len J),n) ) by A15, A23;
then A37: (Mx2Tran (M,b1,b1)) . (b1 /. (Sum (Len (J | (min ((Len J),n)))))) = (0. K) * (b1 /. (Sum (Len (J | (min ((Len J),n)))))) by A1, Th24
.= 0. V1 by VECTSP_1:14 ;
thus ((Mx2Tran (M,b1,b1)) |^ (((Sum (Len (J | (min ((Len J),n))))) -' n) + 1)) . (b1 /. n) = (((Mx2Tran (M,b1,b1)) |^ 1) * ((Mx2Tran (M,b1,b1)) |^ ((Sum (Len (J | (min ((Len J),n))))) -' n))) . (b1 /. n) by VECTSP11:20
.= ((Mx2Tran (M,b1,b1)) |^ 1) . (((Mx2Tran (M,b1,b1)) |^ ((Sum (Len (J | (min ((Len J),n))))) -' n)) . (b1 /. n)) by A35, FUNCT_1:13
.= 0. V1 by A36, A37, VECTSP11:19 ; :: thesis: verum
end;
end;
end;
(Sum ((Len J) | ((min ((Len J),n)) -' 1))) - n < n - n by A20, XREAL_1:9;
then A38: (len (J . (min ((Len J),n)))) + ((Sum ((Len J) | ((min ((Len J),n)) -' 1))) - n) < (len (J . (min ((Len J),n)))) + 0 by XREAL_1:6;
then 0 < m by A2, A7, A12, A30, A19;
then reconsider m1 = m - 1 as Element of NAT by NAT_1:20;
len (J . (min ((Len J),n))) <= m by A2, A7, A12;
then (Sum (Len (J | (min ((Len J),n))))) -' n < m1 + 1 by A30, A19, A38, XXREAL_0:2;
then A39: (Sum (Len (J | (min ((Len J),n))))) -' n <= m1 by NAT_1:13;
A40: for k being Nat st (Sum (Len (J | (min ((Len J),n))))) -' n <= k & S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( (Sum (Len (J | (min ((Len J),n))))) -' n <= k & S1[k] implies S1[k + 1] )
assume (Sum (Len (J | (min ((Len J),n))))) -' n <= k ; :: thesis: ( not S1[k] or S1[k + 1] )
set k1 = k + 1;
assume A41: S1[k] ; :: thesis: S1[k + 1]
A42: dom ((Mx2Tran (M,b1,b1)) |^ (k + 1)) = the carrier of V1 by FUNCT_2:def 1;
thus ((Mx2Tran (M,b1,b1)) |^ ((k + 1) + 1)) . (b1 /. n) = (((Mx2Tran (M,b1,b1)) |^ 1) * ((Mx2Tran (M,b1,b1)) |^ (k + 1))) . (b1 /. n) by VECTSP11:20
.= ((Mx2Tran (M,b1,b1)) |^ 1) . (((Mx2Tran (M,b1,b1)) |^ (k + 1)) . (b1 /. n)) by A42, FUNCT_1:13
.= (Mx2Tran (M,b1,b1)) . (0. V1) by A41, VECTSP11:19
.= (Mx2Tran (M,b1,b1)) . ((0. K) * (0. V1)) by VECTSP_1:14
.= (0. K) * ((Mx2Tran (M,b1,b1)) . (0. V1)) by MOD_2:def 2
.= 0. V1 by VECTSP_1:14 ; :: thesis: verum
end;
for k being Nat st (Sum (Len (J | (min ((Len J),n))))) -' n <= k holds
S1[k] from NAT_1:sch 8(A33, A40);
then A43: ((Mx2Tran (M,b1,b1)) |^ (m1 + 1)) . (b1 /. n) = 0. V1 by A39;
thus (Z * b1) . x = Z . (b1 . x) by A10, FUNCT_1:13
.= Z . (b1 /. x) by A10, PARTFUN1:def 6
.= ( the carrier of V1 --> (0. V1)) . (b1 /. x) by GRCAT_1:def 7
.= 0. V1
.= ((Mx2Tran (M,b1,b1)) |^ m) . (b1 . n) by A10, A43, PARTFUN1:def 6
.= (((Mx2Tran (M,b1,b1)) |^ m) * b1) . x by A10, FUNCT_1:13 ; :: thesis: verum
end;
( dom (Z * b1) = dom b1 & dom (((Mx2Tran (M,b1,b1)) |^ m) * b1) = dom b1 ) by A4, A3, RELAT_1:27;
hence (Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1) by A6, A9, FUNCT_1:2, MATRLIN:22; :: thesis: verum
end;
end;