let K be Field; 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; 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; 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; 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; ( 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))
; 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; ( ( 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
; (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
;
(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)
;
verum end; suppose A6:
len b1 > 0
;
(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 for x being object st x in dom b1 holds
(Z * b1) . x = (((Mx2Tran (M,b1,b1)) |^ m) * b1) . xlet x be
object ;
( x in dom b1 implies (Z * b1) . x = (((Mx2Tran (M,b1,b1)) |^ m) * b1) . x )assume A10:
x in dom b1
;
(Z * b1) . x = (((Mx2Tran (M,b1,b1)) |^ m) * b1) . xreconsider 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 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;
( 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))))
;
n + k in dom b1then 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;
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 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;
( 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))))
;
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;
verum end; A25:
for
k being
Nat st
S2[
k] holds
S2[
k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A26:
S2[
k]
;
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))))
;
((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
;
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 ]
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
(Sum (Len (J | (min ((Len J),n))))) -' n > 0
;
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
;
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;
( (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
;
( not S1[k] or S1[k + 1] )
set k1 =
k + 1;
assume A41:
S1[
k]
;
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
;
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
;
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;
verum end; end;