Metamath Proof Explorer

Theorem eleigvec2

Description: Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 18-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eleigvec2 ⊢ T : ℋ ⟶ ℋ → A ∈ eigvec ⁡ T ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ T ⁡ A ∈ span ⁡ A

Proof

Step Hyp Ref Expression
1 eleigvec ⊢ T : ℋ ⟶ ℋ → A ∈ eigvec ⁡ T ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
2 elspansn ⊢ A ∈ ℋ → T ⁡ A ∈ span ⁡ A ↔ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
3 2 adantr ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ A ∈ span ⁡ A ↔ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
4 3 pm5.32i ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ T ⁡ A ∈ span ⁡ A ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
5 df-3an ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ T ⁡ A ∈ span ⁡ A ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ T ⁡ A ∈ span ⁡ A
6 df-3an ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
7 4 5 6 3bitr4i ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ T ⁡ A ∈ span ⁡ A ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
8 1 7 bitr4di ⊢ T : ℋ ⟶ ℋ → A ∈ eigvec ⁡ T ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ T ⁡ A ∈ span ⁡ A