let K be Field; :: thesis: for V being non trivial VectSp of K
for f1, f2 being with_eigenvalues Function of V,V
for L1, L2 being Scalar of K st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st
( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) holds
( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )
let V be non trivial VectSp of K; :: thesis: for f1, f2 being with_eigenvalues Function of V,V
for L1, L2 being Scalar of K st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st
( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) holds
( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )
let f1, f2 be with_eigenvalues Function of V,V; :: thesis: for L1, L2 being Scalar of K st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st
( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) holds
( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )
let L1, L2 be Scalar of K; :: thesis: ( L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st
( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) implies ( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) ) )
set g = f1 + f2;
assume that
A1: L1 is eigenvalue of f1 and
A2: L2 is eigenvalue of f2 ; :: thesis: ( for v being Vector of V holds
( not v is eigenvector of f1,L1 or not v is eigenvector of f2,L2 or not v <> 0. V ) or ( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) ) )
given v being Vector of V such that A3: v is eigenvector of f1,L1 and
A4: v is eigenvector of f2,L2 and
A5: v <> 0. V ; :: thesis: ( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )
A6: (f1 + f2) . v = (f1 . v) + (f2 . v) by MATRLIN:def 3
.= (L1 * v) + (f2 . v) by A1, A3, Def3
.= (L1 * v) + (L2 * v) by A2, A4, Def3
.= (L1 + L2) * v by VECTSP_1:def 15 ;
hence A7: f1 + f2 is with_eigenvalues by A5; :: thesis: ( L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )
hence A8: L1 + L2 is eigenvalue of f1 + f2 by A5, A6, Def2; :: thesis: for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2
let w be Vector of V; :: thesis: ( w is eigenvector of f1,L1 & w is eigenvector of f2,L2 implies w is eigenvector of f1 + f2,L1 + L2 )
assume that
A9: w is eigenvector of f1,L1 and
A10: w is eigenvector of f2,L2 ; :: thesis: w is eigenvector of f1 + f2,L1 + L2
(f1 + f2) . w = (f1 . w) + (f2 . w) by MATRLIN:def 3
.= (L1 * w) + (f2 . w) by A1, A9, Def3
.= (L1 * w) + (L2 * w) by A2, A10, Def3
.= (L1 + L2) * w by VECTSP_1:def 15 ;
hence w is eigenvector of f1 + f2,L1 + L2 by A7, A8, Def3; :: thesis: verum