MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tng Structured version   Visualization version   GIF version

Definition df-tng 22590
Description: Define a function that fills in the topology and metric components of a structure given a group and a norm on it. (Contributed by Mario Carneiro, 2-Oct-2015.)
Assertion
Ref Expression
df-tng toNrmGrp = (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g𝑔)))⟩))
Distinct variable group:   𝑓,𝑔

Detailed syntax breakdown of Definition df-tng
StepHypRef Expression
1 ctng 22584 . 2 class toNrmGrp
2 vg . . 3 setvar 𝑔
3 vf . . 3 setvar 𝑓
4 cvv 3340 . . 3 class V
52cv 1631 . . . . 5 class 𝑔
6 cnx 16056 . . . . . . 7 class ndx
7 cds 16152 . . . . . . 7 class dist
86, 7cfv 6049 . . . . . 6 class (dist‘ndx)
93cv 1631 . . . . . . 7 class 𝑓
10 csg 17625 . . . . . . . 8 class -g
115, 10cfv 6049 . . . . . . 7 class (-g𝑔)
129, 11ccom 5270 . . . . . 6 class (𝑓 ∘ (-g𝑔))
138, 12cop 4327 . . . . 5 class ⟨(dist‘ndx), (𝑓 ∘ (-g𝑔))⟩
14 csts 16057 . . . . 5 class sSet
155, 13, 14co 6813 . . . 4 class (𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g𝑔))⟩)
16 cts 16149 . . . . . 6 class TopSet
176, 16cfv 6049 . . . . 5 class (TopSet‘ndx)
18 cmopn 19938 . . . . . 6 class MetOpen
1912, 18cfv 6049 . . . . 5 class (MetOpen‘(𝑓 ∘ (-g𝑔)))
2017, 19cop 4327 . . . 4 class ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g𝑔)))⟩
2115, 20, 14co 6813 . . 3 class ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g𝑔)))⟩)
222, 3, 4, 4, 21cmpt2 6815 . 2 class (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g𝑔)))⟩))
231, 22wceq 1632 1 wff toNrmGrp = (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g𝑔)))⟩))
Colors of variables: wff setvar class
This definition is referenced by:  reldmtng  22643  tngval  22644
  Copyright terms: Public domain W3C validator