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 e. _V , f e. _V |-> ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctng
 |-  toNrmGrp
1 vg
 |-  g
2 cvv
 |-  _V
3 vf
 |-  f
4 1 cv
 |-  g
5 csts
 |-  sSet
6 cds
 |-  dist
7 cnx
 |-  ndx
8 7 6 cfv
 |-  ( dist ` ndx )
9 3 cv
 |-  f
10 csg
 |-  -g
11 4 10 cfv
 |-  ( -g ` g )
12 9 11 ccom
 |-  ( f o. ( -g ` g ) )
13 8 12 cop
 |-  <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >.
14 4 13 5 co
 |-  ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. )
15 cts
 |-  TopSet
16 7 15 cfv
 |-  ( TopSet ` ndx )
17 cmopn
 |-  MetOpen
18 12 17 cfv
 |-  ( MetOpen ` ( f o. ( -g ` g ) ) )
19 16 18 cop
 |-  <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >.
20 14 19 5 co
 |-  ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. )
21 1 3 2 2 20 cmpo
 |-  ( g e. _V , f e. _V |-> ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) )
22 0 21 wceq
 |-  toNrmGrp = ( g e. _V , f e. _V |-> ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) )