Definition df-tng

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)

	Ref	Expression
Assertion	df-tng	⊢ toNrmGrp = ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ( ( 𝑔 sSet ⟨ ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ) ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctng	⊢ toNrmGrp
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vf	⊢ 𝑓
4	1	cv	⊢ 𝑔
5		csts	⊢ sSet
6		cds	⊢ dist
7		cnx	⊢ ndx
8	7 6	cfv	⊢ ( dist ‘ ndx )
9	3	cv	⊢ 𝑓
10		csg	⊢ -g
11	4 10	cfv	⊢ ( -g ‘ 𝑔 )
12	9 11	ccom	⊢ ( 𝑓 ∘ ( -g ‘ 𝑔 ) )
13	8 12	cop	⊢ ⟨ ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ⟩
14	4 13 5	co	⊢ ( 𝑔 sSet ⟨ ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ⟩ )
15		cts	⊢ TopSet
16	7 15	cfv	⊢ ( TopSet ‘ ndx )
17		cmopn	⊢ MetOpen
18	12 17	cfv	⊢ ( MetOpen ‘ ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) )
19	16 18	cop	⊢ ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ) ⟩
20	14 19 5	co	⊢ ( ( 𝑔 sSet ⟨ ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ) ⟩ )
21	1 3 2 2 20	cmpo	⊢ ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ( ( 𝑔 sSet ⟨ ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ) ⟩ ) )
22	0 21	wceq	⊢ toNrmGrp = ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ( ( 𝑔 sSet ⟨ ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ) ⟩ ) )