let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 st not ker f is trivial holds
( f is with_eigenvalues & 0. K is eigenvalue of f )
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1 st not ker f is trivial holds
( f is with_eigenvalues & 0. K is eigenvalue of f )
let f be linear-transformation of V1,V1; :: thesis: ( not ker f is trivial implies ( f is with_eigenvalues & 0. K is eigenvalue of f ) )
assume not ker f is trivial ; :: thesis: ( f is with_eigenvalues & 0. K is eigenvalue of f )
then consider v being Vector of (ker f) such that
A1: v <> 0. (ker f) ;
reconsider v = v as Vector of V1 by VECTSP_4:10;
A2: f . v = 0. V1 by RANKNULL:14
.= (0. K) * v by VECTSP_1:14 ;
A3: v <> 0. V1 by A1, VECTSP_4:11;
then f is with_eigenvalues by A2;
hence ( f is with_eigenvalues & 0. K is eigenvalue of f ) by A3, A2, Def2; :: thesis: verum