Metamath Proof Explorer


Definition df-tng

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)

Ref Expression
Assertion df-tng toNrmGrp = g V , f V g sSet dist ndx f - g sSet TopSet ndx MetOpen f - g

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctng class toNrmGrp
1 vg setvar g
2 cvv class V
3 vf setvar f
4 1 cv setvar g
5 csts class sSet
6 cds class dist
7 cnx class ndx
8 7 6 cfv class dist ndx
9 3 cv setvar f
10 csg class - 𝑔
11 4 10 cfv class - g
12 9 11 ccom class f - g
13 8 12 cop class dist ndx f - g
14 4 13 5 co class g sSet dist ndx f - g
15 cts class TopSet
16 7 15 cfv class TopSet ndx
17 cmopn class MetOpen
18 12 17 cfv class MetOpen f - g
19 16 18 cop class TopSet ndx MetOpen f - g
20 14 19 5 co class g sSet dist ndx f - g sSet TopSet ndx MetOpen f - g
21 1 3 2 2 20 cmpo class g V , f V g sSet dist ndx f - g sSet TopSet ndx MetOpen f - g
22 0 21 wceq wff toNrmGrp = g V , f V g sSet dist ndx f - g sSet TopSet ndx MetOpen f - g