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:33;
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:39;
then (Mx2Tran M,b1,b1) |^ m = the carrier of V1 --> (0. V1) by A4, FUNCOP_1:15
.= Z by GRCAT_1:def 12 ;
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_1:25;
A9: now
let x be set ; :: 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
min (Len J),n <= len (Len J) by A12, FINSEQ_3:27;
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:79;
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:3, NAT_1:11;
then 1 <= n + k by XXREAL_0:2;
hence n + k in dom b1 by A17, FINSEQ_3:27; :: 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 8;
(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:11;
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:104;
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:235;
then A22: n -' (Sum ((Len J) | ((min (Len J),n) -' 1))) <> 0 by A11, MATRIXJ1:7;
A23: now
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:11;
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:59
.= b1 /. ((n + (k + 1)) + 1) by RLVECT_1:def 7 ;
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:23, 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:235;
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:59
.= b1 /. (n + 1) by RLVECT_1:def 7 ;
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:59 ;
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:12;
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:59 ;
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:23
.= 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:11;
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:8;
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:23
.= (Mx2Tran M,b1,b1) . (0. V1) by A41, VECTSP11:19
.= (Mx2Tran M,b1,b1) . ((0. K) * (0. V1)) by VECTSP_1:59
.= (0. K) * ((Mx2Tran M,b1,b1) . (0. V1)) by MOD_2:def 3
.= 0. V1 by VECTSP_1:59 ; :: 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:23
.= Z . (b1 /. x) by A10, PARTFUN1:def 8
.= (the carrier of V1 --> (0. V1)) . (b1 /. x) by GRCAT_1:def 12
.= 0. V1 by FUNCOP_1:13
.= ((Mx2Tran M,b1,b1) |^ m) . (b1 . n) by A10, A43, PARTFUN1:def 8
.= (((Mx2Tran M,b1,b1) |^ m) * b1) . x by A10, FUNCT_1:23 ; :: thesis: verum
end;
( dom (Z * b1) = dom b1 & dom (((Mx2Tran M,b1,b1) |^ m) * b1) = dom b1 ) by A4, A3, RELAT_1:46;
hence (Mx2Tran M,b1,b1) |^ m = ZeroMap V1,V1 by A6, A9, FUNCT_1:9, MATRLIN:26; :: thesis: verum
end;
end;