Theorem eleigvec2

Description: Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 18-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	eleigvec2	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝐴 ∈ ( eigvec ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleigvec	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝐴 ∈ ( eigvec ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) ) )
2		elspansn	⊢ ( 𝐴 ∈ ℋ → ( ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ↔ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) )
3	2	adantr	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ↔ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) )
4	3	pm5.32i	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) ↔ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) )
5		df-3an	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) ↔ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) )
6		df-3an	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) ↔ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) )
7	4 5 6	3bitr4i	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) )
8	1 7	bitr4di	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝐴 ∈ ( eigvec ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) ) )