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 ⊢ T : ℋ ⟶ ℂ → A ∈ null ⁡ T ↔ A ∈ ℋ ∧ T ⁡ A = 0

Proof

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