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	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( eigvec ‘ 𝑇 ) = { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑦 ∈ ℂ ( 𝑇 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) } )

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	⊢ ℋ ∈ V
2		difexg	⊢ ( ℋ ∈ V → ( ℋ ∖ 0ℋ ) ∈ V )
3	1 2	ax-mp	⊢ ( ℋ ∖ 0ℋ ) ∈ V
4	3	rabex	⊢ { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑦 ∈ ℂ ( 𝑇 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) } ∈ V
5		fveq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
6	5	eqeq1d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) ↔ ( 𝑇 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) ) )
7	6	rexbidv	⊢ ( 𝑡 = 𝑇 → ( ∃ 𝑦 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) ↔ ∃ 𝑦 ∈ ℂ ( 𝑇 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) ) )
8	7	rabbidv	⊢ ( 𝑡 = 𝑇 → { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑦 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) } = { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑦 ∈ ℂ ( 𝑇 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) } )
9		df-eigvec	⊢ eigvec = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑦 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) } )
10	4 1 1 8 9	fvmptmap	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( eigvec ‘ 𝑇 ) = { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑦 ∈ ℂ ( 𝑇 ‘ 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) } )