# 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 ${⊢}{T}:ℋ⟶ℋ\to \left({A}\in \mathrm{eigvec}\left({T}\right)↔\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\wedge {T}\left({A}\right)\in \mathrm{span}\left(\left\{{A}\right\}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 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)$
2 elspansn ${⊢}{A}\in ℋ\to \left({T}\left({A}\right)\in \mathrm{span}\left(\left\{{A}\right\}\right)↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)$
3 2 adantr ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \left({T}\left({A}\right)\in \mathrm{span}\left(\left\{{A}\right\}\right)↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)$
4 3 pm5.32i ${⊢}\left(\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\wedge {T}\left({A}\right)\in \mathrm{span}\left(\left\{{A}\right\}\right)\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)$
5 df-3an ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\wedge {T}\left({A}\right)\in \mathrm{span}\left(\left\{{A}\right\}\right)\right)↔\left(\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\wedge {T}\left({A}\right)\in \mathrm{span}\left(\left\{{A}\right\}\right)\right)$
6 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)$
7 4 5 6 3bitr4i ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\wedge {T}\left({A}\right)\in \mathrm{span}\left(\left\{{A}\right\}\right)\right)↔\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\wedge \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({A}\right)={x}{\cdot }_{ℎ}{A}\right)$
8 1 7 syl6bbr ${⊢}{T}:ℋ⟶ℋ\to \left({A}\in \mathrm{eigvec}\left({T}\right)↔\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\wedge {T}\left({A}\right)\in \mathrm{span}\left(\left\{{A}\right\}\right)\right)\right)$