Definition df-tng 24597

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 = (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))

Distinct variable group:   𝑓,𝑔

Detailed syntax breakdown of Definition df-tng

Step	Hyp	Ref	Expression
1		ctng 24591	. 2 class toNrmGrp
2		vg	. . 3 setvar 𝑔
3		vf	. . 3 setvar 𝑓
4		cvv 3480	. . 3 class V
5	2	cv 1539	. . . . 5 class 𝑔
6		cnx 17230	. . . . . . 7 class ndx
7		cds 17306	. . . . . . 7 class dist
8	6, 7	cfv 6561	. . . . . 6 class (dist‘ndx)
9	3	cv 1539	. . . . . . 7 class 𝑓
10		csg 18953	. . . . . . . 8 class -g
11	5, 10	cfv 6561	. . . . . . 7 class (-g‘𝑔)
12	9, 11	ccom 5689	. . . . . 6 class (𝑓 ∘ (-g‘𝑔))
13	8, 12	cop 4632	. . . . 5 class ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩
14		csts 17200	. . . . 5 class sSet
15	5, 13, 14	co 7431	. . . 4 class (𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩)
16		cts 17303	. . . . . 6 class TopSet
17	6, 16	cfv 6561	. . . . 5 class (TopSet‘ndx)
18		cmopn 21354	. . . . . 6 class MetOpen
19	12, 18	cfv 6561	. . . . 5 class (MetOpen‘(𝑓 ∘ (-g‘𝑔)))
20	17, 19	cop 4632	. . . 4 class ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩
21	15, 20, 14	co 7431	. . 3 class ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩)
22	2, 3, 4, 4, 21	cmpo 7433	. 2 class (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))
23	1, 22	wceq 1540	1 wff toNrmGrp = (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))

This definition is referenced by:  reldmtng  24651  tngval  24652