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	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝐴 ∈ ( eigvec ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eigvecval	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( eigvec ‘ 𝑇 ) = { 𝑦 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝑦 ) = ( 𝑥 ·ℎ 𝑦 ) } )
2	1	eleq2d	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝐴 ∈ ( eigvec ‘ 𝑇 ) ↔ 𝐴 ∈ { 𝑦 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝑦 ) = ( 𝑥 ·ℎ 𝑦 ) } ) )
3		eldif	⊢ ( 𝐴 ∈ ( ℋ ∖ 0ℋ ) ↔ ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 ∈ 0ℋ ) )
4		elch0	⊢ ( 𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ )
5	4	necon3bbii	⊢ ( ¬ 𝐴 ∈ 0ℋ ↔ 𝐴 ≠ 0ℎ )
6	5	anbi2i	⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 ∈ 0ℋ ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) )
7	3 6	bitri	⊢ ( 𝐴 ∈ ( ℋ ∖ 0ℋ ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) )
8	7	anbi1i	⊢ ( ( 𝐴 ∈ ( ℋ ∖ 0ℋ ) ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) ↔ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) )
9		fveq2	⊢ ( 𝑦 = 𝐴 → ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ 𝐴 ) )
10		oveq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 ·ℎ 𝑦 ) = ( 𝑥 ·ℎ 𝐴 ) )
11	9 10	eqeq12d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑇 ‘ 𝑦 ) = ( 𝑥 ·ℎ 𝑦 ) ↔ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) )
12	11	rexbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝑦 ) = ( 𝑥 ·ℎ 𝑦 ) ↔ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) )
13	12	elrab	⊢ ( 𝐴 ∈ { 𝑦 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝑦 ) = ( 𝑥 ·ℎ 𝑦 ) } ↔ ( 𝐴 ∈ ( ℋ ∖ 0ℋ ) ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) )
14		df-3an	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) ↔ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) )
15	8 13 14	3bitr4i	⊢ ( 𝐴 ∈ { 𝑦 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝑦 ) = ( 𝑥 ·ℎ 𝑦 ) } ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) )
16	2 15	bitrdi	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝐴 ∈ ( eigvec ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ∃ 𝑥 ∈ ℂ ( 𝑇 ‘ 𝐴 ) = ( 𝑥 ·ℎ 𝐴 ) ) ) )