Metamath Proof Explorer


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 ) ) ) )