let K be algebraic-closed Field; for V1 being non trivial finite-dimensional VectSp of K
for f being linear-transformation of V1,V1 holds f is with_eigenvalues
let V1 be non trivial finite-dimensional VectSp of K; for f being linear-transformation of V1,V1 holds f is with_eigenvalues
let f be linear-transformation of V1,V1; f is with_eigenvalues
set b1 = the OrdBasis of V1;
set AutA = AutMt (f, the OrdBasis of V1, the OrdBasis of V1);
consider P being Polynomial of K such that
A1:
len P = (len the OrdBasis of V1) + 1
and
A2:
for x being Element of K holds eval (P,x) = Det ((AutMt (f, the OrdBasis of V1, the OrdBasis of V1)) + (x * (1. (K,(len the OrdBasis of V1)))))
by Th8;
( dim V1 <> 0 & dim V1 = len the OrdBasis of V1 )
by MATRLIN2:21, MATRLIN2:42;
then
len P > 1 + 0
by A1, XREAL_1:8;
then
P is with_roots
by POLYNOM5:def 9;
then consider L being Element of K such that
A3:
L is_a_root_of P
by POLYNOM5:def 8;
A4: Mx2Tran ((L * (AutMt ((id V1), the OrdBasis of V1, the OrdBasis of V1))), the OrdBasis of V1, the OrdBasis of V1) =
L * (Mx2Tran ((AutMt ((id V1), the OrdBasis of V1, the OrdBasis of V1)), the OrdBasis of V1, the OrdBasis of V1))
by MATRLIN2:38
.=
L * (id V1)
by MATRLIN2:34
.=
Mx2Tran ((AutMt ((L * (id V1)), the OrdBasis of V1, the OrdBasis of V1)), the OrdBasis of V1, the OrdBasis of V1)
by MATRLIN2:34
;
0. K =
eval (P,L)
by A3, POLYNOM5:def 7
.=
Det ((AutMt (f, the OrdBasis of V1, the OrdBasis of V1)) + (L * (1. (K,(len the OrdBasis of V1)))))
by A2
.=
Det ((AutMt (f, the OrdBasis of V1, the OrdBasis of V1)) + (L * (AutMt ((id V1), the OrdBasis of V1, the OrdBasis of V1))))
by MATRLIN2:28
.=
Det ((AutMt (f, the OrdBasis of V1, the OrdBasis of V1)) + (AutMt ((L * (id V1)), the OrdBasis of V1, the OrdBasis of V1)))
by A4, MATRLIN2:39
.=
Det (AutMt ((f + (L * (id V1))), the OrdBasis of V1, the OrdBasis of V1))
by MATRLIN:42
.=
Det (AutMt ((f + ((- (- L)) * (id V1))), the OrdBasis of V1, the OrdBasis of V1))
by RLVECT_1:17
.=
Det (AutEqMt ((f + ((- (- L)) * (id V1))), the OrdBasis of V1, the OrdBasis of V1))
by MATRLIN2:def 2
;
hence
f is with_eigenvalues
by Th15; verum