# 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 ${⊢}{T}:ℋ⟶ℋ\to \left({A}\in \mathrm{eigvec}\left({T}\right)↔\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\wedge \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 eigvecval ${⊢}{T}:ℋ⟶ℋ\to \mathrm{eigvec}\left({T}\right)=\left\{{y}\in \left(ℋ\setminus {0}_{ℋ}\right)|\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({y}\right)={x}{\cdot }_{ℎ}{y}\right\}$
2 1 eleq2d ${⊢}{T}:ℋ⟶ℋ\to \left({A}\in \mathrm{eigvec}\left({T}\right)↔{A}\in \left\{{y}\in \left(ℋ\setminus {0}_{ℋ}\right)|\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({y}\right)={x}{\cdot }_{ℎ}{y}\right\}\right)$
3 eldif ${⊢}{A}\in \left(ℋ\setminus {0}_{ℋ}\right)↔\left({A}\in ℋ\wedge ¬{A}\in {0}_{ℋ}\right)$
4 elch0 ${⊢}{A}\in {0}_{ℋ}↔{A}={0}_{ℎ}$
5 4 necon3bbii ${⊢}¬{A}\in {0}_{ℋ}↔{A}\ne {0}_{ℎ}$
6 5 anbi2i ${⊢}\left({A}\in ℋ\wedge ¬{A}\in {0}_{ℋ}\right)↔\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)$
7 3 6 bitri ${⊢}{A}\in \left(ℋ\setminus {0}_{ℋ}\right)↔\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)$
8 7 anbi1i ${⊢}\left({A}\in \left(ℋ\setminus {0}_{ℋ}\right)\wedge \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)↔\left(\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\wedge \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)$
9 fveq2 ${⊢}{y}={A}\to {T}\left({y}\right)={T}\left({A}\right)$
10 oveq2 ${⊢}{y}={A}\to {x}{\cdot }_{ℎ}{y}={x}{\cdot }_{ℎ}{A}$
11 9 10 eqeq12d ${⊢}{y}={A}\to \left({T}\left({y}\right)={x}{\cdot }_{ℎ}{y}↔{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)$
12 11 rexbidv ${⊢}{y}={A}\to \left(\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({y}\right)={x}{\cdot }_{ℎ}{y}↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)$
13 12 elrab ${⊢}{A}\in \left\{{y}\in \left(ℋ\setminus {0}_{ℋ}\right)|\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({y}\right)={x}{\cdot }_{ℎ}{y}\right\}↔\left({A}\in \left(ℋ\setminus {0}_{ℋ}\right)\wedge \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)$
14 df-3an ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\wedge \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)↔\left(\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\wedge \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)$
15 8 13 14 3bitr4i ${⊢}{A}\in \left\{{y}\in \left(ℋ\setminus {0}_{ℋ}\right)|\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({y}\right)={x}{\cdot }_{ℎ}{y}\right\}↔\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\wedge \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)$
16 2 15 syl6bb ${⊢}{T}:ℋ⟶ℋ\to \left({A}\in \mathrm{eigvec}\left({T}\right)↔\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\wedge \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)\right)$