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

Definition df-tng 18637
 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 sSet sSet TopSet
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-tng
StepHypRef Expression
1 ctng 18631 . 2 toNrmGrp
2 vg . . 3
3 vf . . 3
4 cvv 2958 . . 3
52cv 1652 . . . . 5
6 cnx 13471 . . . . . . 7
7 cds 13543 . . . . . . 7
86, 7cfv 5457 . . . . . 6
93cv 1652 . . . . . . 7
10 csg 14693 . . . . . . . 8
115, 10cfv 5457 . . . . . . 7
129, 11ccom 4885 . . . . . 6
138, 12cop 3819 . . . . 5
14 csts 13472 . . . . 5 sSet
155, 13, 14co 6084 . . . 4 sSet
16 cts 13540 . . . . . 6 TopSet
176, 16cfv 5457 . . . . 5 TopSet
18 cmopn 16696 . . . . . 6
1912, 18cfv 5457 . . . . 5
2017, 19cop 3819 . . . 4 TopSet
2115, 20, 14co 6084 . . 3 sSet sSet TopSet
222, 3, 4, 4, 21cmpt2 6086 . 2 sSet sSet TopSet
231, 22wceq 1653 1 toNrmGrp sSet sSet TopSet
 Colors of variables: wff set class This definition is referenced by:  reldmtng  18684  tngval  18685
 Copyright terms: Public domain W3C validator