:: Eigenvalues of a Linear Transformation
:: by Karol P\c{a}k
::
:: Received July 11, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

theorem Th1: :: VECTSP11:1
for n, m being Nat
for K being Field
for A, B being Matrix of K
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
Segm ((A + B),nt,mt) = (Segm (A,nt,mt)) + (Segm (B,nt,mt))
proofend;

theorem Th2: :: VECTSP11:2
for n being Nat
for K being Field
for P being finite without_zero Subset of NAT st P c= Seg n holds
Segm ((1. (K,n)),P,P) = 1. (K,(card P))
proofend;

theorem Th3: :: VECTSP11:3
for K being Field
for A, B being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A holds
Segm ((A + B),P,Q) = (Segm (A,P,Q)) + (Segm (B,P,Q))
proofend;

theorem Th4: :: VECTSP11:4
for n, i, j being Nat
for K being Field
for A, B being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j))
proofend;

theorem Th5: :: VECTSP11:5
for n, i, j being Nat
for K being Field
for a being Element of K
for A being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((a * A),i,j) = a * (Delete (A,i,j))
proofend;

theorem Th6: :: VECTSP11:6
for i, n being Nat
for K being Field st i in Seg n holds
Delete ((1. (K,n)),i,i) = 1. (K,(n -' 1))
proofend;

theorem Th7: :: VECTSP11:7
for n being Nat
for K being Field
for A, B being Matrix of n,K ex P being Polynomial of K st
( len P <= n + 1 &amp; ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) )
proofend;

:: The Characteristic Polynomials of Square Matrixs
theorem Th8: :: VECTSP11:8
for n being Nat
for K being Field
for A being Matrix of n,K ex P being Polynomial of K st
( len P = n + 1 &amp; ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,n)))) ) )
proofend;

Lm1:  for K being Field
for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2
for W1 being Subspace of V1
for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
proofend;

registration
let K be Field;
cluster non empty non trivial right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finite-dimensional for VectSpStr over K;
existence
 ex b1 being VectSp of K st
( not b1 is trivial &amp; b1 is finite-dimensional )
proofend;
end;

begin

definition
let R be non empty doubleLoopStr ;
let V be non empty VectSpStr over R;
let IT be Function of V,V;
attrIT is with_eigenvalues  means :Def1: :: VECTSP11:def 1
 ex v being Vector of V ex a being Scalar of R st
( v <> 0. V &amp; IT . v = a * v );
end;

:: deftheorem Def1 defines with_eigenvalues VECTSP11:def_1_:_
 for R being non empty doubleLoopStr
for V being non empty VectSpStr over R
for IT being Function of V,V holds
( IT is with_eigenvalues iff ex v being Vector of V ex a being Scalar of R st
( v <> 0. V &amp; IT . v = a * v ) );

Lm2:  for K being Field
for V being non trivial VectSp of K holds
( id V is with_eigenvalues &amp; ex v being Vector of V st
( v <> 0. V &amp; (id V) . v = (1_ K) * v ) )
proofend;

registration
let K be Field;
let V be non trivial VectSp of K;
cluster Relation-like the carrier of V -defined the carrier of V -valued Function-like non empty total quasi_total additive homogeneous with_eigenvalues for Element of bool [: the carrier of V, the carrier of V:];
existence
 ex b1 being linear-transformation of V,V st b1 is with_eigenvalues
proofend;
end;

definition
let R be non empty doubleLoopStr ;
let V be non empty VectSpStr over R;
let f be Function of V,V;
assume A1: f is with_eigenvalues ;
mode eigenvalue of f ->  Element of R means :Def2: :: VECTSP11:def 2
 ex v being Vector of V st
( v <> 0. V &amp; f . v = it * v );
existence
 ex b1 being Element of R ex v being Vector of V st
( v <> 0. V &amp; f . v = b1 * v )
proofend;
end;

:: deftheorem Def2 defines eigenvalue VECTSP11:def_2_:_
 for R being non empty doubleLoopStr
for V being non empty VectSpStr over R
for f being Function of V,V st f is with_eigenvalues holds
for b4 being Element of R holds
( b4 is eigenvalue of f iff ex v being Vector of V st
( v <> 0. V &amp; f . v = b4 * v ) );

definition
let R be non empty doubleLoopStr ;
let V be non empty VectSpStr over R;
let f be Function of V,V;
let L be Scalar of R;
assume A1: ( f is with_eigenvalues &amp; L is eigenvalue of f ) ;
mode eigenvector of f,L ->  Vector of V means :Def3: :: VECTSP11:def 3
f . it = L * it;
existence
 ex b1 being Vector of V st f . b1 = L * b1
proofend;
end;

:: deftheorem Def3 defines eigenvector VECTSP11:def_3_:_
 for R being non empty doubleLoopStr
for V being non empty VectSpStr over R
for f being Function of V,V
for L being Scalar of R st f is with_eigenvalues &amp; L is eigenvalue of f holds
for b5 being Vector of V holds
( b5 is eigenvector of f,L iff f . b5 = L * b5 );

