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	⊢ 𝑇 ∈ LinFn
	nlelch.2	⊢ 𝑇 ∈ ContFn
Assertion	nlelchi	⊢ ( null ‘ 𝑇 ) ∈ Cℋ

Proof

Step	Hyp	Ref	Expression
1		nlelch.1	⊢ 𝑇 ∈ LinFn
2		nlelch.2	⊢ 𝑇 ∈ ContFn
3	1	nlelshi	⊢ ( null ‘ 𝑇 ) ∈ Sℋ
4		vex	⊢ 𝑥 ∈ V
5	4	hlimveci	⊢ ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ ℋ )
6	5	adantl	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ℋ )
7		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
8	7	cnfldhaus	⊢ ( TopOpen ‘ ℂfld ) ∈ Haus
9	8	a1i	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( TopOpen ‘ ℂfld ) ∈ Haus )
10		eqid	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
11		eqid	⊢ ( normℎ ∘ −ℎ ) = ( normℎ ∘ −ℎ )
12	10 11	hhims	⊢ ( normℎ ∘ −ℎ ) = ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
13		eqid	⊢ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) = ( MetOpen ‘ ( normℎ ∘ −ℎ ) )
14	10 12 13	hhlm	⊢ ⇝𝑣 = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ) ↾ ( ℋ ↑m ℕ ) )
15		resss	⊢ ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ) ↾ ( ℋ ↑m ℕ ) ) ⊆ ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) )
16	14 15	eqsstri	⊢ ⇝𝑣 ⊆ ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) )
17	16	ssbri	⊢ ( 𝑓 ⇝𝑣 𝑥 → 𝑓 ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ) 𝑥 )
18	17	adantl	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑓 ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ) 𝑥 )
19	11 13 7	hhcnf	⊢ ContFn = ( ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) Cn ( TopOpen ‘ ℂfld ) )
20	2 19	eleqtri	⊢ 𝑇 ∈ ( ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) Cn ( TopOpen ‘ ℂfld ) )
21	20	a1i	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑇 ∈ ( ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) Cn ( TopOpen ‘ ℂfld ) ) )
22	18 21	lmcn	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 𝑇 ∘ 𝑓 ) ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) ( 𝑇 ‘ 𝑥 ) )
23	1	lnfnfi	⊢ 𝑇 : ℋ ⟶ ℂ
24		ffvelcdm	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ ( null ‘ 𝑇 ) )
25	24	adantlr	⊢ ( ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ ( null ‘ 𝑇 ) )
26		elnlfn2	⊢ ( ( 𝑇 : ℋ ⟶ ℂ ∧ ( 𝑓 ‘ 𝑛 ) ∈ ( null ‘ 𝑇 ) ) → ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) = 0 )
27	23 25 26	sylancr	⊢ ( ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) = 0 )
28		fvco3	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑇 ∘ 𝑓 ) ‘ 𝑛 ) = ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) )
29	28	adantlr	⊢ ( ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑇 ∘ 𝑓 ) ‘ 𝑛 ) = ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) )
30		c0ex	⊢ 0 ∈ V
31	30	fvconst2	⊢ ( 𝑛 ∈ ℕ → ( ( ℕ × { 0 } ) ‘ 𝑛 ) = 0 )
32	31	adantl	⊢ ( ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( ( ℕ × { 0 } ) ‘ 𝑛 ) = 0 )
33	27 29 32	3eqtr4d	⊢ ( ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑇 ∘ 𝑓 ) ‘ 𝑛 ) = ( ( ℕ × { 0 } ) ‘ 𝑛 ) )
34	33	ralrimiva	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ∀ 𝑛 ∈ ℕ ( ( 𝑇 ∘ 𝑓 ) ‘ 𝑛 ) = ( ( ℕ × { 0 } ) ‘ 𝑛 ) )
35		ffn	⊢ ( 𝑇 : ℋ ⟶ ℂ → 𝑇 Fn ℋ )
36	23 35	ax-mp	⊢ 𝑇 Fn ℋ
37		simpl	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) )
38	3	shssii	⊢ ( null ‘ 𝑇 ) ⊆ ℋ
39		fss	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ ( null ‘ 𝑇 ) ⊆ ℋ ) → 𝑓 : ℕ ⟶ ℋ )
40	37 38 39	sylancl	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑓 : ℕ ⟶ ℋ )
41		fnfco	⊢ ( ( 𝑇 Fn ℋ ∧ 𝑓 : ℕ ⟶ ℋ ) → ( 𝑇 ∘ 𝑓 ) Fn ℕ )
42	36 40 41	sylancr	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 𝑇 ∘ 𝑓 ) Fn ℕ )
43	30	fconst	⊢ ( ℕ × { 0 } ) : ℕ ⟶ { 0 }
44		ffn	⊢ ( ( ℕ × { 0 } ) : ℕ ⟶ { 0 } → ( ℕ × { 0 } ) Fn ℕ )
45	43 44	ax-mp	⊢ ( ℕ × { 0 } ) Fn ℕ
46		eqfnfv	⊢ ( ( ( 𝑇 ∘ 𝑓 ) Fn ℕ ∧ ( ℕ × { 0 } ) Fn ℕ ) → ( ( 𝑇 ∘ 𝑓 ) = ( ℕ × { 0 } ) ↔ ∀ 𝑛 ∈ ℕ ( ( 𝑇 ∘ 𝑓 ) ‘ 𝑛 ) = ( ( ℕ × { 0 } ) ‘ 𝑛 ) ) )
47	42 45 46	sylancl	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( ( 𝑇 ∘ 𝑓 ) = ( ℕ × { 0 } ) ↔ ∀ 𝑛 ∈ ℕ ( ( 𝑇 ∘ 𝑓 ) ‘ 𝑛 ) = ( ( ℕ × { 0 } ) ‘ 𝑛 ) ) )
48	34 47	mpbird	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 𝑇 ∘ 𝑓 ) = ( ℕ × { 0 } ) )
49	7	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
50	49	a1i	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
51		0cnd	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 0 ∈ ℂ )
52		1zzd	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 1 ∈ ℤ )
53		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
54	53	lmconst	⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℤ ) → ( ℕ × { 0 } ) ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 0 )
55	50 51 52 54	syl3anc	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( ℕ × { 0 } ) ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 0 )
56	48 55	eqbrtrd	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 𝑇 ∘ 𝑓 ) ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 0 )
57	9 22 56	lmmo	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 𝑇 ‘ 𝑥 ) = 0 )
58		elnlfn	⊢ ( 𝑇 : ℋ ⟶ ℂ → ( 𝑥 ∈ ( null ‘ 𝑇 ) ↔ ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) = 0 ) ) )
59	23 58	ax-mp	⊢ ( 𝑥 ∈ ( null ‘ 𝑇 ) ↔ ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) = 0 ) )
60	6 57 59	sylanbrc	⊢ ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ( null ‘ 𝑇 ) )
61	60	gen2	⊢ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ( null ‘ 𝑇 ) )
62		isch2	⊢ ( ( null ‘ 𝑇 ) ∈ Cℋ ↔ ( ( null ‘ 𝑇 ) ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ ( null ‘ 𝑇 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ( null ‘ 𝑇 ) ) ) )
63	3 61 62	mpbir2an	⊢ ( null ‘ 𝑇 ) ∈ Cℋ