This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) )