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 ⊢ T : ℋ ⟶ ℋ → eigvec ⁡ T = x ∈ ℋ ∖ 0 ℋ | ∃ y ∈ ℂ T ⁡ x = y ⋅ ℎ x

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ ℋ ∈ V
2 difexg ⊢ ℋ ∈ V → ℋ ∖ 0 ℋ ∈ V
3 1 2 ax-mp ⊢ ℋ ∖ 0 ℋ ∈ V
4 3 rabex ⊢ x ∈ ℋ ∖ 0 ℋ | ∃ y ∈ ℂ T ⁡ x = y ⋅ ℎ x ∈ V
5 fveq1 ⊢ t = T → t ⁡ x = T ⁡ x
6 5 eqeq1d ⊢ t = T → t ⁡ x = y ⋅ ℎ x ↔ T ⁡ x = y ⋅ ℎ x
7 6 rexbidv ⊢ t = T → ∃ y ∈ ℂ t ⁡ x = y ⋅ ℎ x ↔ ∃ y ∈ ℂ T ⁡ x = y ⋅ ℎ x
8 7 rabbidv ⊢ t = T → x ∈ ℋ ∖ 0 ℋ | ∃ y ∈ ℂ t ⁡ x = y ⋅ ℎ x = x ∈ ℋ ∖ 0 ℋ | ∃ y ∈ ℂ T ⁡ x = y ⋅ ℎ x
9 df-eigvec ⊢ eigvec = t ∈ ℋ ℋ ⟼ x ∈ ℋ ∖ 0 ℋ | ∃ y ∈ ℂ t ⁡ x = y ⋅ ℎ x
10 4 1 1 8 9 fvmptmap ⊢ T : ℋ ⟶ ℋ → eigvec ⁡ T = x ∈ ℋ ∖ 0 ℋ | ∃ y ∈ ℂ T ⁡ x = y ⋅ ℎ x