Theorem nlfnval

Description: Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nlfnval	⊢ ( 𝑇 : ℋ ⟶ ℂ → ( null ‘ 𝑇 ) = ( ◡ 𝑇 “ { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		cnex	⊢ ℂ ∈ V
2		ax-hilex	⊢ ℋ ∈ V
3	1 2	elmap	⊢ ( 𝑇 ∈ ( ℂ ↑m ℋ ) ↔ 𝑇 : ℋ ⟶ ℂ )
4		cnvexg	⊢ ( 𝑇 ∈ ( ℂ ↑m ℋ ) → ◡ 𝑇 ∈ V )
5		imaexg	⊢ ( ◡ 𝑇 ∈ V → ( ◡ 𝑇 “ { 0 } ) ∈ V )
6	4 5	syl	⊢ ( 𝑇 ∈ ( ℂ ↑m ℋ ) → ( ◡ 𝑇 “ { 0 } ) ∈ V )
7		cnveq	⊢ ( 𝑡 = 𝑇 → ◡ 𝑡 = ◡ 𝑇 )
8	7	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ◡ 𝑡 “ { 0 } ) = ( ◡ 𝑇 “ { 0 } ) )
9		df-nlfn	⊢ null = ( 𝑡 ∈ ( ℂ ↑m ℋ ) ↦ ( ◡ 𝑡 “ { 0 } ) )
10	8 9	fvmptg	⊢ ( ( 𝑇 ∈ ( ℂ ↑m ℋ ) ∧ ( ◡ 𝑇 “ { 0 } ) ∈ V ) → ( null ‘ 𝑇 ) = ( ◡ 𝑇 “ { 0 } ) )
11	6 10	mpdan	⊢ ( 𝑇 ∈ ( ℂ ↑m ℋ ) → ( null ‘ 𝑇 ) = ( ◡ 𝑇 “ { 0 } ) )
12	3 11	sylbir	⊢ ( 𝑇 : ℋ ⟶ ℂ → ( null ‘ 𝑇 ) = ( ◡ 𝑇 “ { 0 } ) )