Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
2 | 1 | cnfldhaus 23682 |
. . 3
⊢
(TopOpen‘ℂfld) ∈ Haus |
3 | 2 | a1i 11 |
. 2
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Haus) |
4 | | occl.2 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ Cauchy) |
5 | | ax-hcompl 29283 |
. . . . . . 7
⊢ (𝐹 ∈ Cauchy →
∃𝑥 ∈ ℋ
𝐹
⇝𝑣 𝑥) |
6 | | hlimf 29318 |
. . . . . . . . . 10
⊢
⇝𝑣 :dom ⇝𝑣 ⟶
ℋ |
7 | | ffn 6545 |
. . . . . . . . . 10
⊢ (
⇝𝑣 :dom ⇝𝑣 ⟶ ℋ
→ ⇝𝑣 Fn dom ⇝𝑣
) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . 9
⊢
⇝𝑣 Fn dom ⇝𝑣 |
9 | | fnbr 6486 |
. . . . . . . . 9
⊢ ((
⇝𝑣 Fn dom ⇝𝑣 ∧ 𝐹 ⇝𝑣
𝑥) → 𝐹 ∈ dom ⇝𝑣
) |
10 | 8, 9 | mpan 690 |
. . . . . . . 8
⊢ (𝐹 ⇝𝑣
𝑥 → 𝐹 ∈ dom ⇝𝑣
) |
11 | 10 | rexlimivw 3201 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℋ 𝐹
⇝𝑣 𝑥 → 𝐹 ∈ dom ⇝𝑣
) |
12 | 4, 5, 11 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ dom ⇝𝑣
) |
13 | | ffun 6548 |
. . . . . . 7
⊢ (
⇝𝑣 :dom ⇝𝑣 ⟶ ℋ
→ Fun ⇝𝑣 ) |
14 | | funfvbrb 6871 |
. . . . . . 7
⊢ (Fun
⇝𝑣 → (𝐹 ∈ dom ⇝𝑣
↔ 𝐹
⇝𝑣 ( ⇝𝑣 ‘𝐹))) |
15 | 6, 13, 14 | mp2b 10 |
. . . . . 6
⊢ (𝐹 ∈ dom
⇝𝑣 ↔ 𝐹 ⇝𝑣 (
⇝𝑣 ‘𝐹)) |
16 | 12, 15 | sylib 221 |
. . . . 5
⊢ (𝜑 → 𝐹 ⇝𝑣 (
⇝𝑣 ‘𝐹)) |
17 | | eqid 2737 |
. . . . . . . 8
⊢
〈〈 +ℎ , ·ℎ
〉, normℎ〉 = 〈〈 +ℎ ,
·ℎ 〉,
normℎ〉 |
18 | | eqid 2737 |
. . . . . . . . 9
⊢
(normℎ ∘ −ℎ ) =
(normℎ ∘ −ℎ ) |
19 | 17, 18 | hhims 29253 |
. . . . . . . 8
⊢
(normℎ ∘ −ℎ ) =
(IndMet‘〈〈 +ℎ ,
·ℎ 〉,
normℎ〉) |
20 | | eqid 2737 |
. . . . . . . 8
⊢
(MetOpen‘(normℎ ∘
−ℎ )) = (MetOpen‘(normℎ ∘
−ℎ )) |
21 | 17, 19, 20 | hhlm 29280 |
. . . . . . 7
⊢
⇝𝑣 =
((⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ ))) ↾ ( ℋ ↑m
ℕ)) |
22 | | resss 5876 |
. . . . . . 7
⊢
((⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ ))) ↾ ( ℋ ↑m
ℕ)) ⊆
(⇝𝑡‘(MetOpen‘(normℎ ∘
−ℎ ))) |
23 | 21, 22 | eqsstri 3935 |
. . . . . 6
⊢
⇝𝑣 ⊆
(⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ ))) |
24 | 23 | ssbri 5098 |
. . . . 5
⊢ (𝐹 ⇝𝑣 (
⇝𝑣 ‘𝐹) → 𝐹(⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ )))( ⇝𝑣 ‘𝐹)) |
25 | 16, 24 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹(⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ )))( ⇝𝑣 ‘𝐹)) |
26 | 18 | hilxmet 29276 |
. . . . . 6
⊢
(normℎ ∘ −ℎ ) ∈
(∞Met‘ ℋ) |
27 | 20 | mopntopon 23337 |
. . . . . 6
⊢
((normℎ ∘ −ℎ ) ∈
(∞Met‘ ℋ) → (MetOpen‘(normℎ
∘ −ℎ )) ∈ (TopOn‘
ℋ)) |
28 | 26, 27 | mp1i 13 |
. . . . 5
⊢ (𝜑 →
(MetOpen‘(normℎ ∘ −ℎ ))
∈ (TopOn‘ ℋ)) |
29 | 28 | cnmptid 22558 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℋ ↦ 𝑥) ∈
((MetOpen‘(normℎ ∘ −ℎ ))
Cn (MetOpen‘(normℎ ∘ −ℎ
)))) |
30 | | occl.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ℋ) |
31 | | occl.4 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
32 | 30, 31 | sseldd 3902 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℋ) |
33 | 28, 28, 32 | cnmptc 22559 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℋ ↦ 𝐵) ∈
((MetOpen‘(normℎ ∘ −ℎ ))
Cn (MetOpen‘(normℎ ∘ −ℎ
)))) |
34 | 17 | hhnv 29246 |
. . . . . 6
⊢
〈〈 +ℎ , ·ℎ
〉, normℎ〉 ∈ NrmCVec |
35 | 17 | hhip 29258 |
. . . . . . 7
⊢
·ih =
(·𝑖OLD‘〈〈 +ℎ
, ·ℎ 〉,
normℎ〉) |
36 | 35, 19, 20, 1 | dipcn 28801 |
. . . . . 6
⊢
(〈〈 +ℎ , ·ℎ
〉, normℎ〉 ∈ NrmCVec →
·ih ∈
(((MetOpen‘(normℎ ∘ −ℎ ))
×t (MetOpen‘(normℎ ∘
−ℎ ))) Cn
(TopOpen‘ℂfld))) |
37 | 34, 36 | mp1i 13 |
. . . . 5
⊢ (𝜑 →
·ih ∈
(((MetOpen‘(normℎ ∘ −ℎ ))
×t (MetOpen‘(normℎ ∘
−ℎ ))) Cn
(TopOpen‘ℂfld))) |
38 | 28, 29, 33, 37 | cnmpt12f 22563 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∈
((MetOpen‘(normℎ ∘ −ℎ ))
Cn (TopOpen‘ℂfld))) |
39 | 25, 38 | lmcn 22202 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹)(⇝𝑡‘(TopOpen‘ℂfld))((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘( ⇝𝑣 ‘𝐹))) |
40 | | occl.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ⟶(⊥‘𝐴)) |
41 | 40 | ffvelrnda 6904 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (⊥‘𝐴)) |
42 | | ocel 29362 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ ℋ → ((𝐹‘𝑘) ∈ (⊥‘𝐴) ↔ ((𝐹‘𝑘) ∈ ℋ ∧ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑘) ·ih 𝑥) = 0))) |
43 | 30, 42 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹‘𝑘) ∈ (⊥‘𝐴) ↔ ((𝐹‘𝑘) ∈ ℋ ∧ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑘) ·ih 𝑥) = 0))) |
44 | 43 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) ∈ (⊥‘𝐴) ↔ ((𝐹‘𝑘) ∈ ℋ ∧ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑘) ·ih 𝑥) = 0))) |
45 | 41, 44 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) ∈ ℋ ∧ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑘) ·ih 𝑥) = 0)) |
46 | 45 | simpld 498 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℋ) |
47 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑘) → (𝑥 ·ih 𝐵) = ((𝐹‘𝑘) ·ih 𝐵)) |
48 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℋ ↦ (𝑥
·ih 𝐵)) = (𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) |
49 | | ovex 7246 |
. . . . . . . . 9
⊢ ((𝐹‘𝑘) ·ih 𝐵) ∈ V |
50 | 47, 48, 49 | fvmpt 6818 |
. . . . . . . 8
⊢ ((𝐹‘𝑘) ∈ ℋ → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(𝐹‘𝑘)) = ((𝐹‘𝑘) ·ih 𝐵)) |
51 | 46, 50 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(𝐹‘𝑘)) = ((𝐹‘𝑘) ·ih 𝐵)) |
52 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑘) ·ih 𝑥) = ((𝐹‘𝑘) ·ih 𝐵)) |
53 | 52 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (((𝐹‘𝑘) ·ih 𝑥) = 0 ↔ ((𝐹‘𝑘) ·ih 𝐵) = 0)) |
54 | 45 | simprd 499 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑘) ·ih 𝑥) = 0) |
55 | 31 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ 𝐴) |
56 | 53, 54, 55 | rspcdva 3539 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) ·ih 𝐵) = 0) |
57 | 51, 56 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(𝐹‘𝑘)) = 0) |
58 | | ocss 29366 |
. . . . . . . . 9
⊢ (𝐴 ⊆ ℋ →
(⊥‘𝐴) ⊆
ℋ) |
59 | 30, 58 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (⊥‘𝐴) ⊆
ℋ) |
60 | 40, 59 | fssd 6563 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶ ℋ) |
61 | | fvco3 6810 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶ ℋ ∧
𝑘 ∈ ℕ) →
(((𝑥 ∈ ℋ ↦
(𝑥
·ih 𝐵)) ∘ 𝐹)‘𝑘) = ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(𝐹‘𝑘))) |
62 | 60, 61 | sylan 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹)‘𝑘) = ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(𝐹‘𝑘))) |
63 | | c0ex 10827 |
. . . . . . . 8
⊢ 0 ∈
V |
64 | 63 | fvconst2 7019 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((ℕ
× {0})‘𝑘) =
0) |
65 | 64 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℕ ×
{0})‘𝑘) =
0) |
66 | 57, 62, 65 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹)‘𝑘) = ((ℕ × {0})‘𝑘)) |
67 | 66 | ralrimiva 3105 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ ℕ (((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹)‘𝑘) = ((ℕ × {0})‘𝑘)) |
68 | | ovex 7246 |
. . . . . . 7
⊢ (𝑥
·ih 𝐵) ∈ V |
69 | 68, 48 | fnmpti 6521 |
. . . . . 6
⊢ (𝑥 ∈ ℋ ↦ (𝑥
·ih 𝐵)) Fn ℋ |
70 | | fnfco 6584 |
. . . . . 6
⊢ (((𝑥 ∈ ℋ ↦ (𝑥
·ih 𝐵)) Fn ℋ ∧ 𝐹:ℕ⟶ ℋ) → ((𝑥 ∈ ℋ ↦ (𝑥
·ih 𝐵)) ∘ 𝐹) Fn ℕ) |
71 | 69, 60, 70 | sylancr 590 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹) Fn ℕ) |
72 | 63 | fconst 6605 |
. . . . . 6
⊢ (ℕ
× {0}):ℕ⟶{0} |
73 | | ffn 6545 |
. . . . . 6
⊢ ((ℕ
× {0}):ℕ⟶{0} → (ℕ × {0}) Fn
ℕ) |
74 | 72, 73 | ax-mp 5 |
. . . . 5
⊢ (ℕ
× {0}) Fn ℕ |
75 | | eqfnfv 6852 |
. . . . 5
⊢ ((((𝑥 ∈ ℋ ↦ (𝑥
·ih 𝐵)) ∘ 𝐹) Fn ℕ ∧ (ℕ × {0}) Fn
ℕ) → (((𝑥 ∈
ℋ ↦ (𝑥
·ih 𝐵)) ∘ 𝐹) = (ℕ × {0}) ↔
∀𝑘 ∈ ℕ
(((𝑥 ∈ ℋ ↦
(𝑥
·ih 𝐵)) ∘ 𝐹)‘𝑘) = ((ℕ × {0})‘𝑘))) |
76 | 71, 74, 75 | sylancl 589 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹) = (ℕ × {0}) ↔
∀𝑘 ∈ ℕ
(((𝑥 ∈ ℋ ↦
(𝑥
·ih 𝐵)) ∘ 𝐹)‘𝑘) = ((ℕ × {0})‘𝑘))) |
77 | 67, 76 | mpbird 260 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹) = (ℕ × {0})) |
78 | | fvex 6730 |
. . . . 5
⊢ (
⇝𝑣 ‘𝐹) ∈ V |
79 | 78 | hlimveci 29271 |
. . . 4
⊢ (𝐹 ⇝𝑣 (
⇝𝑣 ‘𝐹) → ( ⇝𝑣
‘𝐹) ∈
ℋ) |
80 | | oveq1 7220 |
. . . . 5
⊢ (𝑥 = ( ⇝𝑣
‘𝐹) → (𝑥
·ih 𝐵) = (( ⇝𝑣
‘𝐹)
·ih 𝐵)) |
81 | | ovex 7246 |
. . . . 5
⊢ ((
⇝𝑣 ‘𝐹) ·ih 𝐵) ∈ V |
82 | 80, 48, 81 | fvmpt 6818 |
. . . 4
⊢ ((
⇝𝑣 ‘𝐹) ∈ ℋ → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(
⇝𝑣 ‘𝐹)) = (( ⇝𝑣
‘𝐹)
·ih 𝐵)) |
83 | 16, 79, 82 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(
⇝𝑣 ‘𝐹)) = (( ⇝𝑣
‘𝐹)
·ih 𝐵)) |
84 | 39, 77, 83 | 3brtr3d 5084 |
. 2
⊢ (𝜑 → (ℕ ×
{0})(⇝𝑡‘(TopOpen‘ℂfld))((
⇝𝑣 ‘𝐹) ·ih 𝐵)) |
85 | 1 | cnfldtopon 23680 |
. . . 4
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
86 | 85 | a1i 11 |
. . 3
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
87 | | 0cnd 10826 |
. . 3
⊢ (𝜑 → 0 ∈
ℂ) |
88 | | 1zzd 12208 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
89 | | nnuz 12477 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
90 | 89 | lmconst 22158 |
. . 3
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 0 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ ×
{0})(⇝𝑡‘(TopOpen‘ℂfld))0) |
91 | 86, 87, 88, 90 | syl3anc 1373 |
. 2
⊢ (𝜑 → (ℕ ×
{0})(⇝𝑡‘(TopOpen‘ℂfld))0) |
92 | 3, 84, 91 | lmmo 22277 |
1
⊢ (𝜑 → ((
⇝𝑣 ‘𝐹) ·ih 𝐵) = 0) |