This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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ℋ ) ∣ ∃ 𝑧 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 ·ℎ 𝑥 ) } )