Theorem eigvecval

Description: 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	eigvecval	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \mathrm{eigvec}\left(T\right)=\left\{x\in \left(\mathscr{H}\setminus 0_{\mathscr{H}}\right)|\exists y\in ℂT\left(x\right)=y{\cdot }_{ℎ}x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
2		difexg	$$⊢\mathscr{H}\in \mathrm{V}\to \mathscr{H}\setminus 0_{\mathscr{H}}\in \mathrm{V}$$
3	1 2	ax-mp	$$⊢\mathscr{H}\setminus 0_{\mathscr{H}}\in \mathrm{V}$$
4	3	rabex	$$⊢\left\{x\in \left(\mathscr{H}\setminus 0_{\mathscr{H}}\right)|\exists y\in ℂT\left(x\right)=y{\cdot }_{ℎ}x\right\}\in \mathrm{V}$$
5		fveq1	$$⊢t=T\to t\left(x\right)=T\left(x\right)$$
6	5	eqeq1d	$$⊢t=T\to \left(t\left(x\right)=y{\cdot }_{ℎ}x\leftrightarrow T\left(x\right)=y{\cdot }_{ℎ}x\right)$$
7	6	rexbidv	$$⊢t=T\to \left(\exists y\in ℂt\left(x\right)=y{\cdot }_{ℎ}x\leftrightarrow \exists y\in ℂT\left(x\right)=y{\cdot }_{ℎ}x\right)$$
8	7	rabbidv	$$⊢t=T\to \left\{x\in \left(\mathscr{H}\setminus 0_{\mathscr{H}}\right)|\exists y\in ℂt\left(x\right)=y{\cdot }_{ℎ}x\right\}=\left\{x\in \left(\mathscr{H}\setminus 0_{\mathscr{H}}\right)|\exists y\in ℂT\left(x\right)=y{\cdot }_{ℎ}x\right\}$$
9		df-eigvec	$$⊢\mathrm{eigvec}=\left(t\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left\{x\in \left(\mathscr{H}\setminus 0_{\mathscr{H}}\right)|\exists y\in ℂt\left(x\right)=y{\cdot }_{ℎ}x\right\}\right)$$
10	4 1 1 8 9	fvmptmap	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \mathrm{eigvec}\left(T\right)=\left\{x\in \left(\mathscr{H}\setminus 0_{\mathscr{H}}\right)|\exists y\in ℂT\left(x\right)=y{\cdot }_{ℎ}x\right\}$$