let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L1, L2 being Scalar of K st f is with_eigenvalues & L1 <> L2 & L1 is eigenvalue of f & L2 is eigenvalue of f holds
for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1
for L1, L2 being Scalar of K st f is with_eigenvalues & L1 <> L2 & L1 is eigenvalue of f & L2 is eigenvalue of f holds
for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
let f be linear-transformation of V1,V1; :: thesis: for L1, L2 being Scalar of K st f is with_eigenvalues & L1 <> L2 & L1 is eigenvalue of f & L2 is eigenvalue of f holds
for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
let L1, L2 be Scalar of K; :: thesis: ( f is with_eigenvalues & L1 <> L2 & L1 is eigenvalue of f & L2 is eigenvalue of f implies for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I ) )
assume that
A1: f is with_eigenvalues and
A2: L1 <> L2 and
L1 is eigenvalue of f and
A3: L2 is eigenvalue of f ; :: thesis: for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
set V = V1;
set f1 = f + ((- L1) * (id V1));
set f2 = f + ((- L2) * (id V1));
set U = UnionKers (f + ((- L1) * (id V1)));
let I be Linear_Compl of UnionKers (f + ((- L1) * (id V1))); :: thesis: for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
let fI be linear-transformation of I,I; :: thesis: ( fI = f | I implies ( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I ) )
assume A4: fI = f | I ; :: thesis: ( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
reconsider fU = f | (UnionKers (f + ((- L1) * (id V1)))) as linear-transformation of (UnionKers (f + ((- L1) * (id V1)))),(UnionKers (f + ((- L1) * (id V1)))) by Th31;
A5: now
let v be Vector of V1; :: thesis: ( v in UnionKers (f + ((- L2) * (id V1))) implies v is Vector of I )
assume A6: v in UnionKers (f + ((- L2) * (id V1))) ; :: thesis: v is Vector of I
set v1 = v |-- I,(UnionKers (f + ((- L1) * (id V1))));
set i1 = (v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `1 ;
set u1 = (v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ;
A7: V1 is_the_direct_sum_of I, UnionKers (f + ((- L1) * (id V1))) by VECTSP_5:def 5;
then A8: ( v = ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `1 ) + ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ) & (v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `1 in I & (v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 in UnionKers (f + ((- L1) * (id V1))) ) by VECTSP_5:def 6;
consider n being Nat such that
A9: ((f + ((- L1) * (id V1))) |^ n) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ) = 0. V1 by A8, Th24;
assume A10: v is not Vector of I ; :: thesis: contradiction
A11: (v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 <> 0. V1
proof
assume (v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 = 0. V1 ; :: thesis: contradiction
then v = (v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `1 by A8, RLVECT_1:def 7;
hence contradiction by A8, A10, STRUCT_0:def 5; :: thesis: verum
end;
set L21 = L2 - L1;
set f21 = (f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1));
n <> 0
proof
assume n = 0 ; :: thesis: contradiction
then 0. V1 = (id V1) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ) by A9, Th18
.= (v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 by FUNCT_1:35 ;
hence contradiction by A11; :: thesis: verum
end;
then consider h being linear-transformation of V1,V1 such that
A12: ((f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1))) |^ n = ((f + ((- L2) * (id V1))) * h) + (((L2 - L1) * (id V1)) |^ n) and
A13: for i being Nat holds ((f + ((- L2) * (id V1))) |^ i) * h = h * ((f + ((- L2) * (id V1))) |^ i) by Th38, NAT_1:14;
consider m being Nat such that
A14: ((f + ((- L2) * (id V1))) |^ m) . v = 0. V1 by A6, Th24;
defpred S1[ Nat] means for W being Subspace of V1 st ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) holds
for w being Vector of V1 st w in W holds
((f + ((- L2) * (id V1))) |^ $1) . w in W;
A15: S1[ 0 ]
proof
let W be Subspace of V1; :: thesis: ( ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) implies for w being Vector of V1 st w in W holds
((f + ((- L2) * (id V1))) |^ 0 ) . w in W )
assume ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) ; :: thesis: for w being Vector of V1 st w in W holds
((f + ((- L2) * (id V1))) |^ 0 ) . w in W
let w be Vector of V1; :: thesis: ( w in W implies ((f + ((- L2) * (id V1))) |^ 0 ) . w in W )
assume A16: w in W ; :: thesis: ((f + ((- L2) * (id V1))) |^ 0 ) . w in W
((f + ((- L2) * (id V1))) |^ 0 ) . w = (id V1) . w by Th18
.= w by FUNCT_1:35 ;
hence ((f + ((- L2) * (id V1))) |^ 0 ) . w in W by A16; :: thesis: verum
end;
A17: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A18: S1[n] ; :: thesis: S1[n + 1]
let W be Subspace of V1; :: thesis: ( ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) implies for w being Vector of V1 st w in W holds
((f + ((- L2) * (id V1))) |^ (n + 1)) . w in W )
assume A19: ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) ; :: thesis: for w being Vector of V1 st w in W holds
((f + ((- L2) * (id V1))) |^ (n + 1)) . w in W
let w be Vector of V1; :: thesis: ( w in W implies ((f + ((- L2) * (id V1))) |^ (n + 1)) . w in W )
assume A20: w in W ; :: thesis: ((f + ((- L2) * (id V1))) |^ (n + 1)) . w in W
A21: dom ((f + ((- L2) * (id V1))) |^ n) = [#] V1 by FUNCT_2:def 1;
set fnw = ((f + ((- L2) * (id V1))) |^ n) . w;
A22: ((f + ((- L2) * (id V1))) |^ n) . w in W by A18, A19, A20;
A23: now
per cases ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) by A19;
suppose A24: W = I ; :: thesis: f . (((f + ((- L2) * (id V1))) |^ n) . w) in W
then reconsider F = ((f + ((- L2) * (id V1))) |^ n) . w as Vector of I by A22, STRUCT_0:def 5;
f . (((f + ((- L2) * (id V1))) |^ n) . w) = fI . F by A4, FUNCT_1:72;
hence f . (((f + ((- L2) * (id V1))) |^ n) . w) in W by A24, STRUCT_0:def 5; :: thesis: verum
end;
suppose A25: W = UnionKers (f + ((- L1) * (id V1))) ; :: thesis: f . (((f + ((- L2) * (id V1))) |^ n) . w) in W
then reconsider F = ((f + ((- L2) * (id V1))) |^ n) . w as Vector of (UnionKers (f + ((- L1) * (id V1)))) by A22, STRUCT_0:def 5;
f . (((f + ((- L2) * (id V1))) |^ n) . w) = fU . F by FUNCT_1:72;
hence f . (((f + ((- L2) * (id V1))) |^ n) . w) in W by A25, STRUCT_0:def 5; :: thesis: verum
end;
end;
end;
((- L2) * (id V1)) . (((f + ((- L2) * (id V1))) |^ n) . w) = (- L2) * ((id V1) . (((f + ((- L2) * (id V1))) |^ n) . w)) by MATRLIN:def 6
.= (- L2) * (((f + ((- L2) * (id V1))) |^ n) . w) by FUNCT_1:35 ;
then A26: ((- L2) * (id V1)) . (((f + ((- L2) * (id V1))) |^ n) . w) in W by A22, VECTSP_4:29;
((f + ((- L2) * (id V1))) |^ (n + 1)) . w = (((f + ((- L2) * (id V1))) |^ 1) * ((f + ((- L2) * (id V1))) |^ n)) . w by Th20
.= ((f + ((- L2) * (id V1))) |^ 1) . (((f + ((- L2) * (id V1))) |^ n) . w) by A21, FUNCT_1:23
.= (f + ((- L2) * (id V1))) . (((f + ((- L2) * (id V1))) |^ n) . w) by Th19
.= (f . (((f + ((- L2) * (id V1))) |^ n) . w)) + (((- L2) * (id V1)) . (((f + ((- L2) * (id V1))) |^ n) . w)) by MATRLIN:def 5 ;
hence ((f + ((- L2) * (id V1))) |^ (n + 1)) . w in W by A23, A26, VECTSP_4:28; :: thesis: verum
end;
A27: for n being Nat holds S1[n] from NAT_1:sch 2(A15, A17);
defpred S2[ Nat] means ((f + ((- L2) * (id V1))) |^ $1) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ) = 0. V1;
A28: ( ((f + ((- L2) * (id V1))) |^ m) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `1 ) in I & ((f + ((- L2) * (id V1))) |^ m) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ) in UnionKers (f + ((- L1) * (id V1))) & 0. V1 in I & 0. V1 in UnionKers (f + ((- L1) * (id V1))) ) by A8, A27, VECTSP_4:25;
(0. V1) + (0. V1) = 0. V1 by RLVECT_1:def 7
.= (((f + ((- L2) * (id V1))) |^ m) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `1 )) + (((f + ((- L2) * (id V1))) |^ m) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 )) by A8, A14, MOD_2:def 5 ;
then ((f + ((- L2) * (id V1))) |^ m) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ) = 0. V1 by A7, A28, VECTSP_5:58;
then A29: ex m being Nat st S2[m] ;
consider MIN being Nat such that
A30: S2[MIN] and
A31: for n being Nat st S2[n] holds
MIN <= n from NAT_1:sch 5(A29);
 MIN <> 0
