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