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

Metamath Proof Explorer

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 ‘ { 𝐴 } ) ) ) )