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 ) ) ) >. ) )