| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nlelch.1 | . . 3
⊢ 𝑇 ∈ LinFn | 
| 2 | 1 | nlelshi 32080 | . 2
⊢
(null‘𝑇)
∈ Sℋ | 
| 3 |  | vex 3483 | . . . . . 6
⊢ 𝑥 ∈ V | 
| 4 | 3 | hlimveci 31210 | . . . . 5
⊢ (𝑓 ⇝𝑣
𝑥 → 𝑥 ∈ ℋ) | 
| 5 | 4 | adantl 481 | . . . 4
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ ℋ) | 
| 6 |  | eqid 2736 | . . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 7 | 6 | cnfldhaus 24806 | . . . . . 6
⊢
(TopOpen‘ℂfld) ∈ Haus | 
| 8 | 7 | a1i 11 | . . . . 5
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) →
(TopOpen‘ℂfld) ∈ Haus) | 
| 9 |  | eqid 2736 | . . . . . . . . . 10
⊢
〈〈 +ℎ , ·ℎ
〉, normℎ〉 = 〈〈 +ℎ ,
·ℎ 〉,
normℎ〉 | 
| 10 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(normℎ ∘ −ℎ ) =
(normℎ ∘ −ℎ ) | 
| 11 | 9, 10 | hhims 31192 | . . . . . . . . . 10
⊢
(normℎ ∘ −ℎ ) =
(IndMet‘〈〈 +ℎ ,
·ℎ 〉,
normℎ〉) | 
| 12 |  | eqid 2736 | . . . . . . . . . 10
⊢
(MetOpen‘(normℎ ∘
−ℎ )) = (MetOpen‘(normℎ ∘
−ℎ )) | 
| 13 | 9, 11, 12 | hhlm 31219 | . . . . . . . . 9
⊢ 
⇝𝑣 =
((⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ ))) ↾ ( ℋ ↑m
ℕ)) | 
| 14 |  | resss 6018 | . . . . . . . . 9
⊢
((⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ ))) ↾ ( ℋ ↑m
ℕ)) ⊆
(⇝𝑡‘(MetOpen‘(normℎ ∘
−ℎ ))) | 
| 15 | 13, 14 | eqsstri 4029 | . . . . . . . 8
⊢ 
⇝𝑣 ⊆
(⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ ))) | 
| 16 | 15 | ssbri 5187 | . . . . . . 7
⊢ (𝑓 ⇝𝑣
𝑥 → 𝑓(⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ )))𝑥) | 
| 17 | 16 | adantl 481 | . . . . . 6
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑓(⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ )))𝑥) | 
| 18 |  | nlelch.2 | . . . . . . . 8
⊢ 𝑇 ∈ ContFn | 
| 19 | 10, 12, 6 | hhcnf 31925 | . . . . . . . 8
⊢ ContFn =
((MetOpen‘(normℎ ∘ −ℎ ))
Cn (TopOpen‘ℂfld)) | 
| 20 | 18, 19 | eleqtri 2838 | . . . . . . 7
⊢ 𝑇 ∈
((MetOpen‘(normℎ ∘ −ℎ ))
Cn (TopOpen‘ℂfld)) | 
| 21 | 20 | a1i 11 | . . . . . 6
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑇 ∈
((MetOpen‘(normℎ ∘ −ℎ ))
Cn (TopOpen‘ℂfld))) | 
| 22 | 17, 21 | lmcn 23314 | . . . . 5
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇 ∘ 𝑓)(⇝𝑡‘(TopOpen‘ℂfld))(𝑇‘𝑥)) | 
| 23 | 1 | lnfnfi 32061 | . . . . . . . . . 10
⊢ 𝑇:
ℋ⟶ℂ | 
| 24 |  | ffvelcdm 7100 | . . . . . . . . . . 11
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ (null‘𝑇)) | 
| 25 | 24 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ (null‘𝑇)) | 
| 26 |  | elnlfn2 31949 | . . . . . . . . . 10
⊢ ((𝑇: ℋ⟶ℂ ∧
(𝑓‘𝑛) ∈ (null‘𝑇)) → (𝑇‘(𝑓‘𝑛)) = 0) | 
| 27 | 23, 25, 26 | sylancr 587 | . . . . . . . . 9
⊢ (((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑓‘𝑛)) = 0) | 
| 28 |  | fvco3 7007 | . . . . . . . . . 10
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑛 ∈ ℕ) → ((𝑇 ∘ 𝑓)‘𝑛) = (𝑇‘(𝑓‘𝑛))) | 
| 29 | 28 | adantlr 715 | . . . . . . . . 9
⊢ (((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑛 ∈ ℕ) → ((𝑇 ∘ 𝑓)‘𝑛) = (𝑇‘(𝑓‘𝑛))) | 
| 30 |  | c0ex 11256 | . . . . . . . . . . 11
⊢ 0 ∈
V | 
| 31 | 30 | fvconst2 7225 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → ((ℕ
× {0})‘𝑛) =
0) | 
| 32 | 31 | adantl 481 | . . . . . . . . 9
⊢ (((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑛 ∈ ℕ) → ((ℕ ×
{0})‘𝑛) =
0) | 
| 33 | 27, 29, 32 | 3eqtr4d 2786 | . . . . . . . 8
⊢ (((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑛 ∈ ℕ) → ((𝑇 ∘ 𝑓)‘𝑛) = ((ℕ × {0})‘𝑛)) | 
| 34 | 33 | ralrimiva 3145 | . . . . . . 7
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → ∀𝑛 ∈ ℕ ((𝑇 ∘ 𝑓)‘𝑛) = ((ℕ × {0})‘𝑛)) | 
| 35 |  | ffn 6735 | . . . . . . . . . 10
⊢ (𝑇: ℋ⟶ℂ →
𝑇 Fn
ℋ) | 
| 36 | 23, 35 | ax-mp 5 | . . . . . . . . 9
⊢ 𝑇 Fn ℋ | 
| 37 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑓:ℕ⟶(null‘𝑇)) | 
| 38 | 2 | shssii 31233 | . . . . . . . . . 10
⊢
(null‘𝑇)
⊆ ℋ | 
| 39 |  | fss 6751 | . . . . . . . . . 10
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ (null‘𝑇) ⊆ ℋ) → 𝑓:ℕ⟶ ℋ) | 
| 40 | 37, 38, 39 | sylancl 586 | . . . . . . . . 9
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑓:ℕ⟶ ℋ) | 
| 41 |  | fnfco 6772 | . . . . . . . . 9
⊢ ((𝑇 Fn ℋ ∧ 𝑓:ℕ⟶ ℋ) →
(𝑇 ∘ 𝑓) Fn ℕ) | 
| 42 | 36, 40, 41 | sylancr 587 | . . . . . . . 8
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇 ∘ 𝑓) Fn ℕ) | 
| 43 | 30 | fconst 6793 | . . . . . . . . 9
⊢ (ℕ
× {0}):ℕ⟶{0} | 
| 44 |  | ffn 6735 | . . . . . . . . 9
⊢ ((ℕ
× {0}):ℕ⟶{0} → (ℕ × {0}) Fn
ℕ) | 
| 45 | 43, 44 | ax-mp 5 | . . . . . . . 8
⊢ (ℕ
× {0}) Fn ℕ | 
| 46 |  | eqfnfv 7050 | . . . . . . . 8
⊢ (((𝑇 ∘ 𝑓) Fn ℕ ∧ (ℕ × {0}) Fn
ℕ) → ((𝑇 ∘
𝑓) = (ℕ × {0})
↔ ∀𝑛 ∈
ℕ ((𝑇 ∘ 𝑓)‘𝑛) = ((ℕ × {0})‘𝑛))) | 
| 47 | 42, 45, 46 | sylancl 586 | . . . . . . 7
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → ((𝑇 ∘ 𝑓) = (ℕ × {0}) ↔
∀𝑛 ∈ ℕ
((𝑇 ∘ 𝑓)‘𝑛) = ((ℕ × {0})‘𝑛))) | 
| 48 | 34, 47 | mpbird 257 | . . . . . 6
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇 ∘ 𝑓) = (ℕ × {0})) | 
| 49 | 6 | cnfldtopon 24804 | . . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) | 
| 50 | 49 | a1i 11 | . . . . . . 7
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) | 
| 51 |  | 0cnd 11255 | . . . . . . 7
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 0 ∈
ℂ) | 
| 52 |  | 1zzd 12650 | . . . . . . 7
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 1 ∈
ℤ) | 
| 53 |  | nnuz 12922 | . . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) | 
| 54 | 53 | lmconst 23270 | . . . . . . 7
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 0 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ ×
{0})(⇝𝑡‘(TopOpen‘ℂfld))0) | 
| 55 | 50, 51, 52, 54 | syl3anc 1372 | . . . . . 6
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → (ℕ ×
{0})(⇝𝑡‘(TopOpen‘ℂfld))0) | 
| 56 | 48, 55 | eqbrtrd 5164 | . . . . 5
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇 ∘ 𝑓)(⇝𝑡‘(TopOpen‘ℂfld))0) | 
| 57 | 8, 22, 56 | lmmo 23389 | . . . 4
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇‘𝑥) = 0) | 
| 58 |  | elnlfn 31948 | . . . . 5
⊢ (𝑇: ℋ⟶ℂ →
(𝑥 ∈ (null‘𝑇) ↔ (𝑥 ∈ ℋ ∧ (𝑇‘𝑥) = 0))) | 
| 59 | 23, 58 | ax-mp 5 | . . . 4
⊢ (𝑥 ∈ (null‘𝑇) ↔ (𝑥 ∈ ℋ ∧ (𝑇‘𝑥) = 0)) | 
| 60 | 5, 57, 59 | sylanbrc 583 | . . 3
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ (null‘𝑇)) | 
| 61 | 60 | gen2 1795 | . 2
⊢
∀𝑓∀𝑥((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ (null‘𝑇)) | 
| 62 |  | isch2 31243 | . 2
⊢
((null‘𝑇)
∈ Cℋ ↔ ((null‘𝑇) ∈ Sℋ
∧ ∀𝑓∀𝑥((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ (null‘𝑇)))) | 
| 63 | 2, 61, 62 | mpbir2an 711 | 1
⊢
(null‘𝑇)
∈ Cℋ |