| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 2 | 1 | cnfldhaus 24805 |
. . 3
⊢
(TopOpen‘ℂfld) ∈ Haus |
| 3 | 2 | a1i 11 |
. 2
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Haus) |
| 4 | | occl.2 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ Cauchy) |
| 5 | | ax-hcompl 31221 |
. . . . . . 7
⊢ (𝐹 ∈ Cauchy →
∃𝑥 ∈ ℋ
𝐹
⇝𝑣 𝑥) |
| 6 | | hlimf 31256 |
. . . . . . . . . 10
⊢
⇝𝑣 :dom ⇝𝑣 ⟶
ℋ |
| 7 | | ffn 6736 |
. . . . . . . . . 10
⊢ (
⇝𝑣 :dom ⇝𝑣 ⟶ ℋ
→ ⇝𝑣 Fn dom ⇝𝑣
) |
| 8 | 6, 7 | ax-mp 5 |
. . . . . . . . 9
⊢
⇝𝑣 Fn dom ⇝𝑣 |
| 9 | | fnbr 6676 |
. . . . . . . . 9
⊢ ((
⇝𝑣 Fn dom ⇝𝑣 ∧ 𝐹 ⇝𝑣
𝑥) → 𝐹 ∈ dom ⇝𝑣
) |
| 10 | 8, 9 | mpan 690 |
. . . . . . . 8
⊢ (𝐹 ⇝𝑣
𝑥 → 𝐹 ∈ dom ⇝𝑣
) |
| 11 | 10 | rexlimivw 3151 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℋ 𝐹
⇝𝑣 𝑥 → 𝐹 ∈ dom ⇝𝑣
) |
| 12 | 4, 5, 11 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ dom ⇝𝑣
) |
| 13 | | ffun 6739 |
. . . . . . 7
⊢ (
⇝𝑣 :dom ⇝𝑣 ⟶ ℋ
→ Fun ⇝𝑣 ) |
| 14 | | funfvbrb 7071 |
. . . . . . 7
⊢ (Fun
⇝𝑣 → (𝐹 ∈ dom ⇝𝑣
↔ 𝐹
⇝𝑣 ( ⇝𝑣 ‘𝐹))) |
| 15 | 6, 13, 14 | mp2b 10 |
. . . . . 6
⊢ (𝐹 ∈ dom
⇝𝑣 ↔ 𝐹 ⇝𝑣 (
⇝𝑣 ‘𝐹)) |
| 16 | 12, 15 | sylib 218 |
. . . . 5
⊢ (𝜑 → 𝐹 ⇝𝑣 (
⇝𝑣 ‘𝐹)) |
| 17 | | eqid 2737 |
. . . . . . . 8
⊢
〈〈 +ℎ , ·ℎ
〉, normℎ〉 = 〈〈 +ℎ ,
·ℎ 〉,
normℎ〉 |
| 18 | | eqid 2737 |
. . . . . . . . 9
⊢
(normℎ ∘ −ℎ ) =
(normℎ ∘ −ℎ ) |
| 19 | 17, 18 | hhims 31191 |
. . . . . . . 8
⊢
(normℎ ∘ −ℎ ) =
(IndMet‘〈〈 +ℎ ,
·ℎ 〉,
normℎ〉) |
| 20 | | eqid 2737 |
. . . . . . . 8
⊢
(MetOpen‘(normℎ ∘
−ℎ )) = (MetOpen‘(normℎ ∘
−ℎ )) |
| 21 | 17, 19, 20 | hhlm 31218 |
. . . . . . 7
⊢
⇝𝑣 =
((⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ ))) ↾ ( ℋ ↑m
ℕ)) |
| 22 | | resss 6019 |
. . . . . . 7
⊢
((⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ ))) ↾ ( ℋ ↑m
ℕ)) ⊆
(⇝𝑡‘(MetOpen‘(normℎ ∘
−ℎ ))) |
| 23 | 21, 22 | eqsstri 4030 |
. . . . . 6
⊢
⇝𝑣 ⊆
(⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ ))) |
| 24 | 23 | ssbri 5188 |
. . . . 5
⊢ (𝐹 ⇝𝑣 (
⇝𝑣 ‘𝐹) → 𝐹(⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ )))( ⇝𝑣 ‘𝐹)) |
| 25 | 16, 24 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹(⇝𝑡‘(MetOpen‘(normℎ
∘ −ℎ )))( ⇝𝑣 ‘𝐹)) |
| 26 | 18 | hilxmet 31214 |
. . . . . 6
⊢
(normℎ ∘ −ℎ ) ∈
(∞Met‘ ℋ) |
| 27 | 20 | mopntopon 24449 |
. . . . . 6
⊢
((normℎ ∘ −ℎ ) ∈
(∞Met‘ ℋ) → (MetOpen‘(normℎ
∘ −ℎ )) ∈ (TopOn‘
ℋ)) |
| 28 | 26, 27 | mp1i 13 |
. . . . 5
⊢ (𝜑 →
(MetOpen‘(normℎ ∘ −ℎ ))
∈ (TopOn‘ ℋ)) |
| 29 | 28 | cnmptid 23669 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℋ ↦ 𝑥) ∈
((MetOpen‘(normℎ ∘ −ℎ ))
Cn (MetOpen‘(normℎ ∘ −ℎ
)))) |
| 30 | | occl.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ℋ) |
| 31 | | occl.4 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
| 32 | 30, 31 | sseldd 3984 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℋ) |
| 33 | 28, 28, 32 | cnmptc 23670 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℋ ↦ 𝐵) ∈
((MetOpen‘(normℎ ∘ −ℎ ))
Cn (MetOpen‘(normℎ ∘ −ℎ
)))) |
| 34 | 17 | hhnv 31184 |
. . . . . 6
⊢
〈〈 +ℎ , ·ℎ
〉, normℎ〉 ∈ NrmCVec |
| 35 | 17 | hhip 31196 |
. . . . . . 7
⊢
·ih =
(·𝑖OLD‘〈〈 +ℎ
, ·ℎ 〉,
normℎ〉) |
| 36 | 35, 19, 20, 1 | dipcn 30739 |
. . . . . 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 23674 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∈
((MetOpen‘(normℎ ∘ −ℎ ))
Cn (TopOpen‘ℂfld))) |
| 39 | 25, 38 | lmcn 23313 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹)(⇝𝑡‘(TopOpen‘ℂfld))((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘( ⇝𝑣 ‘𝐹))) |
| 40 | | occl.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ⟶(⊥‘𝐴)) |
| 41 | 40 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (⊥‘𝐴)) |
| 42 | | ocel 31300 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ ℋ → ((𝐹‘𝑘) ∈ (⊥‘𝐴) ↔ ((𝐹‘𝑘) ∈ ℋ ∧ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑘) ·ih 𝑥) = 0))) |
| 43 | 30, 42 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹‘𝑘) ∈ (⊥‘𝐴) ↔ ((𝐹‘𝑘) ∈ ℋ ∧ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑘) ·ih 𝑥) = 0))) |
| 44 | 43 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) ∈ (⊥‘𝐴) ↔ ((𝐹‘𝑘) ∈ ℋ ∧ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑘) ·ih 𝑥) = 0))) |
| 45 | 41, 44 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) ∈ ℋ ∧ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑘) ·ih 𝑥) = 0)) |
| 46 | 45 | simpld 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℋ) |
| 47 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑘) → (𝑥 ·ih 𝐵) = ((𝐹‘𝑘) ·ih 𝐵)) |
| 48 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℋ ↦ (𝑥
·ih 𝐵)) = (𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) |
| 49 | | ovex 7464 |
. . . . . . . . 9
⊢ ((𝐹‘𝑘) ·ih 𝐵) ∈ V |
| 50 | 47, 48, 49 | fvmpt 7016 |
. . . . . . . 8
⊢ ((𝐹‘𝑘) ∈ ℋ → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(𝐹‘𝑘)) = ((𝐹‘𝑘) ·ih 𝐵)) |
| 51 | 46, 50 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(𝐹‘𝑘)) = ((𝐹‘𝑘) ·ih 𝐵)) |
| 52 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑘) ·ih 𝑥) = ((𝐹‘𝑘) ·ih 𝐵)) |
| 53 | 52 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (((𝐹‘𝑘) ·ih 𝑥) = 0 ↔ ((𝐹‘𝑘) ·ih 𝐵) = 0)) |
| 54 | 45 | simprd 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑘) ·ih 𝑥) = 0) |
| 55 | 31 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ 𝐴) |
| 56 | 53, 54, 55 | rspcdva 3623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) ·ih 𝐵) = 0) |
| 57 | 51, 56 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(𝐹‘𝑘)) = 0) |
| 58 | | ocss 31304 |
. . . . . . . . 9
⊢ (𝐴 ⊆ ℋ →
(⊥‘𝐴) ⊆
ℋ) |
| 59 | 30, 58 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (⊥‘𝐴) ⊆
ℋ) |
| 60 | 40, 59 | fssd 6753 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶ ℋ) |
| 61 | | fvco3 7008 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶ ℋ ∧
𝑘 ∈ ℕ) →
(((𝑥 ∈ ℋ ↦
(𝑥
·ih 𝐵)) ∘ 𝐹)‘𝑘) = ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(𝐹‘𝑘))) |
| 62 | 60, 61 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹)‘𝑘) = ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(𝐹‘𝑘))) |
| 63 | | c0ex 11255 |
. . . . . . . 8
⊢ 0 ∈
V |
| 64 | 63 | fvconst2 7224 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((ℕ
× {0})‘𝑘) =
0) |
| 65 | 64 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℕ ×
{0})‘𝑘) =
0) |
| 66 | 57, 62, 65 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹)‘𝑘) = ((ℕ × {0})‘𝑘)) |
| 67 | 66 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ ℕ (((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹)‘𝑘) = ((ℕ × {0})‘𝑘)) |
| 68 | | ovex 7464 |
. . . . . . 7
⊢ (𝑥
·ih 𝐵) ∈ V |
| 69 | 68, 48 | fnmpti 6711 |
. . . . . 6
⊢ (𝑥 ∈ ℋ ↦ (𝑥
·ih 𝐵)) Fn ℋ |
| 70 | | fnfco 6773 |
. . . . . 6
⊢ (((𝑥 ∈ ℋ ↦ (𝑥
·ih 𝐵)) Fn ℋ ∧ 𝐹:ℕ⟶ ℋ) → ((𝑥 ∈ ℋ ↦ (𝑥
·ih 𝐵)) ∘ 𝐹) Fn ℕ) |
| 71 | 69, 60, 70 | sylancr 587 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹) Fn ℕ) |
| 72 | 63 | fconst 6794 |
. . . . . 6
⊢ (ℕ
× {0}):ℕ⟶{0} |
| 73 | | ffn 6736 |
. . . . . 6
⊢ ((ℕ
× {0}):ℕ⟶{0} → (ℕ × {0}) Fn
ℕ) |
| 74 | 72, 73 | ax-mp 5 |
. . . . 5
⊢ (ℕ
× {0}) Fn ℕ |
| 75 | | eqfnfv 7051 |
. . . . 5
⊢ ((((𝑥 ∈ ℋ ↦ (𝑥
·ih 𝐵)) ∘ 𝐹) Fn ℕ ∧ (ℕ × {0}) Fn
ℕ) → (((𝑥 ∈
ℋ ↦ (𝑥
·ih 𝐵)) ∘ 𝐹) = (ℕ × {0}) ↔
∀𝑘 ∈ ℕ
(((𝑥 ∈ ℋ ↦
(𝑥
·ih 𝐵)) ∘ 𝐹)‘𝑘) = ((ℕ × {0})‘𝑘))) |
| 76 | 71, 74, 75 | sylancl 586 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹) = (ℕ × {0}) ↔
∀𝑘 ∈ ℕ
(((𝑥 ∈ ℋ ↦
(𝑥
·ih 𝐵)) ∘ 𝐹)‘𝑘) = ((ℕ × {0})‘𝑘))) |
| 77 | 67, 76 | mpbird 257 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵)) ∘ 𝐹) = (ℕ × {0})) |
| 78 | | fvex 6919 |
. . . . 5
⊢ (
⇝𝑣 ‘𝐹) ∈ V |
| 79 | 78 | hlimveci 31209 |
. . . 4
⊢ (𝐹 ⇝𝑣 (
⇝𝑣 ‘𝐹) → ( ⇝𝑣
‘𝐹) ∈
ℋ) |
| 80 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = ( ⇝𝑣
‘𝐹) → (𝑥
·ih 𝐵) = (( ⇝𝑣
‘𝐹)
·ih 𝐵)) |
| 81 | | ovex 7464 |
. . . . 5
⊢ ((
⇝𝑣 ‘𝐹) ·ih 𝐵) ∈ V |
| 82 | 80, 48, 81 | fvmpt 7016 |
. . . 4
⊢ ((
⇝𝑣 ‘𝐹) ∈ ℋ → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(
⇝𝑣 ‘𝐹)) = (( ⇝𝑣
‘𝐹)
·ih 𝐵)) |
| 83 | 16, 79, 82 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐵))‘(
⇝𝑣 ‘𝐹)) = (( ⇝𝑣
‘𝐹)
·ih 𝐵)) |
| 84 | 39, 77, 83 | 3brtr3d 5174 |
. 2
⊢ (𝜑 → (ℕ ×
{0})(⇝𝑡‘(TopOpen‘ℂfld))((
⇝𝑣 ‘𝐹) ·ih 𝐵)) |
| 85 | 1 | cnfldtopon 24803 |
. . . 4
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 86 | 85 | a1i 11 |
. . 3
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
| 87 | | 0cnd 11254 |
. . 3
⊢ (𝜑 → 0 ∈
ℂ) |
| 88 | | 1zzd 12648 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
| 89 | | nnuz 12921 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
| 90 | 89 | lmconst 23269 |
. . 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 23388 |
1
⊢ (𝜑 → ((
⇝𝑣 ‘𝐹) ·ih 𝐵) = 0) |