Definition df-tng 22199

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 22193	. 2 class toNrmGrp
2		vg	. . 3 setvar 𝑔
3		vf	. . 3 setvar 𝑓
4		cvv 3173	. . 3 class V
5	2	cv 1474	. . . . 5 class 𝑔
6		cnx 15692	. . . . . . 7 class ndx
7		cds 15777	. . . . . . 7 class dist
8	6, 7	cfv 5804	. . . . . 6 class (dist‘ndx)
9	3	cv 1474	. . . . . . 7 class 𝑓
10		csg 17247	. . . . . . . 8 class -g
11	5, 10	cfv 5804	. . . . . . 7 class (-g‘𝑔)
12	9, 11	ccom 5042	. . . . . 6 class (𝑓 ∘ (-g‘𝑔))
13	8, 12	cop 4131	. . . . 5 class ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩
14		csts 15693	. . . . 5 class sSet
15	5, 13, 14	co 6549	. . . 4 class (𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩)
16		cts 15774	. . . . . 6 class TopSet
17	6, 16	cfv 5804	. . . . 5 class (TopSet‘ndx)
18		cmopn 19557	. . . . . 6 class MetOpen
19	12, 18	cfv 5804	. . . . 5 class (MetOpen‘(𝑓 ∘ (-g‘𝑔)))
20	17, 19	cop 4131	. . . 4 class ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩
21	15, 20, 14	co 6549	. . 3 class ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩)
22	2, 3, 4, 4, 21	cmpt2 6551	. 2 class (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))
23	1, 22	wceq 1475	1 wff toNrmGrp = (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))

This definition is referenced by:  reldmtng  22252  tngval  22253