Metamath Proof Explorer

Theorem eleigvec

Description: Membership in 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 eleigvec ⊢ T : ℋ ⟶ ℋ → A ∈ eigvec ⁡ T ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A

Proof

Step Hyp Ref Expression
1 eigvecval ⊢ T : ℋ ⟶ ℋ → eigvec ⁡ T = y ∈ ℋ ∖ 0 ℋ | ∃ x ∈ ℂ T ⁡ y = x ⋅ ℎ y
2 1 eleq2d ⊢ T : ℋ ⟶ ℋ → A ∈ eigvec ⁡ T ↔ A ∈ y ∈ ℋ ∖ 0 ℋ | ∃ x ∈ ℂ T ⁡ y = x ⋅ ℎ y
3 eldif ⊢ A ∈ ℋ ∖ 0 ℋ ↔ A ∈ ℋ ∧ ¬ A ∈ 0 ℋ
4 elch0 ⊢ A ∈ 0 ℋ ↔ A = 0 ℎ
5 4 necon3bbii ⊢ ¬ A ∈ 0 ℋ ↔ A ≠ 0 ℎ
6 5 anbi2i ⊢ A ∈ ℋ ∧ ¬ A ∈ 0 ℋ ↔ A ∈ ℋ ∧ A ≠ 0 ℎ
7 3 6 bitri ⊢ A ∈ ℋ ∖ 0 ℋ ↔ A ∈ ℋ ∧ A ≠ 0 ℎ
8 7 anbi1i ⊢ A ∈ ℋ ∖ 0 ℋ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
9 fveq2 ⊢ y = A → T ⁡ y = T ⁡ A
10 oveq2 ⊢ y = A → x ⋅ ℎ y = x ⋅ ℎ A
11 9 10 eqeq12d ⊢ y = A → T ⁡ y = x ⋅ ℎ y ↔ T ⁡ A = x ⋅ ℎ A
12 11 rexbidv ⊢ y = A → ∃ x ∈ ℂ T ⁡ y = x ⋅ ℎ y ↔ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
13 12 elrab ⊢ A ∈ y ∈ ℋ ∖ 0 ℋ | ∃ x ∈ ℂ T ⁡ y = x ⋅ ℎ y ↔ A ∈ ℋ ∖ 0 ℋ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
14 df-3an ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
15 8 13 14 3bitr4i ⊢ A ∈ y ∈ ℋ ∖ 0 ℋ | ∃ x ∈ ℂ T ⁡ y = x ⋅ ℎ y ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
16 2 15 bitrdi ⊢ T : ℋ ⟶ ℋ → A ∈ eigvec ⁡ T ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A