theorem :: VECTSP11:9
for K being Field
for V being non trivial VectSp of K
for w being Vector of V
for a being Element of K st a <> 0. K holds
for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues &amp; a * L is eigenvalue of a * f &amp; ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) &amp; ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
proofend;

theorem :: VECTSP11:10
for K being Field
for V being non trivial VectSp of K
for f1, f2 being with_eigenvalues Function of V,V
for L1, L2 being Scalar of K st L1 is eigenvalue of f1 &amp; L2 is eigenvalue of f2 &amp; ex v being Vector of V st
( v is eigenvector of f1,L1 &amp; v is eigenvector of f2,L2 &amp; v <> 0. V ) holds
( f1 + f2 is with_eigenvalues &amp; L1 + L2 is eigenvalue of f1 + f2 &amp; ( for w being Vector of V st w is eigenvector of f1,L1 &amp; w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )
proofend;

theorem Th11: :: VECTSP11:11
for K being Field
for V being non trivial VectSp of K holds
( id V is with_eigenvalues &amp; 1_ K is eigenvalue of id V &amp; ( for v being Vector of V holds v is eigenvector of id V, 1_ K ) )
proofend;

theorem :: VECTSP11:12
for K being Field
for V being non trivial VectSp of K
for L being eigenvalue of id V holds L = 1_ K
proofend;

theorem :: VECTSP11:13
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 st not ker f is trivial holds
( f is with_eigenvalues &amp; 0. K is eigenvalue of f )
proofend;

theorem Th14: :: VECTSP11:14
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds
( ( f is with_eigenvalues &amp; L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )
proofend;

theorem Th15: :: VECTSP11:15
for K being Field
for L being Scalar of K
for V1 being finite-dimensional VectSp of K
for b1, b19 being OrdBasis of V1
for f being linear-transformation of V1,V1 holds
( ( f is with_eigenvalues &amp; L is eigenvalue of f ) iff Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K )
proofend;

theorem :: VECTSP11:16
for K being 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
proofend;

theorem Th17: :: VECTSP11:17
for K being Field
for V1 being VectSp of K
for v1 being Vector of V1
for f being linear-transformation of V1,V1
for L being Scalar of K st f is with_eigenvalues &amp; L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
proofend;

definition
let S be 1-sorted ;
let F be Function of S,S;
let n be Nat;
funcF |^ n ->  Function of S,S means :Def4: :: VECTSP11:def 4
 for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
it = Product (n |-> F9);
existence
 ex b1 being Function of S,S st
for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b1 = Product (n |-> F9)
proofend;
uniqueness
 for b1, b2 being Function of S,S st ( for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b1 = Product (n |-> F9) ) &amp; ( for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b2 = Product (n |-> F9) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines |^ VECTSP11:def_4_:_
 for S being 1-sorted
for F being Function of S,S
for n being Nat
for b4 being Function of S,S holds
( b4 = F |^ n iff for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b4 = Product (n |-> F9) );

theorem Th18: :: VECTSP11:18
for S being 1-sorted
for F being Function of S,S holds F |^ 0 = id S
proofend;

theorem Th19: :: VECTSP11:19
for S being 1-sorted
for F being Function of S,S holds F |^ 1 = F
proofend;

theorem Th20: :: VECTSP11:20
for i, j being Nat
for S being 1-sorted
for F being Function of S,S holds F |^ (i + j) = (F |^ j) * (F |^ i)
proofend;

theorem :: VECTSP11:21
for i being Nat
for S being 1-sorted
for F being Function of S,S
for s1, s2 being Element of S
for n, m being Nat st (F |^ m) . s1 = s2 &amp; (F |^ n) . s2 = s2 holds
(F |^ (m + (i * n))) . s1 = s2
proofend;

theorem :: VECTSP11:22
for n being Nat
for K being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V1 being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
for W being Subspace of V1
for f being Function of V1,V1
for fW being Function of W,W st fW = f | W holds
(f |^ n) | W = fW |^ n
proofend;

registration
let K be Field;
let V1 be VectSp of K;
let f be linear-transformation of V1,V1;
let n be Nat;
clusterf |^ n ->  additive homogeneous ;
coherence
 ( f |^ n is homogeneous &amp; f |^ n is additive )
proofend;
end;

theorem Th23: :: VECTSP11:23
for i, j being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds
(f |^ (i + j)) . v1 = 0. V1
proofend;

begin

definition
let K be Field;
let V1 be VectSp of K;
let f be linear-transformation of V1,V1;
func UnionKers f ->  strict Subspace of V1 means :Def5: :: VECTSP11:def 5
 the carrier of it =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  ;
existence
 ex b1 being strict Subspace of V1 st the carrier of b1 =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }
proofend;
uniqueness
 for b1, b2 being strict Subspace of V1 st the carrier of b1 =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  &amp; the carrier of b2 =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def5 defines UnionKers VECTSP11:def_5_:_
 for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for b4 being strict Subspace of V1 holds
( b4 = UnionKers f iff the carrier of b4 =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  );

theorem Th24: :: VECTSP11:24
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for v1 being Vector of V1 holds
( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )
proofend;

theorem Th25: :: VECTSP11:25
for i being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of UnionKers f
proofend;

theorem Th26: :: VECTSP11:26
for i, j being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of ker (f |^ (i + j))
proofend;

theorem :: VECTSP11:27
for K being Field
for V being finite-dimensional VectSp of K
for f being linear-transformation of V,V ex n being Nat st UnionKers f = ker (f |^ n)
proofend;

theorem Th28: :: VECTSP11:28
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))
proofend;

