Definition df-eigvec

Description: Define the eigenvector function. Theorem eleigveccl shows that eigvecT , the set of eigenvectors of Hilbert space operator T , are Hilbert space vectors. (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	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 z\in ℂt\left(x\right)=z{\cdot }_{ℎ}x\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cei	$$class\mathrm{eigvec}$$
1		vt	$$setvart$$
2		chba	$$class\mathscr{H}$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4	2 2 3	co	$$class\left({\mathscr{H}}^{\mathscr{H}}\right)$$
5		vx	$$setvarx$$
6		c0h	$$class{0}_{\mathscr{H}}$$
7	2 6	cdif	$$class\left(\mathscr{H}\setminus 0_{\mathscr{H}}\right)$$
8		vz	$$setvarz$$
9		cc	$$classℂ$$
10	1	cv	$$setvart$$
11	5	cv	$$setvarx$$
12	11 10	cfv	$$classt\left(x\right)$$
13	8	cv	$$setvarz$$
14		csm	$$class{\cdot }_{ℎ}$$
15	13 11 14	co	$$class\left(z{\cdot }_{ℎ}x\right)$$
16	12 15	wceq	$$wfft\left(x\right)=z{\cdot }_{ℎ}x$$
17	16 8 9	wrex	$$wff\exists z\in ℂt\left(x\right)=z{\cdot }_{ℎ}x$$
18	17 5 7	crab	$$class\left\{x\in \left(\mathscr{H}\setminus 0_{\mathscr{H}}\right)|\exists z\in ℂt\left(x\right)=z{\cdot }_{ℎ}x\right\}$$
19	1 4 18	cmpt	$$class\left(t\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left\{x\in \left(\mathscr{H}\setminus 0_{\mathscr{H}}\right)|\exists z\in ℂt\left(x\right)=z{\cdot }_{ℎ}x\right\}\right)$$
20	0 19	wceq	$$wff\mathrm{eigvec}=\left(t\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left\{x\in \left(\mathscr{H}\setminus 0_{\mathscr{H}}\right)|\exists z\in ℂt\left(x\right)=z{\cdot }_{ℎ}x\right\}\right)$$