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 LinFn$
	nlelch.2	$⊢ T \in ContFn$
Assertion	nlelchi	$⊢ null (T) \in C_{ℋ}$

Proof

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

Metamath Proof Explorer

Theorem nlelchi

Proof