This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database COMPLEX HILBERT SPACE EXPLORER (DEPRECATED) Operators on Hilbert spaces Linear, continuous, bounded, Hermitian, unitary operators and norms df-eigval
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 ) ) ) )