let K be Field; :: thesis: for V1 being VectSp of K
for v1 being Vector of V1
for f being linear-transformation of V1,V1
for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
let V1 be VectSp of K; :: thesis: for v1 being Vector of V1
for f being linear-transformation of V1,V1
for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
let v1 be Vector of V1; :: thesis: for f being linear-transformation of V1,V1
for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
let f be linear-transformation of V1,V1; :: thesis: for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
let L be Scalar of K; :: thesis: ( f is with_eigenvalues & L is eigenvalue of f implies ( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) ) )
assume A1: ( f is with_eigenvalues & L is eigenvalue of f ) ; :: thesis: ( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )

hereby :: thesis: ( v1 in ker (f + ((- L) * (id V1))) implies v1 is eigenvector of f,L )

assume v1 is eigenvector of f,L ; :: thesis: v1 in ker (f + ((- L) * (id V1)))
then A2: f . v1 = L * v1 by A1, Def3;
(f + ((- L) * (id V1))) . v1 = (f . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def 3
.= (f . v1) + ((- L) * ((id V1) . v1)) by MATRLIN:def 4
.= (f . v1) + ((- L) * v1)
.= (L + (- L)) * v1 by A2, VECTSP_1:def 15
.= (0. K) * v1 by VECTSP_1:19
.= 0. V1 by VECTSP_1:15 ;
hence v1 in ker (f + ((- L) * (id V1))) by RANKNULL:10; :: thesis: verum

end;

assume v1 in ker (f + ((- L) * (id V1))) ; :: thesis: v1 is eigenvector of f,L
then 0. V1 = (f + ((- L) * (id V1))) . v1 by RANKNULL:10
.= (f . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def 3
.= (f . v1) + ((- L) * ((id V1) . v1)) by MATRLIN:def 4
.= (f . v1) + ((- L) * v1) ;
then f . v1 = - ((- L) * v1) by VECTSP_1:16
.= (- (- L)) * v1 by VECTSP_1:21
.= L * v1 by RLVECT_1:17 ;
hence v1 is eigenvector of f,L by A1, Def3; :: thesis: verum