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