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	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( 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_ℎ ) )