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 ⊢ 𝑇 ∈ 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ℋ