# Metamath Proof Explorer

## Theorem nlelchi

Description: The null space of a continuous linear functional is a closed subspace. Remark 3.8 of Beran p. 103. (Contributed by NM, 11-Feb-2006) (Proof shortened by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses nlelch.1 ${⊢}{T}\in \mathrm{LinFn}$
nlelch.2 ${⊢}{T}\in \mathrm{ContFn}$
Assertion nlelchi ${⊢}\mathrm{null}\left({T}\right)\in {\mathbf{C}}_{ℋ}$

### Proof

Step Hyp Ref Expression
1 nlelch.1 ${⊢}{T}\in \mathrm{LinFn}$
2 nlelch.2 ${⊢}{T}\in \mathrm{ContFn}$
3 1 nlelshi ${⊢}\mathrm{null}\left({T}\right)\in {\mathbf{S}}_{ℋ}$
4 vex ${⊢}{x}\in \mathrm{V}$
5 4 hlimveci
7 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
8 7 cnfldhaus ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Haus}$
9 8 a1i
10 eqid ${⊢}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
11 eqid ${⊢}{norm}_{ℎ}\circ {-}_{ℎ}={norm}_{ℎ}\circ {-}_{ℎ}$
12 10 11 hhims ${⊢}{norm}_{ℎ}\circ {-}_{ℎ}=\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
13 eqid ${⊢}\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)=\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)$
14 10 12 13 hhlm
15 resss
16 14 15 eqsstri
17 16 ssbri
19 11 13 7 hhcnf ${⊢}\mathrm{ContFn}=\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
20 2 19 eleqtri ${⊢}{T}\in \left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
21 20 a1i
22 18 21 lmcn
23 1 lnfnfi ${⊢}{T}:ℋ⟶ℂ$
24 ffvelrn ${⊢}\left({f}:ℕ⟶\mathrm{null}\left({T}\right)\wedge {n}\in ℕ\right)\to {f}\left({n}\right)\in \mathrm{null}\left({T}\right)$
26 elnlfn2 ${⊢}\left({T}:ℋ⟶ℂ\wedge {f}\left({n}\right)\in \mathrm{null}\left({T}\right)\right)\to {T}\left({f}\left({n}\right)\right)=0$
27 23 25 26 sylancr
28 fvco3 ${⊢}\left({f}:ℕ⟶\mathrm{null}\left({T}\right)\wedge {n}\in ℕ\right)\to \left({T}\circ {f}\right)\left({n}\right)={T}\left({f}\left({n}\right)\right)$
30 c0ex ${⊢}0\in \mathrm{V}$
31 30 fvconst2 ${⊢}{n}\in ℕ\to \left(ℕ×\left\{0\right\}\right)\left({n}\right)=0$
33 27 29 32 3eqtr4d
34 33 ralrimiva
35 ffn ${⊢}{T}:ℋ⟶ℂ\to {T}Fnℋ$
36 23 35 ax-mp ${⊢}{T}Fnℋ$
37 simpl
38 3 shssii ${⊢}\mathrm{null}\left({T}\right)\subseteq ℋ$
39 fss ${⊢}\left({f}:ℕ⟶\mathrm{null}\left({T}\right)\wedge \mathrm{null}\left({T}\right)\subseteq ℋ\right)\to {f}:ℕ⟶ℋ$
40 37 38 39 sylancl
41 fnfco ${⊢}\left({T}Fnℋ\wedge {f}:ℕ⟶ℋ\right)\to \left({T}\circ {f}\right)Fnℕ$
42 36 40 41 sylancr
43 30 fconst ${⊢}\left(ℕ×\left\{0\right\}\right):ℕ⟶\left\{0\right\}$
44 ffn ${⊢}\left(ℕ×\left\{0\right\}\right):ℕ⟶\left\{0\right\}\to \left(ℕ×\left\{0\right\}\right)Fnℕ$
45 43 44 ax-mp ${⊢}\left(ℕ×\left\{0\right\}\right)Fnℕ$
46 eqfnfv ${⊢}\left(\left({T}\circ {f}\right)Fnℕ\wedge \left(ℕ×\left\{0\right\}\right)Fnℕ\right)\to \left({T}\circ {f}=ℕ×\left\{0\right\}↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({T}\circ {f}\right)\left({n}\right)=\left(ℕ×\left\{0\right\}\right)\left({n}\right)\right)$
47 42 45 46 sylancl
48 34 47 mpbird
49 7 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
50 49 a1i
51 0cnd
52 1zzd
53 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
54 53 lmconst
55 50 51 52 54 syl3anc
56 48 55 eqbrtrd
57 9 22 56 lmmo
58 elnlfn ${⊢}{T}:ℋ⟶ℂ\to \left({x}\in \mathrm{null}\left({T}\right)↔\left({x}\in ℋ\wedge {T}\left({x}\right)=0\right)\right)$
59 23 58 ax-mp ${⊢}{x}\in \mathrm{null}\left({T}\right)↔\left({x}\in ℋ\wedge {T}\left({x}\right)=0\right)$
60 6 57 59 sylanbrc
61 60 gen2
62 isch2
63 3 61 62 mpbir2an ${⊢}\mathrm{null}\left({T}\right)\in {\mathbf{C}}_{ℋ}$