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