Metamath Proof Explorer

Theorem elnlfn

Description: Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion elnlfn ( 𝑇 : ℋ ⟶ ℂ → ( 𝐴 ∈ ( null ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ ( 𝑇 ‘ 𝐴 ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 nlfnval ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( null ‘ 𝑇 ) = ( ◡ 𝑇 “ { 0 } ) )
2 cnvimass ⊢ ( ◡ 𝑇 “ { 0 } ) ⊆ dom 𝑇
3 1 2 eqsstrdi ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( null ‘ 𝑇 ) ⊆ dom 𝑇 )
4 fdm ⊢ ( 𝑇 : ℋ ⟶ ℂ → dom 𝑇 = ℋ )
5 3 4 sseqtrd ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( null ‘ 𝑇 ) ⊆ ℋ )
6 5 sseld ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( 𝐴 ∈ ( null ‘ 𝑇 ) → 𝐴 ∈ ℋ ) )
7 6 pm4.71rd ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( 𝐴 ∈ ( null ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ∈ ( null ‘ 𝑇 ) ) ) )
8 1 eleq2d ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( 𝐴 ∈ ( null ‘ 𝑇 ) ↔ 𝐴 ∈ ( ◡ 𝑇 “ { 0 } ) ) )
9 8 adantr ⊢ ( ( 𝑇 : ℋ ⟶ ℂ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ∈ ( null ‘ 𝑇 ) ↔ 𝐴 ∈ ( ◡ 𝑇 “ { 0 } ) ) )
10 ffn ⊢ ( 𝑇 : ℋ ⟶ ℂ → 𝑇 Fn ℋ )
11 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ( ◡ 𝑇 “ { 0 } ) ↔ 𝐴 ∈ ( ◡ 𝑇 “ { 0 } ) ) )
12 fveqeq2 ⊢ ( 𝑥 = 𝐴 → ( ( 𝑇 ‘ 𝑥 ) = 0 ↔ ( 𝑇 ‘ 𝐴 ) = 0 ) )
13 11 12 bibi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ ( ◡ 𝑇 “ { 0 } ) ↔ ( 𝑇 ‘ 𝑥 ) = 0 ) ↔ ( 𝐴 ∈ ( ◡ 𝑇 “ { 0 } ) ↔ ( 𝑇 ‘ 𝐴 ) = 0 ) ) )
14 13 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑇 Fn ℋ → ( 𝑥 ∈ ( ◡ 𝑇 “ { 0 } ) ↔ ( 𝑇 ‘ 𝑥 ) = 0 ) ) ↔ ( 𝑇 Fn ℋ → ( 𝐴 ∈ ( ◡ 𝑇 “ { 0 } ) ↔ ( 𝑇 ‘ 𝐴 ) = 0 ) ) ) )
15 0cn ⊢ 0 ∈ ℂ
16 vex ⊢ 𝑥 ∈ V
17 16 eliniseg ⊢ ( 0 ∈ ℂ → ( 𝑥 ∈ ( ◡ 𝑇 “ { 0 } ) ↔ 𝑥 𝑇 0 ) )
18 15 17 ax-mp ⊢ ( 𝑥 ∈ ( ◡ 𝑇 “ { 0 } ) ↔ 𝑥 𝑇 0 )
19 fnbrfvb ⊢ ( ( 𝑇 Fn ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) = 0 ↔ 𝑥 𝑇 0 ) )
20 18 19 bitr4id ⊢ ( ( 𝑇 Fn ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ∈ ( ◡ 𝑇 “ { 0 } ) ↔ ( 𝑇 ‘ 𝑥 ) = 0 ) )
21 20 expcom ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 Fn ℋ → ( 𝑥 ∈ ( ◡ 𝑇 “ { 0 } ) ↔ ( 𝑇 ‘ 𝑥 ) = 0 ) ) )
22 14 21 vtoclga ⊢ ( 𝐴 ∈ ℋ → ( 𝑇 Fn ℋ → ( 𝐴 ∈ ( ◡ 𝑇 “ { 0 } ) ↔ ( 𝑇 ‘ 𝐴 ) = 0 ) ) )
23 10 22 mpan9 ⊢ ( ( 𝑇 : ℋ ⟶ ℂ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ∈ ( ◡ 𝑇 “ { 0 } ) ↔ ( 𝑇 ‘ 𝐴 ) = 0 ) )
24 9 23 bitrd ⊢ ( ( 𝑇 : ℋ ⟶ ℂ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ∈ ( null ‘ 𝑇 ) ↔ ( 𝑇 ‘ 𝐴 ) = 0 ) )
25 24 pm5.32da ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( ( 𝐴 ∈ ℋ ∧ 𝐴 ∈ ( null ‘ 𝑇 ) ) ↔ ( 𝐴 ∈ ℋ ∧ ( 𝑇 ‘ 𝐴 ) = 0 ) ) )
26 7 25 bitrd ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( 𝐴 ∈ ( null ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ ( 𝑇 ‘ 𝐴 ) = 0 ) ) )