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

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 eqtrid 
 |-  ( ( 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 ) )