Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
Operators on Hilbert spaces
Linear, continuous, bounded, Hermitian, unitary operators and norms
df-eigval
Metamath Proof Explorer
Description: Define the eigenvalue function. The range of eigval T is the set
of eigenvalues of Hilbert space operator T . Theorem eigvalcl shows that ( eigval T ) 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 ) ) ) )