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

Metamath Proof Explorer

Theorem eigvecval

Description: The set of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion eigvecval ( 𝑇 : ℋ ⟶ ℋ → ( eigvec ‘ 𝑇 ) = { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑦 ∈ ℂ ( 𝑇 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ ℋ ∈ V
2 difexg ⊢ ( ℋ ∈ V → ( ℋ ∖ 0ℋ ) ∈ V )
3 1 2 ax-mp ⊢ ( ℋ ∖ 0ℋ ) ∈ V
4 3 rabex ⊢ { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑦 ∈ ℂ ( 𝑇 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) } ∈ V
5 fveq1 ⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
6 5 eqeq1d ⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) ↔ ( 𝑇 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) ) )
7 6 rexbidv ⊢ ( 𝑡 = 𝑇 → ( ∃ 𝑦 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) ↔ ∃ 𝑦 ∈ ℂ ( 𝑇 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) ) )
8 7 rabbidv ⊢ ( 𝑡 = 𝑇 → { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑦 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) } = { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑦 ∈ ℂ ( 𝑇 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) } )
9 df-eigvec ⊢ eigvec = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑦 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) } )
10 4 1 1 8 9 fvmptmap ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( eigvec ‘ 𝑇 ) = { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑦 ∈ ℂ ( 𝑇 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) } )