This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⋅ ih A norm ℎ ⁡ A 2
2 1 oveq1d ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → eigval ⁡ T ⁡ A ⋅ ℎ A = T ⁡ A ⋅ ih A norm ℎ ⁡ A 2 ⋅ ℎ 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 ⋅ ih A norm ℎ ⁡ A 2 ⋅ ℎ A = T ⁡ A
6 4 5 syl ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → T ⁡ A ⋅ ih A norm ℎ ⁡ A 2 ⋅ ℎ 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 ℎ