Definition df-tng 24896

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 24890	. 2 class toNrmGrp
2		vg	. . 3 setvar 𝑔
3		vf	. . 3 setvar 𝑓
4		cvv 3451	. . 3 class V
5	2	cv 1569	. . . . 5 class 𝑔
6		cnx 17364	. . . . . . 7 class ndx
7		cds 17430	. . . . . . 7 class dist
8	6, 7	cfv 6537	. . . . . 6 class (dist‘ndx)
9	3	cv 1569	. . . . . . 7 class 𝑓
10		csg 19139	. . . . . . . 8 class -g
11	5, 10	cfv 6537	. . . . . . 7 class (-g‘𝑔)
12	9, 11	ccom 5655	. . . . . 6 class (𝑓 ∘ (-g‘𝑔))
13	8, 12	cop 4590	. . . . 5 class ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩
14		csts 17334	. . . . 5 class sSet
15	5, 13, 14	co 7418	. . . 4 class (𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩)
16		cts 17427	. . . . . 6 class TopSet
17	6, 16	cfv 6537	. . . . 5 class (TopSet‘ndx)
18		cmopn 21661	. . . . . 6 class MetOpen
19	12, 18	cfv 6537	. . . . 5 class (MetOpen‘(𝑓 ∘ (-g‘𝑔)))
20	17, 19	cop 4590	. . . 4 class ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩
21	15, 20, 14	co 7418	. . 3 class ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩)
22	2, 3, 4, 4, 21	cmpo 7420	. 2 class (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))
23	1, 22	wceq 1570	1 wff toNrmGrp = (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))

This definition is used by:  reldmtng  24950  tngval  24951