Definition df-tng 22389

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

Distinct variable group:   f, g

Detailed syntax breakdown of Definition df-tng

Step	Hyp	Ref	Expression
1		ctng 22383	. 2 class toNrmGrp
2		vg	. . 3 setvar g
3		vf	. . 3 setvar f
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . . 5 class g
6		cnx 15854	. . . . . . 7 class ndx
7		cds 15950	. . . . . . 7 class dist
8	6, 7	cfv 5888	. . . . . 6 class ( dist ` ndx )
9	3	cv 1482	. . . . . . 7 class f
10		csg 17424	. . . . . . . 8 class -g
11	5, 10	cfv 5888	. . . . . . 7 class ( -g ` g )
12	9, 11	ccom 5118	. . . . . 6 class ( f o. ( -g ` g ) )
13	8, 12	cop 4183	. . . . 5 class <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >.
14		csts 15855	. . . . 5 class sSet
15	5, 13, 14	co 6650	. . . 4 class ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. )
16		cts 15947	. . . . . 6 class TopSet
17	6, 16	cfv 5888	. . . . 5 class (TopSet ` ndx )
18		cmopn 19736	. . . . . 6 class MetOpen
19	12, 18	cfv 5888	. . . . 5 class ( MetOpen ` ( f o. ( -g ` g ) ) )
20	17, 19	cop 4183	. . . 4 class <. (TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >.
21	15, 20, 14	co 6650	. . 3 class ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. (TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. )
22	2, 3, 4, 4, 21	cmpt2 6652	. 2 class ( g e. _V , f e. _V |-> ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. (TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) )
23	1, 22	wceq 1483	1 wff toNrmGrp = ( g e. _V , f e. _V |-> ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. (TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) )

This definition is referenced by:  reldmtng  22442  tngval  22443