let K be Field; :: thesis: for V being finite-dimensional VectSp of K
for f being linear-transformation of V,V
for n being Nat st UnionKers f = ker (f |^ n) holds
V is_the_direct_sum_of ker (f |^ n), im (f |^ n)
let V be finite-dimensional VectSp of K; :: thesis: for f being linear-transformation of V,V
for n being Nat st UnionKers f = ker (f |^ n) holds
V is_the_direct_sum_of ker (f |^ n), im (f |^ n)
let f be linear-transformation of V,V; :: thesis: for n being Nat st UnionKers f = ker (f |^ n) holds
V is_the_direct_sum_of ker (f |^ n), im (f |^ n)
let n be Nat; :: thesis: ( UnionKers f = ker (f |^ n) implies V is_the_direct_sum_of ker (f |^ n), im (f |^ n) )
set KER = ker (f |^ n);
set IM = im (f |^ n);
A1: dim V = (rank (f |^ n)) + (nullity (f |^ n)) by RANKNULL:44
.= (dim ((im (f |^ n)) + (ker (f |^ n)))) + (dim ((im (f |^ n)) /\ (ker (f |^ n)))) by VECTSP_9:32 ;
assume A2: UnionKers f = ker (f |^ n) ; :: thesis: V is_the_direct_sum_of ker (f |^ n), im (f |^ n)
then (Omega). ((im (f |^ n)) /\ (ker (f |^ n))) = (0). V by Th34
.= (0). ((im (f |^ n)) /\ (ker (f |^ n))) by VECTSP_4:36 ;
then dim ((im (f |^ n)) /\ (ker (f |^ n))) = 0 by VECTSP_9:29;
then (Omega). V = (Omega). ((im (f |^ n)) + (ker (f |^ n))) by A1, VECTSP_9:28;
then A3: (ker (f |^ n)) + (im (f |^ n)) = (Omega). V by VECTSP_5:5;
(ker (f |^ n)) /\ (im (f |^ n)) = (0). V by A2, Th34;
hence V is_the_direct_sum_of ker (f |^ n), im (f |^ n) by A3, VECTSP_5:def 4; :: thesis: verum