This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑔 ) ) ) ⟩ ) )