Definition df-tng 24313

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 24307	. 2 class toNrmGrp
2		vg	. . 3 setvar 𝑔
3		vf	. . 3 setvar 𝑓
4		cvv 3474	. . 3 class V
5	2	cv 1540	. . . . 5 class 𝑔
6		cnx 17130	. . . . . . 7 class ndx
7		cds 17210	. . . . . . 7 class dist
8	6, 7	cfv 6543	. . . . . 6 class (dist‘ndx)
9	3	cv 1540	. . . . . . 7 class 𝑓
10		csg 18857	. . . . . . . 8 class -g
11	5, 10	cfv 6543	. . . . . . 7 class (-g‘𝑔)
12	9, 11	ccom 5680	. . . . . 6 class (𝑓 ∘ (-g‘𝑔))
13	8, 12	cop 4634	. . . . 5 class ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩
14		csts 17100	. . . . 5 class sSet
15	5, 13, 14	co 7411	. . . 4 class (𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩)
16		cts 17207	. . . . . 6 class TopSet
17	6, 16	cfv 6543	. . . . 5 class (TopSet‘ndx)
18		cmopn 21134	. . . . . 6 class MetOpen
19	12, 18	cfv 6543	. . . . 5 class (MetOpen‘(𝑓 ∘ (-g‘𝑔)))
20	17, 19	cop 4634	. . . 4 class ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩
21	15, 20, 14	co 7411	. . 3 class ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩)
22	2, 3, 4, 4, 21	cmpo 7413	. 2 class (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))
23	1, 22	wceq 1541	1 wff toNrmGrp = (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))

This definition is referenced by:  reldmtng  24367  tngval  24368