let K be Field; 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; 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; 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; ( 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
; ( 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
; ( 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; ( 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; 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; ( 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
; 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; verum