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-10
2 cnvimass ⊢T-10⊆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-10
9 8 adantr ⊢T:ℋ⟶ℂ∧A∈ℋ→A∈null⁡T↔A∈T-10
10 ffn ⊢T:ℋ⟶ℂ→TFnℋ
11 eleq1 ⊢x=A→x∈T-10↔A∈T-10
12 fveqeq2 ⊢x=A→T⁡x=0↔T⁡A=0
13 11 12 bibi12d ⊢x=A→x∈T-10↔T⁡x=0↔A∈T-10↔T⁡A=0
14 13 imbi2d ⊢x=A→TFnℋ→x∈T-10↔T⁡x=0↔TFnℋ→A∈T-10↔T⁡A=0
15 0cn ⊢0∈ℂ
16 vex ⊢x∈V
17 16 eliniseg ⊢0∈ℂ→x∈T-10↔xT0
18 15 17 ax-mp ⊢x∈T-10↔xT0
19 fnbrfvb ⊢TFnℋ∧x∈ℋ→T⁡x=0↔xT0
20 18 19 bitr4id ⊢TFnℋ∧x∈ℋ→x∈T-10↔T⁡x=0
21 20 expcom ⊢x∈ℋ→TFnℋ→x∈T-10↔T⁡x=0
22 14 21 vtoclga ⊢A∈ℋ→TFnℋ→A∈T-10↔T⁡A=0
23 10 22 mpan9 ⊢T:ℋ⟶ℂ∧A∈ℋ→A∈T-10↔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