| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tngbas.t | . . 3
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) | 
| 2 |  | tngtset.2 | . . 3
⊢ 𝐷 = (dist‘𝑇) | 
| 3 |  | tngtset.3 | . . 3
⊢ 𝐽 = (MetOpen‘𝐷) | 
| 4 | 1, 2, 3 | tngtset 24671 | . 2
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopSet‘𝑇)) | 
| 5 |  | df-mopn 21361 | . . . . . . . . 9
⊢ MetOpen =
(𝑥 ∈ ∪ ran ∞Met ↦ (topGen‘ran
(ball‘𝑥))) | 
| 6 | 5 | dmmptss 6260 | . . . . . . . 8
⊢ dom
MetOpen ⊆ ∪ ran ∞Met | 
| 7 | 6 | sseli 3978 | . . . . . . 7
⊢ (𝐷 ∈ dom MetOpen → 𝐷 ∈ ∪ ran ∞Met) | 
| 8 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(-g‘𝐺) = (-g‘𝐺) | 
| 9 | 1, 8 | tngds 24669 | . . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ 𝑊 → (𝑁 ∘ (-g‘𝐺)) = (dist‘𝑇)) | 
| 10 | 9, 2 | eqtr4di 2794 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ 𝑊 → (𝑁 ∘ (-g‘𝐺)) = 𝐷) | 
| 11 | 10 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (𝑁 ∘ (-g‘𝐺)) = 𝐷) | 
| 12 | 11 | dmeqd 5915 | . . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → dom (𝑁 ∘ (-g‘𝐺)) = dom 𝐷) | 
| 13 |  | dmcoss 5984 | . . . . . . . . . . . . . . 15
⊢ dom
(𝑁 ∘
(-g‘𝐺))
⊆ dom (-g‘𝐺) | 
| 14 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 15 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 16 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 17 | 14, 15, 16, 8 | grpsubfval 19002 | . . . . . . . . . . . . . . . 16
⊢
(-g‘𝐺) = (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥(+g‘𝐺)((invg‘𝐺)‘𝑦))) | 
| 18 |  | ovex 7465 | . . . . . . . . . . . . . . . 16
⊢ (𝑥(+g‘𝐺)((invg‘𝐺)‘𝑦)) ∈ V | 
| 19 | 17, 18 | dmmpo 8097 | . . . . . . . . . . . . . . 15
⊢ dom
(-g‘𝐺) =
((Base‘𝐺) ×
(Base‘𝐺)) | 
| 20 | 13, 19 | sseqtri 4031 | . . . . . . . . . . . . . 14
⊢ dom
(𝑁 ∘
(-g‘𝐺))
⊆ ((Base‘𝐺)
× (Base‘𝐺)) | 
| 21 | 12, 20 | eqsstrrdi 4028 | . . . . . . . . . . . . 13
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → dom 𝐷 ⊆ ((Base‘𝐺) × (Base‘𝐺))) | 
| 22 | 21 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) ∧ 𝐷 ∈ ∪ ran
∞Met) → dom 𝐷
⊆ ((Base‘𝐺)
× (Base‘𝐺))) | 
| 23 |  | dmss 5912 | . . . . . . . . . . . 12
⊢ (dom
𝐷 ⊆
((Base‘𝐺) ×
(Base‘𝐺)) → dom
dom 𝐷 ⊆ dom
((Base‘𝐺) ×
(Base‘𝐺))) | 
| 24 | 22, 23 | syl 17 | . . . . . . . . . . 11
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) ∧ 𝐷 ∈ ∪ ran
∞Met) → dom dom 𝐷 ⊆ dom ((Base‘𝐺) × (Base‘𝐺))) | 
| 25 |  | dmxpid 5940 | . . . . . . . . . . 11
⊢ dom
((Base‘𝐺) ×
(Base‘𝐺)) =
(Base‘𝐺) | 
| 26 | 24, 25 | sseqtrdi 4023 | . . . . . . . . . 10
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) ∧ 𝐷 ∈ ∪ ran
∞Met) → dom dom 𝐷 ⊆ (Base‘𝐺)) | 
| 27 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) ∧ 𝐷 ∈ ∪ ran
∞Met) → 𝐷 ∈
∪ ran ∞Met) | 
| 28 |  | xmetunirn 24348 | . . . . . . . . . . . 12
⊢ (𝐷 ∈ ∪ ran ∞Met ↔ 𝐷 ∈ (∞Met‘dom dom 𝐷)) | 
| 29 | 27, 28 | sylib 218 | . . . . . . . . . . 11
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) ∧ 𝐷 ∈ ∪ ran
∞Met) → 𝐷 ∈
(∞Met‘dom dom 𝐷)) | 
| 30 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) | 
| 31 | 30 | mopnuni 24452 | . . . . . . . . . . 11
⊢ (𝐷 ∈ (∞Met‘dom
dom 𝐷) → dom dom 𝐷 = ∪
(MetOpen‘𝐷)) | 
| 32 | 29, 31 | syl 17 | . . . . . . . . . 10
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) ∧ 𝐷 ∈ ∪ ran
∞Met) → dom dom 𝐷 = ∪
(MetOpen‘𝐷)) | 
| 33 | 1, 14 | tngbas 24656 | . . . . . . . . . . 11
⊢ (𝑁 ∈ 𝑊 → (Base‘𝐺) = (Base‘𝑇)) | 
| 34 | 33 | ad2antlr 727 | . . . . . . . . . 10
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) ∧ 𝐷 ∈ ∪ ran
∞Met) → (Base‘𝐺) = (Base‘𝑇)) | 
| 35 | 26, 32, 34 | 3sstr3d 4037 | . . . . . . . . 9
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) ∧ 𝐷 ∈ ∪ ran
∞Met) → ∪ (MetOpen‘𝐷) ⊆ (Base‘𝑇)) | 
| 36 |  | sspwuni 5099 | . . . . . . . . 9
⊢
((MetOpen‘𝐷)
⊆ 𝒫 (Base‘𝑇) ↔ ∪
(MetOpen‘𝐷) ⊆
(Base‘𝑇)) | 
| 37 | 35, 36 | sylibr 234 | . . . . . . . 8
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) ∧ 𝐷 ∈ ∪ ran
∞Met) → (MetOpen‘𝐷) ⊆ 𝒫 (Base‘𝑇)) | 
| 38 | 37 | ex 412 | . . . . . . 7
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (𝐷 ∈ ∪ ran
∞Met → (MetOpen‘𝐷) ⊆ 𝒫 (Base‘𝑇))) | 
| 39 | 7, 38 | syl5 34 | . . . . . 6
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (𝐷 ∈ dom MetOpen →
(MetOpen‘𝐷) ⊆
𝒫 (Base‘𝑇))) | 
| 40 |  | ndmfv 6940 | . . . . . . 7
⊢ (¬
𝐷 ∈ dom MetOpen →
(MetOpen‘𝐷) =
∅) | 
| 41 |  | 0ss 4399 | . . . . . . 7
⊢ ∅
⊆ 𝒫 (Base‘𝑇) | 
| 42 | 40, 41 | eqsstrdi 4027 | . . . . . 6
⊢ (¬
𝐷 ∈ dom MetOpen →
(MetOpen‘𝐷) ⊆
𝒫 (Base‘𝑇)) | 
| 43 | 39, 42 | pm2.61d1 180 | . . . . 5
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (MetOpen‘𝐷) ⊆ 𝒫 (Base‘𝑇)) | 
| 44 | 3, 43 | eqsstrid 4021 | . . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 ⊆ 𝒫 (Base‘𝑇)) | 
| 45 | 4, 44 | eqsstrrd 4018 | . . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (TopSet‘𝑇) ⊆ 𝒫 (Base‘𝑇)) | 
| 46 |  | eqid 2736 | . . . 4
⊢
(Base‘𝑇) =
(Base‘𝑇) | 
| 47 |  | eqid 2736 | . . . 4
⊢
(TopSet‘𝑇) =
(TopSet‘𝑇) | 
| 48 | 46, 47 | topnid 17481 | . . 3
⊢
((TopSet‘𝑇)
⊆ 𝒫 (Base‘𝑇) → (TopSet‘𝑇) = (TopOpen‘𝑇)) | 
| 49 | 45, 48 | syl 17 | . 2
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (TopSet‘𝑇) = (TopOpen‘𝑇)) | 
| 50 | 4, 49 | eqtrd 2776 | 1
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopOpen‘𝑇)) |