Metamath Proof Explorer

Theorem tngtset

Description: The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypotheses tngbas.t ⊢ T = G toNrmGrp N
tngtset.2 ⊢ D = dist ⁡ T
tngtset.3 ⊢ J = MetOpen ⁡ D
Assertion tngtset ⊢ G ∈ V ∧ N ∈ W → J = TopSet ⁡ T

Proof

Step Hyp Ref Expression
1 tngbas.t ⊢ T = G toNrmGrp N
2 tngtset.2 ⊢ D = dist ⁡ T
3 tngtset.3 ⊢ J = MetOpen ⁡ D
4 ovex ⊢ G sSet dist ⁡ ndx N ∘ - G ∈ V
5 fvex ⊢ MetOpen ⁡ N ∘ - G ∈ V
6 tsetid ⊢ TopSet = Slot TopSet ⁡ ndx
7 6 setsid ⊢ G sSet dist ⁡ ndx N ∘ - G ∈ V ∧ MetOpen ⁡ N ∘ - G ∈ V → MetOpen ⁡ N ∘ - G = TopSet ⁡ G sSet dist ⁡ ndx N ∘ - G sSet TopSet ⁡ ndx MetOpen ⁡ N ∘ - G
8 4 5 7 mp2an ⊢ MetOpen ⁡ N ∘ - G = TopSet ⁡ G sSet dist ⁡ ndx N ∘ - G sSet TopSet ⁡ ndx MetOpen ⁡ N ∘ - G
9 eqid ⊢ - G = - G
10 1 9 tngds ⊢ N ∈ W → N ∘ - G = dist ⁡ T
11 2 10 eqtr4id ⊢ N ∈ W → D = N ∘ - G
12 11 adantl ⊢ G ∈ V ∧ N ∈ W → D = N ∘ - G
13 12 fveq2d ⊢ G ∈ V ∧ N ∈ W → MetOpen ⁡ D = MetOpen ⁡ N ∘ - G
14 3 13 eqtrid ⊢ G ∈ V ∧ N ∈ W → J = MetOpen ⁡ N ∘ - G
15 eqid ⊢ N ∘ - G = N ∘ - G
16 eqid ⊢ MetOpen ⁡ N ∘ - G = MetOpen ⁡ N ∘ - G
17 1 9 15 16 tngval ⊢ G ∈ V ∧ N ∈ W → T = G sSet dist ⁡ ndx N ∘ - G sSet TopSet ⁡ ndx MetOpen ⁡ N ∘ - G
18 17 fveq2d ⊢ G ∈ V ∧ N ∈ W → TopSet ⁡ T = TopSet ⁡ G sSet dist ⁡ ndx N ∘ - G sSet TopSet ⁡ ndx MetOpen ⁡ N ∘ - G
19 8 14 18 3eqtr4a ⊢ G ∈ V ∧ N ∈ W → J = TopSet ⁡ T