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