theorem :: VECTSP11:29
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (ker ((f + (L * (id V1))) |^ n)) is linear-transformation of (ker ((f + (L * (id V1))) |^ n)),(ker ((f + (L * (id V1))) |^ n))
proofend;

theorem Th30: :: VECTSP11:30
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f)
proofend;

theorem Th31: :: VECTSP11:31
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))
proofend;

theorem Th32: :: VECTSP11:32
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))
proofend;

theorem :: VECTSP11:33
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))
proofend;

theorem Th34: :: VECTSP11:34
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 st UnionKers f = ker (f |^ n) holds
(ker (f |^ n)) /\ (im (f |^ n)) = (0). V1
proofend;

theorem :: VECTSP11:35
for K being Field
for V being finite-dimensional VectSp of K
for f being linear-transformation of V,V
for n being Nat st UnionKers f = ker (f |^ n) holds
V is_the_direct_sum_of ker (f |^ n), im (f |^ n)
proofend;

theorem Th36: :: VECTSP11:36
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for I being Linear_Compl of UnionKers f holds f | I is one-to-one
proofend;

theorem Th37: :: VECTSP11:37
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K
for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
proofend;

Lm3:  for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a * b) * f = a * (b * f)
proofend;

Lm4:  for K being Field
for V1 being VectSp of K
for L being Scalar of K
for f, g being Function of V1,V1 holds L * (f * g) = (L * f) * g
proofend;

Lm5:  for K being Field
for V1 being VectSp of K
for L being Scalar of K
for f, g being Function of V1,V1 st f is additive &amp; f is homogeneous holds
L * (f * g) = f * (L * g)
proofend;

Lm6:  for K being Field
for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 holds (f1 + f2) * g = (f1 * g) + (f2 * g)
proofend;

Lm7:  for K being Field
for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 st g is additive &amp; g is homogeneous holds
g * (f1 + f2) = (g * f1) + (g * f2)
proofend;

Lm8:  for K being Field
for V1 being VectSp of K
for f1, f2, f3 being Function of V1,V1 holds (f1 + f2) + f3 = f1 + (f2 + f3)
proofend;

Lm9:  for n being Nat
for K being Field
for V1 being VectSp of K
for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
proofend;

Lm10:  for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a + b) * f = (a * f) + (b * f)
proofend;

theorem Th38: :: VECTSP11:38
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K st n >= 1 holds
ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) &amp; ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )
proofend;

theorem :: VECTSP11:39
for K being Field
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 &amp; L1 <> L2 &amp; 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 &amp; L1 is not eigenvalue of fI &amp; L2 is eigenvalue of fI &amp; UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
proofend;

:: Main Lemmas for Expansion of Matrices of Nilpotent Linear Transformations
theorem :: VECTSP11:40
for K being Field
for V1 being VectSp of K
for U being finite Subset of V1 st U is linearly-independent holds
for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) &amp; (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
proofend;

theorem Th41: :: VECTSP11:41
for K being Field
for V1, V2 being VectSp of K
for A being Subset of V1
for L being Linear_Combination of V2
for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds
ex M being Linear_Combination of A st f . (Sum M) = Sum L
proofend;

theorem :: VECTSP11:42
for K being Field
for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2
for A being Subset of V1
for B being Subset of V2 st f .: A = B holds
f .: the carrier of (Lin A) = the carrier of (Lin B)
proofend;

theorem Th43: :: VECTSP11:43
for K being Field
for V1, V2 being VectSp of K
for L being Linear_Combination of V1
for F being FinSequence of V1
for f being linear-transformation of V1,V2 st f | ((Carrier L) /\ (rng F)) is one-to-one &amp; rng F c= Carrier L holds
ex Lf being Linear_Combination of V2 st
( Carrier Lf = f .: ((Carrier L) /\ (rng F)) &amp; f * (L (#) F) = Lf (#) (f * F) &amp; ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1) ) )
proofend;

theorem :: VECTSP11:44
for K being Field
for V1, V2 being VectSp of K
for A, B being Subset of V1
for L being Linear_Combination of V1 st Carrier L c= A \/ B &amp; Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one &amp; f .: B is linearly-independent Subset of V2 &amp; f .: A c= {(0. V2)} holds
Carrier L c= A
proofend;