Definition df-eigval

Description: Define the eigenvalue function. The range of eigvalT is the set of eigenvalues of Hilbert space operator T . Theorem eigvalcl shows that ( eigvalT )A , the eigenvalue associated with eigenvector A , is a complex number. (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-eigval	$$⊢\mathrm{eigval}=\left(t\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left(x\in \mathrm{eigvec}\left(t\right)⟼\frac{t\left(x\right){\cdot }_{\mathrm{ih}}x}{{{norm}_{ℎ}\left(x\right)}^2}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cel	$$class\mathrm{eigval}$$
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		cei	$$class\mathrm{eigvec}$$
7	1	cv	$$setvart$$
8	7 6	cfv	$$class\mathrm{eigvec}\left(t\right)$$
9	5	cv	$$setvarx$$
10	9 7	cfv	$$classt\left(x\right)$$
11		csp	$$class{\cdot }_{\mathrm{ih}}$$
12	10 9 11	co	$$class\left(t\left(x\right){\cdot }_{\mathrm{ih}}x\right)$$
13		cdiv	$$class÷$$
14		cno	$$class{norm}_{ℎ}$$
15	9 14	cfv	$$class{norm}_{ℎ}\left(x\right)$$
16		cexp	$$class^$$
17		c2	$$class2$$
18	15 17 16	co	$$class{{norm}_{ℎ}\left(x\right)}^2$$
19	12 18 13	co	$$class\left(\frac{t\left(x\right){\cdot }_{\mathrm{ih}}x}{{{norm}_{ℎ}\left(x\right)}^2}\right)$$
20	5 8 19	cmpt	$$class\left(x\in \mathrm{eigvec}\left(t\right)⟼\frac{t\left(x\right){\cdot }_{\mathrm{ih}}x}{{{norm}_{ℎ}\left(x\right)}^2}\right)$$
21	1 4 20	cmpt	$$class\left(t\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left(x\in \mathrm{eigvec}\left(t\right)⟼\frac{t\left(x\right){\cdot }_{\mathrm{ih}}x}{{{norm}_{ℎ}\left(x\right)}^2}\right)\right)$$
22	0 21	wceq	$$wff\mathrm{eigval}=\left(t\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left(x\in \mathrm{eigvec}\left(t\right)⟼\frac{t\left(x\right){\cdot }_{\mathrm{ih}}x}{{{norm}_{ℎ}\left(x\right)}^2}\right)\right)$$