Step | Hyp | Ref
| Expression |
1 | | nlelch.1 |
. . 3
⊢ 𝑇 ∈ LinFn |
2 | 1 | nlelshi 29995 |
. 2
⊢
(null‘𝑇)
∈ Sℋ |
3 | | vex 3402 |
. . . . . 6
⊢ 𝑥 ∈ V |
4 | 3 | hlimveci 29125 |
. . . . 5
⊢ (𝑓 ⇝𝑣
𝑥 → 𝑥 ∈ ℋ) |
5 | 4 | adantl 485 |
. . . 4
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ ℋ) |
6 | | eqid 2738 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
7 | 6 | cnfldhaus 23537 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈ Haus |
8 | 7 | a1i 11 |
. . . . 5
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) →
(TopOpen‘ℂfld) ∈ Haus) |
9 | | eqid 2738 |
. . . . . . . . . 10
⊢
〈〈 +ℎ , ·ℎ
〉, normℎ〉 = 〈〈 +ℎ ,
·ℎ 〉,
normℎ〉 |
10 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(normℎ ∘ −ℎ ) =
(normℎ ∘ −ℎ ) |
11 | 9, 10 | hhims 29107 |
. . . . . . . . . 10
⊢
(normℎ ∘ −ℎ ) =
(IndMet‘〈〈 +ℎ ,
·ℎ 〉,
normℎ〉) |
12 | | eqid 2738 |
. . . . . . . . . 10
⊢
(MetOpen‘(normℎ ∘
−ℎ )) = (MetOpen‘(normℎ ∘
−ℎ )) |
13 | 9, 11, 12 | hhlm 29134 |
. . . . . . . . 9
⊢
⇝𝑣 =
((⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ ))) ↾ ( ℋ ↑m
ℕ)) |
14 | | resss 5850 |
. . . . . . . . 9
⊢
((⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ ))) ↾ ( ℋ ↑m
ℕ)) ⊆
(⇝𝑡‘(MetOpen‘(normℎ ∘
−ℎ ))) |
15 | 13, 14 | eqsstri 3911 |
. . . . . . . 8
⊢
⇝𝑣 ⊆
(⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ ))) |
16 | 15 | ssbri 5075 |
. . . . . . 7
⊢ (𝑓 ⇝𝑣
𝑥 → 𝑓(⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ )))𝑥) |
17 | 16 | adantl 485 |
. . . . . 6
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑓(⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ )))𝑥) |
18 | | nlelch.2 |
. . . . . . . 8
⊢ 𝑇 ∈ ContFn |
19 | 10, 12, 6 | hhcnf 29840 |
. . . . . . . 8
⊢ ContFn =
((MetOpen‘(normℎ ∘ −ℎ ))
Cn (TopOpen‘ℂfld)) |
20 | 18, 19 | eleqtri 2831 |
. . . . . . 7
⊢ 𝑇 ∈
((MetOpen‘(normℎ ∘ −ℎ ))
Cn (TopOpen‘ℂfld)) |
21 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑇 ∈
((MetOpen‘(normℎ ∘ −ℎ ))
Cn (TopOpen‘ℂfld))) |
22 | 17, 21 | lmcn 22056 |
. . . . 5
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇 ∘ 𝑓)(⇝𝑡‘(TopOpen‘ℂfld))(𝑇‘𝑥)) |
23 | 1 | lnfnfi 29976 |
. . . . . . . . . 10
⊢ 𝑇:
ℋ⟶ℂ |
24 | | ffvelrn 6859 |
. . . . . . . . . . 11
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ (null‘𝑇)) |
25 | 24 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ (null‘𝑇)) |
26 | | elnlfn2 29864 |
. . . . . . . . . 10
⊢ ((𝑇: ℋ⟶ℂ ∧
(𝑓‘𝑛) ∈ (null‘𝑇)) → (𝑇‘(𝑓‘𝑛)) = 0) |
27 | 23, 25, 26 | sylancr 590 |
. . . . . . . . 9
⊢ (((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑓‘𝑛)) = 0) |
28 | | fvco3 6767 |
. . . . . . . . . 10
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑛 ∈ ℕ) → ((𝑇 ∘ 𝑓)‘𝑛) = (𝑇‘(𝑓‘𝑛))) |
29 | 28 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑛 ∈ ℕ) → ((𝑇 ∘ 𝑓)‘𝑛) = (𝑇‘(𝑓‘𝑛))) |
30 | | c0ex 10713 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
31 | 30 | fvconst2 6976 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → ((ℕ
× {0})‘𝑛) =
0) |
32 | 31 | adantl 485 |
. . . . . . . . 9
⊢ (((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑛 ∈ ℕ) → ((ℕ ×
{0})‘𝑛) =
0) |
33 | 27, 29, 32 | 3eqtr4d 2783 |
. . . . . . . 8
⊢ (((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑛 ∈ ℕ) → ((𝑇 ∘ 𝑓)‘𝑛) = ((ℕ × {0})‘𝑛)) |
34 | 33 | ralrimiva 3096 |
. . . . . . 7
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → ∀𝑛 ∈ ℕ ((𝑇 ∘ 𝑓)‘𝑛) = ((ℕ × {0})‘𝑛)) |
35 | | ffn 6504 |
. . . . . . . . . 10
⊢ (𝑇: ℋ⟶ℂ →
𝑇 Fn
ℋ) |
36 | 23, 35 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝑇 Fn ℋ |
37 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑓:ℕ⟶(null‘𝑇)) |
38 | 2 | shssii 29148 |
. . . . . . . . . 10
⊢
(null‘𝑇)
⊆ ℋ |
39 | | fss 6521 |
. . . . . . . . . 10
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ (null‘𝑇) ⊆ ℋ) → 𝑓:ℕ⟶ ℋ) |
40 | 37, 38, 39 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑓:ℕ⟶ ℋ) |
41 | | fnfco 6543 |
. . . . . . . . 9
⊢ ((𝑇 Fn ℋ ∧ 𝑓:ℕ⟶ ℋ) →
(𝑇 ∘ 𝑓) Fn ℕ) |
42 | 36, 40, 41 | sylancr 590 |
. . . . . . . 8
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇 ∘ 𝑓) Fn ℕ) |
43 | 30 | fconst 6564 |
. . . . . . . . 9
⊢ (ℕ
× {0}):ℕ⟶{0} |
44 | | ffn 6504 |
. . . . . . . . 9
⊢ ((ℕ
× {0}):ℕ⟶{0} → (ℕ × {0}) Fn
ℕ) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . 8
⊢ (ℕ
× {0}) Fn ℕ |
46 | | eqfnfv 6809 |
. . . . . . . 8
⊢ (((𝑇 ∘ 𝑓) Fn ℕ ∧ (ℕ × {0}) Fn
ℕ) → ((𝑇 ∘
𝑓) = (ℕ × {0})
↔ ∀𝑛 ∈
ℕ ((𝑇 ∘ 𝑓)‘𝑛) = ((ℕ × {0})‘𝑛))) |
47 | 42, 45, 46 | sylancl 589 |
. . . . . . 7
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → ((𝑇 ∘ 𝑓) = (ℕ × {0}) ↔
∀𝑛 ∈ ℕ
((𝑇 ∘ 𝑓)‘𝑛) = ((ℕ × {0})‘𝑛))) |
48 | 34, 47 | mpbird 260 |
. . . . . 6
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇 ∘ 𝑓) = (ℕ × {0})) |
49 | 6 | cnfldtopon 23535 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
50 | 49 | a1i 11 |
. . . . . . 7
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
51 | | 0cnd 10712 |
. . . . . . 7
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 0 ∈
ℂ) |
52 | | 1zzd 12094 |
. . . . . . 7
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 1 ∈
ℤ) |
53 | | nnuz 12363 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
54 | 53 | lmconst 22012 |
. . . . . . 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 5052 |
. . . . 5
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇 ∘ 𝑓)(⇝𝑡‘(TopOpen‘ℂfld))0) |
57 | 8, 22, 56 | lmmo 22131 |
. . . 4
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇‘𝑥) = 0) |
58 | | elnlfn 29863 |
. . . . 5
⊢ (𝑇: ℋ⟶ℂ →
(𝑥 ∈ (null‘𝑇) ↔ (𝑥 ∈ ℋ ∧ (𝑇‘𝑥) = 0))) |
59 | 23, 58 | ax-mp 5 |
. . . 4
⊢ (𝑥 ∈ (null‘𝑇) ↔ (𝑥 ∈ ℋ ∧ (𝑇‘𝑥) = 0)) |
60 | 5, 57, 59 | sylanbrc 586 |
. . 3
⊢ ((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ (null‘𝑇)) |
61 | 60 | gen2 1803 |
. 2
⊢
∀𝑓∀𝑥((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ (null‘𝑇)) |
62 | | isch2 29158 |
. 2
⊢
((null‘𝑇)
∈ Cℋ ↔ ((null‘𝑇) ∈ Sℋ
∧ ∀𝑓∀𝑥((𝑓:ℕ⟶(null‘𝑇) ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ (null‘𝑇)))) |
63 | 2, 61, 62 | mpbir2an 711 |
1
⊢
(null‘𝑇)
∈ Cℋ |