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 simpr
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> D e. U. ran *Met )
28 xmetunirn
 |-  ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) )
29 27 28 sylib
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> D e. ( *Met ` dom dom D ) )
30 eqid
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
31 30 mopnuni
 |-  ( D e. ( *Met ` dom dom D ) -> dom dom D = U. ( MetOpen ` D ) )
32 29 31 syl
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> dom dom D = U. ( MetOpen ` D ) )
33 1 14 tngbas
 |-  ( N e. W -> ( Base ` G ) = ( Base ` T ) )
34 33 ad2antlr
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> ( Base ` G ) = ( Base ` T ) )
35 26 32 34 3sstr3d
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> U. ( MetOpen ` D ) C_ ( Base ` T ) )
36 sspwuni
 |-  ( ( MetOpen ` D ) C_ ~P ( Base ` T ) <-> U. ( MetOpen ` D ) C_ ( Base ` T ) )
37 35 36 sylibr
 |-  ( ( ( G e. V /\ N e. W ) /\ D e. U. ran *Met ) -> ( MetOpen ` D ) C_ ~P ( Base ` T ) )
38 37 ex
 |-  ( ( G e. V /\ N e. W ) -> ( D e. U. ran *Met -> ( MetOpen ` D ) C_ ~P ( Base ` T ) ) )
39 7 38 syl5
 |-  ( ( G e. V /\ N e. W ) -> ( D e. dom MetOpen -> ( MetOpen ` D ) C_ ~P ( Base ` T ) ) )
40 ndmfv
 |-  ( -. D e. dom MetOpen -> ( MetOpen ` D ) = (/) )
41 0ss
 |-  (/) C_ ~P ( Base ` T )
42 40 41 eqsstrdi
 |-  ( -. D e. dom MetOpen -> ( MetOpen ` D ) C_ ~P ( Base ` T ) )
43 39 42 pm2.61d1
 |-  ( ( G e. V /\ N e. W ) -> ( MetOpen ` D ) C_ ~P ( Base ` T ) )
44 3 43 eqsstrid
 |-  ( ( G e. V /\ N e. W ) -> J C_ ~P ( Base ` T ) )
45 4 44 eqsstrrd
 |-  ( ( G e. V /\ N e. W ) -> ( TopSet ` T ) C_ ~P ( Base ` T ) )
46 eqid
 |-  ( Base ` T ) = ( Base ` T )
47 eqid
 |-  ( TopSet ` T ) = ( TopSet ` T )
48 46 47 topnid
 |-  ( ( TopSet ` T ) C_ ~P ( Base ` T ) -> ( TopSet ` T ) = ( TopOpen ` T ) )
49 45 48 syl
 |-  ( ( G e. V /\ N e. W ) -> ( TopSet ` T ) = ( TopOpen ` T ) )
50 4 49 eqtrd
 |-  ( ( G e. V /\ N e. W ) -> J = ( TopOpen ` T ) )