Definition df-tng 23749

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 23743	. 2 class toNrmGrp
2		vg	. . 3 setvar 𝑔
3		vf	. . 3 setvar 𝑓
4		cvv 3433	. . 3 class V
5	2	cv 1538	. . . . 5 class 𝑔
6		cnx 16903	. . . . . . 7 class ndx
7		cds 16980	. . . . . . 7 class dist
8	6, 7	cfv 6437	. . . . . 6 class (dist‘ndx)
9	3	cv 1538	. . . . . . 7 class 𝑓
10		csg 18588	. . . . . . . 8 class -g
11	5, 10	cfv 6437	. . . . . . 7 class (-g‘𝑔)
12	9, 11	ccom 5594	. . . . . 6 class (𝑓 ∘ (-g‘𝑔))
13	8, 12	cop 4568	. . . . 5 class ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩
14		csts 16873	. . . . 5 class sSet
15	5, 13, 14	co 7284	. . . 4 class (𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩)
16		cts 16977	. . . . . 6 class TopSet
17	6, 16	cfv 6437	. . . . 5 class (TopSet‘ndx)
18		cmopn 20596	. . . . . 6 class MetOpen
19	12, 18	cfv 6437	. . . . 5 class (MetOpen‘(𝑓 ∘ (-g‘𝑔)))
20	17, 19	cop 4568	. . . 4 class ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩
21	15, 20, 14	co 7284	. . 3 class ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩)
22	2, 3, 4, 4, 21	cmpo 7286	. 2 class (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))
23	1, 22	wceq 1539	1 wff toNrmGrp = (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))

This definition is referenced by:  reldmtng  23803  tngval  23804