Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
Operators on Hilbert spaces
Linear, continuous, bounded, Hermitian, unitary operators and norms
df-eigvec
Metamath Proof Explorer
Description: Define the eigenvector function. Theorem eleigveccl shows that
eigvec T , the set of eigenvectors of Hilbert space operator
T , are Hilbert space vectors. (Contributed by NM , 11-Mar-2006)
(New usage is discouraged.)
Ref
Expression
Assertion
df-eigvec
⊢ eigvec = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑧 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 · ℎ 𝑥 ) } )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cei
⊢ eigvec
1
vt
⊢ 𝑡
2
chba
⊢ ℋ
3
cmap
⊢ ↑m
4
2 2 3
co
⊢ ( ℋ ↑m ℋ )
5
vx
⊢ 𝑥
6
c0h
⊢ 0ℋ
7
2 6
cdif
⊢ ( ℋ ∖ 0ℋ )
8
vz
⊢ 𝑧
9
cc
⊢ ℂ
10
1
cv
⊢ 𝑡
11
5
cv
⊢ 𝑥
12
11 10
cfv
⊢ ( 𝑡 ‘ 𝑥 )
13
8
cv
⊢ 𝑧
14
csm
⊢ · ℎ
15
13 11 14
co
⊢ ( 𝑧 · ℎ 𝑥 )
16
12 15
wceq
⊢ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 · ℎ 𝑥 )
17
16 8 9
wrex
⊢ ∃ 𝑧 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 · ℎ 𝑥 )
18
17 5 7
crab
⊢ { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑧 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 · ℎ 𝑥 ) }
19
1 4 18
cmpt
⊢ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑧 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 · ℎ 𝑥 ) } )
20
0 19
wceq
⊢ eigvec = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑧 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 · ℎ 𝑥 ) } )