Metamath Proof Explorer


Definition df-eigvec

Description: Define the eigenvector function. Theorem eleigveccl shows that eigvecT , 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 ) ∣ ∃ 𝑧 ∈ ℂ ( 𝑡𝑥 ) = ( 𝑧 · 𝑥 ) } )