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 e. V /\ N e. 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 o. ( -g ` G ) ) >. ) e. _V
5 fvex
 |-  ( MetOpen ` ( N o. ( -g ` G ) ) ) e. _V
6 tsetid
 |-  TopSet = Slot ( TopSet ` ndx )
7 6 setsid
 |-  ( ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) e. _V /\ ( MetOpen ` ( N o. ( -g ` G ) ) ) e. _V ) -> ( MetOpen ` ( N o. ( -g ` G ) ) ) = ( TopSet ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) ) )
8 4 5 7 mp2an
 |-  ( MetOpen ` ( N o. ( -g ` G ) ) ) = ( TopSet ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) )
9 eqid
 |-  ( -g ` G ) = ( -g ` G )
10 1 9 tngds
 |-  ( N e. W -> ( N o. ( -g ` G ) ) = ( dist ` T ) )
11 2 10 eqtr4id
 |-  ( N e. W -> D = ( N o. ( -g ` G ) ) )
12 11 adantl
 |-  ( ( G e. V /\ N e. W ) -> D = ( N o. ( -g ` G ) ) )
13 12 fveq2d
 |-  ( ( G e. V /\ N e. W ) -> ( MetOpen ` D ) = ( MetOpen ` ( N o. ( -g ` G ) ) ) )
14 3 13 syl5eq
 |-  ( ( G e. V /\ N e. W ) -> J = ( MetOpen ` ( N o. ( -g ` G ) ) ) )
15 eqid
 |-  ( N o. ( -g ` G ) ) = ( N o. ( -g ` G ) )
16 eqid
 |-  ( MetOpen ` ( N o. ( -g ` G ) ) ) = ( MetOpen ` ( N o. ( -g ` G ) ) )
17 1 9 15 16 tngval
 |-  ( ( G e. V /\ N e. W ) -> T = ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) )
18 17 fveq2d
 |-  ( ( G e. V /\ N e. W ) -> ( TopSet ` T ) = ( TopSet ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) ) )
19 8 14 18 3eqtr4a
 |-  ( ( G e. V /\ N e. W ) -> J = ( TopSet ` T ) )