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

Metamath Proof Explorer

Theorem subgtgp

Description: A subgroup of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypothesis subgtgp.h 
|- H = ( G |`s S )
Assertion subgtgp 
|- ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> H e. TopGrp )

Proof

Step Hyp Ref Expression
1 subgtgp.h 
 |-  H = ( G |`s S )
2 1 subggrp 
 |-  ( S e. ( SubGrp ` G ) -> H e. Grp )
3 2 adantl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> H e. Grp )
4 tgptmd 
 |-  ( G e. TopGrp -> G e. TopMnd )
5 subgsubm 
 |-  ( S e. ( SubGrp ` G ) -> S e. ( SubMnd ` G ) )
6 1 submtmd 
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> H e. TopMnd )
7 4 5 6 syl2an 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> H e. TopMnd )
8 1 subgbas 
 |-  ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) )
9 8 adantl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> S = ( Base ` H ) )
10 9 mpteq1d 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( x e. S |-> ( ( invg ` H ) ` x ) ) = ( x e. ( Base ` H ) |-> ( ( invg ` H ) ` x ) ) )
11 eqid 
 |-  ( invg ` G ) = ( invg ` G )
12 eqid 
 |-  ( invg ` H ) = ( invg ` H )
13 1 11 12 subginv 
 |-  ( ( S e. ( SubGrp ` G ) /\ x e. S ) -> ( ( invg ` G ) ` x ) = ( ( invg ` H ) ` x ) )
14 13 adantll 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) /\ x e. S ) -> ( ( invg ` G ) ` x ) = ( ( invg ` H ) ` x ) )
15 14 mpteq2dva 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( x e. S |-> ( ( invg ` G ) ` x ) ) = ( x e. S |-> ( ( invg ` H ) ` x ) ) )
16 eqid 
 |-  ( Base ` H ) = ( Base ` H )
17 16 12 grpinvf 
 |-  ( H e. Grp -> ( invg ` H ) : ( Base ` H ) --> ( Base ` H ) )
18 3 17 syl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( invg ` H ) : ( Base ` H ) --> ( Base ` H ) )
19 18 feqmptd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( invg ` H ) = ( x e. ( Base ` H ) |-> ( ( invg ` H ) ` x ) ) )
20 10 15 19 3eqtr4rd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( invg ` H ) = ( x e. S |-> ( ( invg ` G ) ` x ) ) )
21 eqid 
 |-  ( ( TopOpen ` G ) |`t S ) = ( ( TopOpen ` G ) |`t S )
22 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
23 eqid 
 |-  ( Base ` G ) = ( Base ` G )
24 22 23 tgptopon 
 |-  ( G e. TopGrp -> ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) )
25 24 adantr 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) )
26 23 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
27 26 adantl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> S C_ ( Base ` G ) )
28 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
29 28 adantr 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> G e. Grp )
30 23 11 grpinvf 
 |-  ( G e. Grp -> ( invg ` G ) : ( Base ` G ) --> ( Base ` G ) )
31 29 30 syl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( invg ` G ) : ( Base ` G ) --> ( Base ` G ) )
32 31 feqmptd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( invg ` G ) = ( x e. ( Base ` G ) |-> ( ( invg ` G ) ` x ) ) )
33 22 11 tgpinv 
 |-  ( G e. TopGrp -> ( invg ` G ) e. ( ( TopOpen ` G ) Cn ( TopOpen ` G ) ) )
34 33 adantr 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( invg ` G ) e. ( ( TopOpen ` G ) Cn ( TopOpen ` G ) ) )
35 32 34 eqeltrrd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( x e. ( Base ` G ) |-> ( ( invg ` G ) ` x ) ) e. ( ( TopOpen ` G ) Cn ( TopOpen ` G ) ) )
36 21 25 27 35 cnmpt1res 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( x e. S |-> ( ( invg ` G ) ` x ) ) e. ( ( ( TopOpen ` G ) |`t S ) Cn ( TopOpen ` G ) ) )
37 20 36 eqeltrd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( invg ` H ) e. ( ( ( TopOpen ` G ) |`t S ) Cn ( TopOpen ` G ) ) )
38 18 frnd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ran ( invg ` H ) C_ ( Base ` H ) )
39 38 9 sseqtrrd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ran ( invg ` H ) C_ S )
40 cnrest2 
 |-  ( ( ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) /\ ran ( invg ` H ) C_ S /\ S C_ ( Base ` G ) ) -> ( ( invg ` H ) e. ( ( ( TopOpen ` G ) |`t S ) Cn ( TopOpen ` G ) ) <-> ( invg ` H ) e. ( ( ( TopOpen ` G ) |`t S ) Cn ( ( TopOpen ` G ) |`t S ) ) ) )
41 25 39 27 40 syl3anc 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( invg ` H ) e. ( ( ( TopOpen ` G ) |`t S ) Cn ( TopOpen ` G ) ) <-> ( invg ` H ) e. ( ( ( TopOpen ` G ) |`t S ) Cn ( ( TopOpen ` G ) |`t S ) ) ) )
42 37 41 mpbid 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( invg ` H ) e. ( ( ( TopOpen ` G ) |`t S ) Cn ( ( TopOpen ` G ) |`t S ) ) )
43 1 22 resstopn 
 |-  ( ( TopOpen ` G ) |`t S ) = ( TopOpen ` H )
44 43 12 istgp 
 |-  ( H e. TopGrp <-> ( H e. Grp /\ H e. TopMnd /\ ( invg ` H ) e. ( ( ( TopOpen ` G ) |`t S ) Cn ( ( TopOpen ` G ) |`t S ) ) ) )
45 3 7 42 44 syl3anbrc 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> H e. TopGrp )