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 \in V, f \in V ⟼ (g sSet ⟨dist (ndx), f \circ -_{g}⟩) sSet ⟨TopSet (ndx), MetOpen (f \circ -_{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 \circ -_{g})$
13	8 12	cop	$class ⟨dist (ndx), f \circ -_{g}⟩$
14	4 13 5	co	$class (g sSet ⟨dist (ndx), f \circ -_{g}⟩)$
15		cts	$class TopSet$
16	7 15	cfv	$class TopSet (ndx)$
17		cmopn	$class MetOpen$
18	12 17	cfv	$class MetOpen (f \circ -_{g})$
19	16 18	cop	$class ⟨TopSet (ndx), MetOpen (f \circ -_{g})⟩$
20	14 19 5	co	$class ((g sSet ⟨dist (ndx), f \circ -_{g}⟩) sSet ⟨TopSet (ndx), MetOpen (f \circ -_{g})⟩)$
21	1 3 2 2 20	cmpo	$class (g \in V, f \in V ⟼ (g sSet ⟨dist (ndx), f \circ -_{g}⟩) sSet ⟨TopSet (ndx), MetOpen (f \circ -_{g})⟩)$
22	0 21	wceq	$wff toNrmGrp = (g \in V, f \in V ⟼ (g sSet ⟨dist (ndx), f \circ -_{g}⟩) sSet ⟨TopSet (ndx), MetOpen (f \circ -_{g})⟩)$

Metamath Proof Explorer

Definition df-tng

Detailed syntax breakdown