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 23943
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 23937 . 2 class toNrmGrp
2 vg . . 3 setvar ๐‘”
3 vf . . 3 setvar ๐‘“
4 cvv 3446 . . 3 class V
52cv 1541 . . . . 5 class ๐‘”
6 cnx 17066 . . . . . . 7 class ndx
7 cds 17143 . . . . . . 7 class dist
86, 7cfv 6497 . . . . . 6 class (distโ€˜ndx)
93cv 1541 . . . . . . 7 class ๐‘“
10 csg 18751 . . . . . . . 8 class -g
115, 10cfv 6497 . . . . . . 7 class (-gโ€˜๐‘”)
129, 11ccom 5638 . . . . . 6 class (๐‘“ โˆ˜ (-gโ€˜๐‘”))
138, 12cop 4593 . . . . 5 class โŸจ(distโ€˜ndx), (๐‘“ โˆ˜ (-gโ€˜๐‘”))โŸฉ
14 csts 17036 . . . . 5 class sSet
155, 13, 14co 7358 . . . 4 class (๐‘” sSet โŸจ(distโ€˜ndx), (๐‘“ โˆ˜ (-gโ€˜๐‘”))โŸฉ)
16 cts 17140 . . . . . 6 class TopSet
176, 16cfv 6497 . . . . 5 class (TopSetโ€˜ndx)
18 cmopn 20789 . . . . . 6 class MetOpen
1912, 18cfv 6497 . . . . 5 class (MetOpenโ€˜(๐‘“ โˆ˜ (-gโ€˜๐‘”)))
2017, 19cop 4593 . . . 4 class โŸจ(TopSetโ€˜ndx), (MetOpenโ€˜(๐‘“ โˆ˜ (-gโ€˜๐‘”)))โŸฉ
2115, 20, 14co 7358 . . 3 class ((๐‘” sSet โŸจ(distโ€˜ndx), (๐‘“ โˆ˜ (-gโ€˜๐‘”))โŸฉ) sSet โŸจ(TopSetโ€˜ndx), (MetOpenโ€˜(๐‘“ โˆ˜ (-gโ€˜๐‘”)))โŸฉ)
222, 3, 4, 4, 21cmpo 7360 . 2 class (๐‘” โˆˆ V, ๐‘“ โˆˆ V โ†ฆ ((๐‘” sSet โŸจ(distโ€˜ndx), (๐‘“ โˆ˜ (-gโ€˜๐‘”))โŸฉ) sSet โŸจ(TopSetโ€˜ndx), (MetOpenโ€˜(๐‘“ โˆ˜ (-gโ€˜๐‘”)))โŸฉ))
231, 22wceq 1542 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  23997  tngval  23998
  Copyright terms: Public domain W3C validator