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 & 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 & 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 & 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 & 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
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;
consider v being Vector of V1 such that
A4: v <> 0. V1 and
A5: f . v = L2 * v by A1, A3, Def2;
set f1 = f + ((- L1) * (id V1));
set U = UnionKers (f + ((- L1) * (id V1)));
reconsider fU = f | (UnionKers (f + ((- L1) * (id V1)))) as linear-transformation of (UnionKers (f + ((- L1) * (id V1)))),(UnionKers (f + ((- L1) * (id V1)))) by Th31;
set f2 = f + ((- L2) * (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 A6: 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 )
A7: now :: thesis: for v being Vector of V1 st v in UnionKers (f + ((- L2) * (id V1))) holds
v is Vector of I
let v be Vector of V1; :: thesis: ( v in UnionKers (f + ((- L2) * (id V1))) implies v is Vector of I )
assume v in UnionKers (f + ((- L2) * (id V1))) ; :: thesis: v is Vector of I
then consider m being Nat such that
A8: ((f + ((- L2) * (id V1))) |^ m) . v = 0. V1 by Th24;
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 ;
A9: V1 is_the_direct_sum_of I, UnionKers (f + ((- L1) * (id V1))) by VECTSP_5:def 5;
then A10: v = ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `1) + ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) by VECTSP_5:def 6;
defpred S1[ Nat] means ((f + ((- L2) * (id V1))) |^ $1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) = 0. V1;
defpred S2[ 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;
set L21 = L2 - L1;
set f21 = (f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1));
A11: ( 0. V1 in I & 0. V1 in UnionKers (f + ((- L1) * (id V1))) ) by VECTSP_4:17;
A12: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A13: S2[n] ; :: thesis: S2[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 A14: ( 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 A15: w in W ; :: thesis: ((f + ((- L2) * (id V1))) |^ (n + 1)) . w in W
set fnw = ((f + ((- L2) * (id V1))) |^ n) . w;
A16: ((f + ((- L2) * (id V1))) |^ n) . w in W by A13, A14, A15;
A17: now :: thesis: f . (((f + ((- L2) * (id V1))) |^ n) . w) in W
per cases ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) by A14;
suppose A18: 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 A16;
f . (((f + ((- L2) * (id V1))) |^ n) . w) = fI . F by A6, FUNCT_1:49;
hence f . (((f + ((- L2) * (id V1))) |^ n) . w) in W by A18; :: thesis: verum
end;
suppose A19: 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 A16;
f . (((f + ((- L2) * (id V1))) |^ n) . w) = fU . F by FUNCT_1:49;
hence f . (((f + ((- L2) * (id V1))) |^ n) . w) in W by A19; :: 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 4
.= (- L2) * (((f + ((- L2) * (id V1))) |^ n) . w) ;
then A20: ((- L2) * (id V1)) . (((f + ((- L2) * (id V1))) |^ n) . w) in W by A16, VECTSP_4:21;
A21: dom ((f + ((- L2) * (id V1))) |^ n) = [#] V1 by FUNCT_2:def 1;
((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:13
.= (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 3 ;
hence ((f + ((- L2) * (id V1))) |^ (n + 1)) . w in W by A17, A20, VECTSP_4:20; :: thesis: verum
end;
A22: (0. V1) + (0. V1) = 0. V1 by RLVECT_1:def 4
.= (((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 A10, A8, VECTSP_1:def 20 ;
A23: (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2 in UnionKers (f + ((- L1) * (id V1))) by A9, VECTSP_5:def 6;
then consider n being Nat such that
A24: ((f + ((- L1) * (id V1))) |^ n) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) = 0. V1 by Th24;
A25: S2[ 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 A26: w in W ; :: thesis: ((f + ((- L2) * (id V1))) |^ 0) . w in W
((f + ((- L2) * (id V1))) |^ 0) . w = (id V1) . w by Th18
.= w ;
hence ((f + ((- L2) * (id V1))) |^ 0) . w in W by A26; :: thesis: verum
end;
A27: for n being Nat holds S2[n] from NAT_1:sch 2(A25, A12);
then A28: ((f + ((- L2) * (id V1))) |^ m) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) in UnionKers (f + ((- L1) * (id V1))) by A23;
A29: (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `1 in I by A9, VECTSP_5:def 6;
then ((f + ((- L2) * (id V1))) |^ m) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `1) in I by A27;
then ((f + ((- L2) * (id V1))) |^ m) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) = 0. V1 by A9, A28, A11, A22, VECTSP_5:48;
then A30: ex m being Nat st S1[m] ;
consider MIN being Nat such that
A31: S1[MIN] and
A32: for n being Nat st S1[n] holds
MIN <= n from NAT_1:sch 5(A30);
assume A33: v is not Vector of I ; :: thesis: contradiction
A34: (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2 <> 0. V1 by A10, RLVECT_1:def 4, A29, A33;
n <> 0
proof
assume n = 0 ; :: thesis: contradiction
then 0. V1 = (id V1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) by A24, Th18
.= (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2 ;
hence contradiction by A34; :: thesis: verum
end;
then consider h being linear-transformation of V1,V1 such that
A35: ((f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1))) |^ n = ((f + ((- L2) * (id V1))) * h) + (((L2 - L1) * (id V1)) |^ n) and
A36: for i being Nat holds ((f + ((- L2) * (id V1))) |^ i) * h = h * ((f + ((- L2) * (id V1))) |^ i) by Th38, NAT_1:14;
A37: dom (((f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1))) |^ n) = [#] V1 by FUNCT_2:def 1;
MIN <> 0
proof
assume MIN = 0 ; :: thesis: contradiction
then 0. V1 = (id V1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) by A31, Th18
.= (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2 ;
hence contradiction by A34; :: thesis: verum
end;
then reconsider M1 = MIN - 1 as Element of NAT by NAT_1:20;
A38: ((f + ((- L2) * (id V1))) |^ M1) * ((f + ((- L2) * (id V1))) * h) = (((f + ((- L2) * (id V1))) |^ M1) * (f + ((- L2) * (id V1)))) * h by RELAT_1:36
.= (((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 A36 ;
dom (((L2 - L1) * (id V1)) |^ n) = [#] V1 by FUNCT_2:def 1;
then A39: (((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 FUNCT_1:13
.= ((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 4
.= ((f + ((- L2) * (id V1))) |^ M1) . (((power K) . ((L2 - L1),n)) * ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2))
.= ((power K) . ((L2 - L1),n)) * (((f + ((- L2) * (id V1))) |^ M1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2)) by MOD_2:def 2 ;
A40: (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 A41: ex k being Nat st
( k in dom (n |-> (L2 - L1)) & (n |-> (L2 - L1)) . k = 0. K ) by FVSUM_1:82;
dom (n |-> (L2 - L1)) = Seg n by FINSEQ_2:124;
then L2 - L1 = 0. K by A41, FINSEQ_2:57;
hence contradiction by A2, VECTSP_1:19; :: thesis: verum
end;
dom ((f + ((- L2) * (id V1))) |^ MIN) = [#] V1 by FUNCT_2:def 1;
then A42: (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:13
.= 0. V1 by A31, RANKNULL:9 ;
(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 3
.= f + (((0. K) + (- L1)) * (id V1)) by VECTSP_1:19
.= f + ((- L1) * (id V1)) by RLVECT_1:def 4 ;
then 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 A24, 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 A35, A37, FUNCT_1:13
.= ((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 A38, Lm7
.= (0. V1) + (((power K) . ((L2 - L1),n)) * (((f + ((- L2) * (id V1))) |^ M1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2))) by A42, A39, MATRLIN:def 3
.= ((power K) . ((L2 - L1),n)) * (((f + ((- L2) * (id V1))) |^ M1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2)) by RLVECT_1:def 4 ;
then ((f + ((- L2) * (id V1))) |^ M1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) = 0. V1 by A40, VECTSP_1:15;
then M1 + 1 <= M1 by A32;
hence contradiction by NAT_1:13; :: thesis: verum
end;
v is eigenvector of f,L2 by A1, A3, A5, 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 A7;
A43: ( 0. V1 = 0. I & L2 * v = L2 * vI ) by VECTSP_4:11, VECTSP_4:14;
A44: f . v = fI . vI by A6, FUNCT_1:49;
hence A45: fI is with_eigenvalues by A4, A5, A43; :: 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
A46: w <> 0. I and
A47: fI . w = L1 * w by A45, Def2;
w = 0. V1 by A6, A47, Th37;
hence contradiction by A46, VECTSP_4:11; :: thesis: verum
end;
hence ( L1 is not eigenvalue of fI & L2 is eigenvalue of fI ) by A4, A5, A43, A44, A45, 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 object ; :: 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 x in the carrier of (UnionKers (f + ((- L2) * (id V1)))) ; :: thesis: x in the carrier of I
then A48: x in UnionKers (f + ((- L2) * (id V1))) ;
then x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 ;
v is Vector of I by A7, A48;
hence x in the carrier of I ; :: thesis: verum
end;
hence UnionKers (f + ((- L2) * (id V1))) is Subspace of I by VECTSP_4:27; :: thesis: verum