let K be doubleLoopStr ; :: thesis: for V being non empty ModuleStr over K
for f being Function of V,V holds
( f is nilpotent iff ex n being Nat st f |^ n = ZeroMap (V,V) )
let V be non empty ModuleStr over K; :: thesis: for f being Function of V,V holds
( f is nilpotent iff ex n being Nat st f |^ n = ZeroMap (V,V) )
let f be Function of V,V; :: thesis: ( f is nilpotent iff ex n being Nat st f |^ n = ZeroMap (V,V) )
hereby :: thesis: ( ex n being Nat st f |^ n = ZeroMap (V,V) implies f is nilpotent )
assume f is nilpotent ; :: thesis: ex n being Nat st f |^ n = ZeroMap (V,V)
then consider n being Nat such that
A1: for v being Vector of V holds (f |^ n) . v = 0. V ;
now :: thesis: for x being object st x in dom (f |^ n) holds
(f |^ n) . x = 0. V
let x be object ; :: thesis: ( x in dom (f |^ n) implies (f |^ n) . x = 0. V )
assume x in dom (f |^ n) ; :: thesis: (f |^ n) . x = 0. V
then reconsider v = x as Vector of V by FUNCT_2:def 1;
thus (f |^ n) . x = (f |^ n) . v
.= 0. V by A1 ; :: thesis: verum
end;
then f |^ n = (dom (f |^ n)) --> (0. V) by FUNCOP_1:11
.= the carrier of V --> (0. V) by FUNCT_2:def 1
.= ZeroMap (V,V) by GRCAT_1:def 7 ;
hence ex n being Nat st f |^ n = ZeroMap (V,V) ; :: thesis: verum
end;
given n being Nat such that A2: f |^ n = ZeroMap (V,V) ; :: thesis: f is nilpotent
take n ; :: according to MATRIXJ2:def 4 :: thesis: for v being Vector of V holds (f |^ n) . v = 0. V
let v be Vector of V; :: thesis: (f |^ n) . v = 0. V
thus (f |^ n) . v = ( the carrier of V --> (0. V)) . v by A2, GRCAT_1:def 7
.= 0. V ; :: thesis: verum