Theorem eigvec1

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

	Ref	Expression
Assertion	eigvec1	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( 𝑇 ‘ 𝐴 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) ∧ 𝐴 ≠ 0ℎ ) )

Proof

Step	Hyp	Ref	Expression
1		eigvalval	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) = ( ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) )
2	1	oveq1d	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) = ( ( ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) ·ℎ 𝐴 ) )
3		eleigvec2	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝐴 ∈ ( eigvec ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) ) )
4	3	biimpa	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) )
5		normcan	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) → ( ( ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) ·ℎ 𝐴 ) = ( 𝑇 ‘ 𝐴 ) )
6	4 5	syl	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) ·ℎ 𝐴 ) = ( 𝑇 ‘ 𝐴 ) )
7	2 6	eqtr2d	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( 𝑇 ‘ 𝐴 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) )
8	4	simp2d	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → 𝐴 ≠ 0ℎ )
9	7 8	jca	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( 𝑇 ‘ 𝐴 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) ∧ 𝐴 ≠ 0ℎ ) )