let K be doubleLoopStr ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ) ; :: thesis: 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
proof
assume j <= 0 ; :: thesis: contradiction
then j = 0 ;
then 0. V = (id V) . v by A5, VECTSP11:18
.= v by FUNCT_1:18 ;
hence contradiction by A3; :: thesis: verum
end;
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 :: thesis: for x being object st x in dom (f |^ ((deg f) -' m)) holds
(f |^ ((deg f) -' m)) . x = 0. V
let x be object ; :: thesis: ( x in dom (f |^ ((deg f) -' m)) implies (f |^ ((deg f) -' m)) . x = 0. V )
assume x in dom (f |^ ((deg f) -' m)) ; :: thesis: (f |^ ((deg f) -' m)) . x = 0. V
then 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 :: thesis: (f |^ ((deg f) -' m)) . X = 0. V
per cases ( MAX = deg f or MAX < deg f ) by A20, XXREAL_0:1;
suppose A23: MAX = deg f ; :: thesis: (f |^ ((deg f) -' m)) . X = 0. V
then I <> 0 by A16, A22;
then reconsider I1 = I - 1 as Nat by NAT_1:20;
(deg f) -' m = k + (I1 * m) by A14, A22, A23;
hence (f |^ ((deg f) -' m)) . X = 0. V by A13, A17, VECTSP11:21; :: thesis: verum
end;
suppose A24: MAX < deg f ; :: thesis: (f |^ ((deg f) -' m)) . X = 0. V
MAX <> 0
proof
assume A25: MAX = 0 ; :: thesis: contradiction
then k = 0 by A22;
then k + (1 * m) < deg f by A13;
hence contradiction by A13, A21, A25; :: thesis: verum
end;
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; :: thesis: verum
end;
end;
end;
hence (f |^ ((deg f) -' m)) . x = 0. V ; :: thesis: 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; :: thesis: verum