Metamath Proof Explorer

Theorem eigvec1

Description: Property of an eigenvector. (Contributed by NM, 12-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eigvec1 ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→T⁡A=eigval⁡T⁡A⋅ℎA∧A≠0ℎ

Proof

Step Hyp Ref Expression
1 eigvalval ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→eigval⁡T⁡A=T⁡A⋅ihAnormℎ⁡A2
2 1 oveq1d ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→eigval⁡T⁡A⋅ℎA=T⁡A⋅ihAnormℎ⁡A2⋅ℎA
3 eleigvec2 ⊢T:ℋ⟶ℋ→A∈eigvec⁡T↔A∈ℋ∧A≠0ℎ∧T⁡A∈span⁡A
4 3 biimpa ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→A∈ℋ∧A≠0ℎ∧T⁡A∈span⁡A
5 normcan ⊢A∈ℋ∧A≠0ℎ∧T⁡A∈span⁡A→T⁡A⋅ihAnormℎ⁡A2⋅ℎA=T⁡A
6 4 5 syl ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→T⁡A⋅ihAnormℎ⁡A2⋅ℎA=T⁡A
7 2 6 eqtr2d ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→T⁡A=eigval⁡T⁡A⋅ℎA
8 4 simp2d ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→A≠0ℎ
9 7 8 jca ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→T⁡A=eigval⁡T⁡A⋅ℎA∧A≠0ℎ