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	⊢ eigval = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ( eigvec ‘ 𝑡 ) ↦ ( ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cel	⊢ eigval
1		vt	⊢ 𝑡
2		chba	⊢ ℋ
3		cmap	⊢ ↑m
4	2 2 3	co	⊢ ( ℋ ↑m ℋ )
5		vx	⊢ 𝑥
6		cei	⊢ eigvec
7	1	cv	⊢ 𝑡
8	7 6	cfv	⊢ ( eigvec ‘ 𝑡 )
9	5	cv	⊢ 𝑥
10	9 7	cfv	⊢ ( 𝑡 ‘ 𝑥 )
11		csp	⊢ ·ih
12	10 9 11	co	⊢ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑥 )
13		cdiv	⊢ /
14		cno	⊢ normℎ
15	9 14	cfv	⊢ ( normℎ ‘ 𝑥 )
16		cexp	⊢ ↑
17		c2	⊢ 2
18	15 17 16	co	⊢ ( ( normℎ ‘ 𝑥 ) ↑ 2 )
19	12 18 13	co	⊢ ( ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) )
20	5 8 19	cmpt	⊢ ( 𝑥 ∈ ( eigvec ‘ 𝑡 ) ↦ ( ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) )
21	1 4 20	cmpt	⊢ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ( eigvec ‘ 𝑡 ) ↦ ( ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) )
22	0 21	wceq	⊢ eigval = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ( eigvec ‘ 𝑡 ) ↦ ( ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) )