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=GtoNrmGrpN
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=GtoNrmGrpN
2 tngtset.2 ⊢D=dist⁡T
3 tngtset.3 ⊢J=MetOpen⁡D
4 ovex ⊢GsSetdist⁡ndxN∘-G∈V
5 fvex ⊢MetOpen⁡N∘-G∈V
6 tsetid ⊢TopSet=SlotTopSet⁡ndx
7 6 setsid ⊢GsSetdist⁡ndxN∘-G∈V∧MetOpen⁡N∘-G∈V→MetOpen⁡N∘-G=TopSet⁡GsSetdist⁡ndxN∘-GsSetTopSet⁡ndxMetOpen⁡N∘-G
8 4 5 7 mp2an ⊢MetOpen⁡N∘-G=TopSet⁡GsSetdist⁡ndxN∘-GsSetTopSet⁡ndxMetOpen⁡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=GsSetdist⁡ndxN∘-GsSetTopSet⁡ndxMetOpen⁡N∘-G
18 17 fveq2d ⊢G∈V∧N∈W→TopSet⁡T=TopSet⁡GsSetdist⁡ndxN∘-GsSetTopSet⁡ndxMetOpen⁡N∘-G
19 8 14 18 3eqtr4a ⊢G∈V∧N∈W→J=TopSet⁡T