Metamath Proof Explorer


Theorem eleigvec

Description: Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion eleigvec ( 𝑇 : ℋ ⟶ ℋ → ( 𝐴 ∈ ( eigvec ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0 ∧ ∃ 𝑥 ∈ ℂ ( 𝑇𝐴 ) = ( 𝑥 · 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 eigvecval ( 𝑇 : ℋ ⟶ ℋ → ( eigvec ‘ 𝑇 ) = { 𝑦 ∈ ( ℋ ∖ 0 ) ∣ ∃ 𝑥 ∈ ℂ ( 𝑇𝑦 ) = ( 𝑥 · 𝑦 ) } )
2 1 eleq2d ( 𝑇 : ℋ ⟶ ℋ → ( 𝐴 ∈ ( eigvec ‘ 𝑇 ) ↔ 𝐴 ∈ { 𝑦 ∈ ( ℋ ∖ 0 ) ∣ ∃ 𝑥 ∈ ℂ ( 𝑇𝑦 ) = ( 𝑥 · 𝑦 ) } ) )
3 eldif ( 𝐴 ∈ ( ℋ ∖ 0 ) ↔ ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 ∈ 0 ) )
4 elch0 ( 𝐴 ∈ 0𝐴 = 0 )
5 4 necon3bbii ( ¬ 𝐴 ∈ 0𝐴 ≠ 0 )
6 5 anbi2i ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 ∈ 0 ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0 ) )
7 3 6 bitri ( 𝐴 ∈ ( ℋ ∖ 0 ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0 ) )
8 7 anbi1i ( ( 𝐴 ∈ ( ℋ ∖ 0 ) ∧ ∃ 𝑥 ∈ ℂ ( 𝑇𝐴 ) = ( 𝑥 · 𝐴 ) ) ↔ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0 ) ∧ ∃ 𝑥 ∈ ℂ ( 𝑇𝐴 ) = ( 𝑥 · 𝐴 ) ) )
9 fveq2 ( 𝑦 = 𝐴 → ( 𝑇𝑦 ) = ( 𝑇𝐴 ) )
10 oveq2 ( 𝑦 = 𝐴 → ( 𝑥 · 𝑦 ) = ( 𝑥 · 𝐴 ) )
11 9 10 eqeq12d ( 𝑦 = 𝐴 → ( ( 𝑇𝑦 ) = ( 𝑥 · 𝑦 ) ↔ ( 𝑇𝐴 ) = ( 𝑥 · 𝐴 ) ) )
12 11 rexbidv ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ ℂ ( 𝑇𝑦 ) = ( 𝑥 · 𝑦 ) ↔ ∃ 𝑥 ∈ ℂ ( 𝑇𝐴 ) = ( 𝑥 · 𝐴 ) ) )
13 12 elrab ( 𝐴 ∈ { 𝑦 ∈ ( ℋ ∖ 0 ) ∣ ∃ 𝑥 ∈ ℂ ( 𝑇𝑦 ) = ( 𝑥 · 𝑦 ) } ↔ ( 𝐴 ∈ ( ℋ ∖ 0 ) ∧ ∃ 𝑥 ∈ ℂ ( 𝑇𝐴 ) = ( 𝑥 · 𝐴 ) ) )
14 df-3an ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0 ∧ ∃ 𝑥 ∈ ℂ ( 𝑇𝐴 ) = ( 𝑥 · 𝐴 ) ) ↔ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0 ) ∧ ∃ 𝑥 ∈ ℂ ( 𝑇𝐴 ) = ( 𝑥 · 𝐴 ) ) )
15 8 13 14 3bitr4i ( 𝐴 ∈ { 𝑦 ∈ ( ℋ ∖ 0 ) ∣ ∃ 𝑥 ∈ ℂ ( 𝑇𝑦 ) = ( 𝑥 · 𝑦 ) } ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0 ∧ ∃ 𝑥 ∈ ℂ ( 𝑇𝐴 ) = ( 𝑥 · 𝐴 ) ) )
16 2 15 bitrdi ( 𝑇 : ℋ ⟶ ℋ → ( 𝐴 ∈ ( eigvec ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0 ∧ ∃ 𝑥 ∈ ℂ ( 𝑇𝐴 ) = ( 𝑥 · 𝐴 ) ) ) )