proof
assume MIN = 0 ; :: thesis: contradiction
then 0. V1 = (id V1) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ) by A30, Th18
.= (v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 by FUNCT_1:35 ;
hence contradiction by A11; :: thesis: verum
end;
then reconsider M1 = MIN - 1 as Element of NAT by NAT_1:20;
A32: ((f + ((- L2) * (id V1))) |^ M1) * ((f + ((- L2) * (id V1))) * h) = (((f + ((- L2) * (id V1))) |^ M1) * (f + ((- L2) * (id V1)))) * h by RELAT_1:55
.= (((f + ((- L2) * (id V1))) |^ M1) * ((f + ((- L2) * (id V1))) |^ 1)) * h by Th19
.= ((f + ((- L2) * (id V1))) |^ (M1 + 1)) * h by Th20
.= h * ((f + ((- L2) * (id V1))) |^ MIN) by A13 ;
dom ((f + ((- L2) * (id V1))) |^ MIN) = [#] V1 by FUNCT_2:def 1;
then A33: (h * ((f + ((- L2) * (id V1))) |^ MIN)) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ) = h . (((f + ((- L2) * (id V1))) |^ MIN) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 )) by FUNCT_1:23
.= 0. V1 by A30, RANKNULL:9 ;
A34: dom (((L2 - L1) * (id V1)) |^ n) = [#] V1 by FUNCT_2:def 1;
A35: (((f + ((- L2) * (id V1))) |^ M1) * (((L2 - L1) * (id V1)) |^ n)) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ) = ((f + ((- L2) * (id V1))) |^ M1) . ((((L2 - L1) * (id V1)) |^ n) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 )) by A34, FUNCT_1:23
.= ((f + ((- L2) * (id V1))) |^ M1) . ((((power K) . (L2 - L1),n) * (id V1)) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 )) by Lm9
.= ((f + ((- L2) * (id V1))) |^ M1) . (((power K) . (L2 - L1),n) * ((id V1) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ))) by MATRLIN:def 6
.= ((f + ((- L2) * (id V1))) |^ M1) . (((power K) . (L2 - L1),n) * ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 )) by FUNCT_1:35
.= ((power K) . (L2 - L1),n) * (((f + ((- L2) * (id V1))) |^ M1) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 )) by MOD_2:def 5 ;
A36: dom (((f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1))) |^ n) = [#] V1 by FUNCT_2:def 1;
(f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1)) = f + (((- L2) * (id V1)) + ((L2 - L1) * (id V1))) by Lm8
.= f + (((- L2) + (L2 - L1)) * (id V1)) by Lm10
.= f + ((((- L2) + L2) - L1) * (id V1)) by RLVECT_1:def 6
.= f + (((0. K) + (- L1)) * (id V1)) by VECTSP_1:66
.= f + ((- L1) * (id V1)) by RLVECT_1:def 7 ;
then A37: 0. V1 = ((f + ((- L2) * (id V1))) |^ M1) . ((((f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1))) |^ n) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 )) by A9, RANKNULL:9
.= (((f + ((- L2) * (id V1))) |^ M1) * (((f + ((- L2) * (id V1))) * h) + (((L2 - L1) * (id V1)) |^ n))) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ) by A12, A36, FUNCT_1:23
.= ((h * ((f + ((- L2) * (id V1))) |^ MIN)) + (((f + ((- L2) * (id V1))) |^ M1) * (((L2 - L1) * (id V1)) |^ n))) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ) by A32, Lm7
.= (0. V1) + (((power K) . (L2 - L1),n) * (((f + ((- L2) * (id V1))) |^ M1) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ))) by A33, A35, MATRLIN:def 5
.= ((power K) . (L2 - L1),n) * (((f + ((- L2) * (id V1))) |^ M1) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 )) by RLVECT_1:def 7 ;
(power K) . (L2 - L1),n <> 0. K
proof
assume 0. K = (power K) . (L2 - L1),n ; :: thesis: contradiction
then 0. K = Product (n |-> (L2 - L1)) by MATRIXJ1:5;
then consider k being Element of NAT such that
A38: ( k in dom (n |-> (L2 - L1)) & (n |-> (L2 - L1)) . k = 0. K ) by FVSUM_1:107;
dom (n |-> (L2 - L1)) = Seg n by FINSEQ_2:144;
then L2 - L1 = 0. K by A38, FINSEQ_2:71;
hence contradiction by A2, VECTSP_1:66; :: thesis: verum
end;
then ((f + ((- L2) * (id V1))) |^ M1) . ((v |-- I,(UnionKers (f + ((- L1) * (id V1))))) `2 ) = 0. V1 by A37, VECTSP_1:60;
then M1 + 1 <= M1 by A31;
hence contradiction by NAT_1:13; :: thesis: verum
end;
consider v being Vector of V1 such that
A39: ( v <> 0. V1 & f . v = L2 * v ) by A1, A3, Def2;
v is eigenvector of f,L2 by A1, A3, A39, Def3;
then v in ker (f + ((- L2) * (id V1))) by A1, A3, Th17;
then 0. V1 = (f + ((- L2) * (id V1))) . v by RANKNULL:10
.= ((f + ((- L2) * (id V1))) |^ 1) . v by Th19 ;
then v in UnionKers (f + ((- L2) * (id V1))) by Th24;
then reconsider vI = v as Vector of I by A5;
A40: ( 0. V1 = 0. I & L2 * v = L2 * vI & f . v = fI . vI ) by A4, FUNCT_1:72, VECTSP_4:19, VECTSP_4:22;
hence A41: fI is with_eigenvalues by A39, Def1; :: thesis: ( L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
L1 is not eigenvalue of fI
proof
assume L1 is eigenvalue of fI ; :: thesis: contradiction
then consider w being Vector of I such that
A42: ( w <> 0. I & fI . w = L1 * w ) by A41, Def2;
w = 0. V1 by A4, A42, Th37;
hence contradiction by A42, VECTSP_4:19; :: thesis: verum
end;
hence ( L1 is not eigenvalue of fI & L2 is eigenvalue of fI ) by A39, A40, A41, Def2; :: thesis: UnionKers (f + ((- L2) * (id V1))) is Subspace of I
the carrier of (UnionKers (f + ((- L2) * (id V1)))) c= the carrier of I
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (UnionKers (f + ((- L2) * (id V1)))) or x in the carrier of I )
assume A43: x in the carrier of (UnionKers (f + ((- L2) * (id V1)))) ; :: thesis: x in the carrier of I
A44: x in UnionKers (f + ((- L2) * (id V1))) by A43, STRUCT_0:def 5;
then x in V1 by VECTSP_4:17;
then reconsider v = x as Vector of V1 by STRUCT_0:def 5;
v is Vector of I by A5, A44;
hence x in the carrier of I ; :: thesis: verum
end;
hence UnionKers (f + ((- L2) * (id V1))) is Subspace of I by VECTSP_4:35; :: thesis: verum