Metamath Proof Explorer

Theorem tngtopn

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

Ref Expression
Hypotheses tngbas.t 
|- T = ( G toNrmGrp N )
tngtset.2 
|- D = ( dist ` T )
tngtset.3 
|- J = ( MetOpen ` D )
Assertion tngtopn 
|- ( ( G e. V /\ N e. W ) -> J = ( TopOpen ` 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 1 2 3 tngtset 
 |-  ( ( G e. V /\ N e. W ) -> J = ( TopSet ` T ) )
5 df-mopn 
 |-  MetOpen = ( x e. U. ran *Met |-> ( topGen ` ran ( ball ` x ) ) )
6 5 dmmptss 
 |-  dom MetOpen C_ U. ran *Met
7 6 sseli 
 |-  ( D e. dom MetOpen -> D e. U. ran *Met )
8 eqid 
 |-  ( -g ` G ) = ( -g ` G )
9 1 8 tngds 
 |-  ( N e. W -> ( N o. ( -g ` G ) ) = ( dist ` T ) )
10 9 2 eqtr4di 
 |-  ( N e. W -> ( N o. ( -g ` G ) ) = D )
11 10 adantl 
 |-  ( ( G e. V /\ N e. W ) -> ( N o. ( -g ` G ) ) = D )
12 11 dmeqd 
 |-  ( ( G e. V /\ N e. W ) -> dom ( N o. ( -g ` G ) ) = dom D )
13 dmcoss 
 |-  dom ( N o. ( -g ` G ) ) C_ dom ( -g ` G )
14 eqid 
 |-  ( Base ` G ) = ( Base ` G )
15 eqid 
 |-  ( +g ` G ) = ( +g ` G )
16 eqid 
 |-  ( invg ` G ) = ( invg ` G )
17 14 15 16 8 grpsubfval 
 |-  ( -g ` G ) = ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x ( +g ` G ) ( ( invg ` G ) ` y ) ) )
18 ovex 
 |-  ( x ( +g ` G ) ( ( invg ` G ) ` y ) ) e. _V
19 17 18 dmmpo 
 |-  dom ( -g ` G ) = ( ( Base ` G ) X. ( Base ` G ) )
20 13 19 sseqtri 
 |-  dom ( N o. ( -g ` G ) ) C_ ( ( Base ` G ) X. ( Base ` G ) )
21 12 20 eqsstrrdi 
 |-  ( ( G e. V /\ N e. W ) -> dom D C_ ( ( Base ` G ) X. ( Base ` G ) ) )
22 21 adantr 
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> dom D C_ ( ( Base ` G ) X. ( Base ` G ) ) )
23 dmss 
 |-  ( dom D C_ ( ( Base ` G ) X. ( Base ` G ) ) -> dom dom D C_ dom ( ( Base ` G ) X. ( Base ` G ) ) )
24 22 23 syl 
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> dom dom D C_ dom ( ( Base ` G ) X. ( Base ` G ) ) )
25 dmxpid 
 |-  dom ( ( Base ` G ) X. ( Base ` G ) ) = ( Base ` G )
26 24 25 sseqtrdi 
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> dom dom D C_ ( Base ` G ) )
27 xmetunirn 
 |-  ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) )
28 27 bilani 
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> D e. ( *Met ` dom dom D ) )
29 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
30 29 mopnuni 
 |-  ( D e. ( *Met ` dom dom D ) -> dom dom D = U. ( MetOpen ` D ) )
31 28 30 syl 
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> dom dom D = U. ( MetOpen ` D ) )
32 1 14 tngbas 
 |-  ( N e. W -> ( Base ` G ) = ( Base ` T ) )
33 32 ad2antlr 
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> ( Base ` G ) = ( Base ` T ) )
34 26 31 33 3sstr3d 
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> U. ( MetOpen ` D ) C_ ( Base ` T ) )
35 sspwuni 
 |-  ( ( MetOpen ` D ) C_ ~P ( Base ` T ) <-> U. ( MetOpen ` D ) C_ ( Base ` T ) )
36 34 35 sylibr 
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> ( MetOpen ` D ) C_ ~P ( Base ` T ) )
37 36 ex 
 |-  ( ( G e. V /\ N e. W ) -> ( D e. U. ran *Met -> ( MetOpen ` D ) C_ ~P ( Base ` T ) ) )
38 7 37 syl5 
 |-  ( ( G e. V /\ N e. W ) -> ( D e. dom MetOpen -> ( MetOpen ` D ) C_ ~P ( Base ` T ) ) )
39 ndmfv 
 |-  ( -. D e. dom MetOpen -> ( MetOpen ` D ) = (/) )
40 0ss 
 |-  (/) C_ ~P ( Base ` T )
41 39 40 eqsstrdi 
 |-  ( -. D e. dom MetOpen -> ( MetOpen ` D ) C_ ~P ( Base ` T ) )
42 38 41 pm2.61d1 
 |-  ( ( G e. V /\ N e. W ) -> ( MetOpen ` D ) C_ ~P ( Base ` T ) )
43 3 42 eqsstrid 
 |-  ( ( G e. V /\ N e. W ) -> J C_ ~P ( Base ` T ) )
44 4 43 eqsstrrd 
 |-  ( ( G e. V /\ N e. W ) -> ( TopSet ` T ) C_ ~P ( Base ` T ) )
45 eqid 
 |-  ( Base ` T ) = ( Base ` T )
46 eqid 
 |-  ( TopSet ` T ) = ( TopSet ` T )
47 45 46 topnid 
 |-  ( ( TopSet ` T ) C_ ~P ( Base ` T ) -> ( TopSet ` T ) = ( TopOpen ` T ) )
48 44 47 syl 
 |-  ( ( G e. V /\ N e. W ) -> ( TopSet ` T ) = ( TopOpen ` T ) )
49 4 48 eqtrd 
 |-  ( ( G e. V /\ N e. W ) -> J = ( TopOpen ` T ) )