let K be doubleLoopStr ; for V being non empty ModuleStr over K
for f being nilpotent Function of V,V ex v being Vector of V st
for i being Nat st i < deg f holds
(f |^ i) . v <> 0. V
let V be non empty ModuleStr over K; for f being nilpotent Function of V,V ex v being Vector of V st
for i being Nat st i < deg f holds
(f |^ i) . v <> 0. V
let f be nilpotent Function of V,V; ex v being Vector of V st
for i being Nat st i < deg f holds
(f |^ i) . v <> 0. V
set D = deg f;
defpred S1[ Nat] means ( 0 < $1 & $1 < deg f & (f |^ $1) . (0. V) = 0. V );
assume A1:
for v being Vector of V ex i being Nat st
( i < deg f & (f |^ i) . v = 0. V )
; contradiction
then
ex i being Nat st
( i < deg f & (f |^ i) . (0. V) = 0. V )
;
then
[#] V <> {(0. V)}
by Th15;
then consider v being object such that
A2:
v in [#] V
and
A3:
v <> 0. V
by ZFMISC_1:35;
reconsider v = v as Vector of V by A2;
consider j being Nat such that
A4:
j < deg f
and
A5:
(f |^ j) . v = 0. V
by A1;
A6:
j - j < (deg f) - j
by A4, XREAL_1:9;
j > 0
then A7:
(deg f) - j < (deg f) - 0
by XREAL_1:10;
A8:
dom (f |^ j) = [#] V
by FUNCT_2:def 1;
A9:
(deg f) - j = (deg f) -' j
by A4, XREAL_1:233;
then A10:
deg f = ((deg f) -' j) + j
;
A11: f |^ (deg f) =
ZeroMap (V,V)
by Def5
.=
the carrier of V --> (0. V)
by GRCAT_1:def 7
;
then 0. V =
(f |^ (deg f)) . v
.=
((f |^ ((deg f) -' j)) * (f |^ j)) . v
by A10, VECTSP11:20
.=
(f |^ ((deg f) -' j)) . (0. V)
by A5, A8, FUNCT_1:13
;
then A12:
ex j being Nat st S1[j]
by A9, A6, A7;
consider m being Nat such that
A13:
( S1[m] & ( for n being Nat st S1[n] holds
m <= n ) )
from NAT_1:sch 5(A12);
A14:
(deg f) -' m = (deg f) - m
by A13, XREAL_1:233;
A15:
now for x being object st x in dom (f |^ ((deg f) -' m)) holds
(f |^ ((deg f) -' m)) . x = 0. Vlet x be
object ;
( x in dom (f |^ ((deg f) -' m)) implies (f |^ ((deg f) -' m)) . x = 0. V )assume
x in dom (f |^ ((deg f) -' m))
;
(f |^ ((deg f) -' m)) . x = 0. Vthen reconsider X =
x as
Vector of
V by FUNCT_2:def 1;
consider k being
Nat such that A16:
k < deg f
and A17:
(f |^ k) . X = 0. V
by A1;
defpred S2[
Nat]
means ( $1
<= deg f & ex
i being
Nat st $1
= k + (i * m) );
k = k + (0 * m)
;
then A18:
ex
k being
Nat st
S2[
k]
by A16;
A19:
for
i being
Nat st
S2[
i] holds
i <= deg f
;
consider MAX being
Nat such that A20:
S2[
MAX]
and A21:
for
k being
Nat st
S2[
k] holds
k <= MAX
from NAT_1:sch 6(A19, A18);
consider I being
Nat such that A22:
MAX = k + (I * m)
by A20;
now (f |^ ((deg f) -' m)) . X = 0. Vper cases
( MAX = deg f or MAX < deg f )
by A20, XXREAL_0:1;
suppose A24:
MAX < deg f
;
(f |^ ((deg f) -' m)) . X = 0. V
MAX <> 0
then A26:
(deg f) - MAX < (deg f) - 0
by XREAL_1:10;
A27:
(
(f |^ MAX) . X = 0. V &
dom (f |^ MAX) = the
carrier of
V )
by A13, A17, A22, FUNCT_2:def 1, VECTSP11:21;
A28:
MAX - MAX < (deg f) - MAX
by A24, XREAL_1:9;
A29:
(deg f) - MAX = (deg f) -' MAX
by A24, XREAL_1:233;
then A30:
deg f = ((deg f) -' MAX) + MAX
;
0. V =
(f |^ (deg f)) . X
by A11
.=
((f |^ ((deg f) -' MAX)) * (f |^ MAX)) . X
by A30, VECTSP11:20
.=
(f |^ ((deg f) -' MAX)) . (0. V)
by A27, FUNCT_1:13
;
then
m <= (deg f) -' MAX
by A13, A29, A28, A26;
then A31:
MAX + m <= MAX + ((deg f) - MAX)
by A29, XREAL_1:6;
MAX + m = k + ((I + 1) * m)
by A22;
then
MAX + m <= MAX + 0
by A21, A31;
hence
(f |^ ((deg f) -' m)) . X = 0. V
by A13, XREAL_1:6;
verum end; hence
(f |^ ((deg f) -' m)) . x = 0. V
;
verum end;
A32:
(deg f) - m < (deg f) - 0
by A13, XREAL_1:10;
dom (f |^ ((deg f) -' m)) = [#] V
by FUNCT_2:def 1;
then f |^ ((deg f) -' m) =
the carrier of V --> (0. V)
by A15, FUNCOP_1:11
.=
ZeroMap (V,V)
by GRCAT_1:def 7
;
hence
contradiction
by A14, A32, Def5; verum