Metamath Proof Explorer

Theorem clsnsg

Description: The closure of a normal subgroup is a normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypothesis subgntr.h 
|- J = ( TopOpen ` G )
Assertion clsnsg 
|- ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) -> ( ( cls ` J ) ` S ) e. ( NrmSGrp ` G ) )

Proof

Step Hyp Ref Expression
1 subgntr.h 
 |-  J = ( TopOpen ` G )
2 nsgsubg 
 |-  ( S e. ( NrmSGrp ` G ) -> S e. ( SubGrp ` G ) )
3 1 clssubg 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( cls ` J ) ` S ) e. ( SubGrp ` G ) )
4 2 3 sylan2 
 |-  ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) -> ( ( cls ` J ) ` S ) e. ( SubGrp ` G ) )
5 df-ima 
 |-  ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " ( ( cls ` J ) ` S ) ) = ran ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) |` ( ( cls ` J ) ` S ) )
6 eqid 
 |-  ( Base ` G ) = ( Base ` G )
7 1 6 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` ( Base ` G ) ) )
8 7 ad2antrr 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> J e. ( TopOn ` ( Base ` G ) ) )
9 topontop 
 |-  ( J e. ( TopOn ` ( Base ` G ) ) -> J e. Top )
10 8 9 syl 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> J e. Top )
11 2 ad2antlr 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> S e. ( SubGrp ` G ) )
12 6 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
13 11 12 syl 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> S C_ ( Base ` G ) )
14 toponuni 
 |-  ( J e. ( TopOn ` ( Base ` G ) ) -> ( Base ` G ) = U. J )
15 8 14 syl 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( Base ` G ) = U. J )
16 13 15 sseqtrd 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> S C_ U. J )
17 eqid 
 |-  U. J = U. J
18 17 clsss3 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( ( cls ` J ) ` S ) C_ U. J )
19 10 16 18 syl2anc 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( ( cls ` J ) ` S ) C_ U. J )
20 19 15 sseqtrrd 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( ( cls ` J ) ` S ) C_ ( Base ` G ) )
21 20 resmptd 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) |` ( ( cls ` J ) ` S ) ) = ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) )
22 21 rneqd 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ran ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) |` ( ( cls ` J ) ` S ) ) = ran ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) )
23 5 22 eqtrid 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " ( ( cls ` J ) ` S ) ) = ran ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) )
24 eqid 
 |-  ( +g ` G ) = ( +g ` G )
25 tgptmd 
 |-  ( G e. TopGrp -> G e. TopMnd )
26 25 ad2antrr 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> G e. TopMnd )
27 simpr 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> x e. ( Base ` G ) )
28 8 8 27 cnmptc 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( y e. ( Base ` G ) |-> x ) e. ( J Cn J ) )
29 8 cnmptid 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( y e. ( Base ` G ) |-> y ) e. ( J Cn J ) )
30 1 24 26 8 28 29 cnmpt1plusg 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( y e. ( Base ` G ) |-> ( x ( +g ` G ) y ) ) e. ( J Cn J ) )
31 eqid 
 |-  ( -g ` G ) = ( -g ` G )
32 1 31 tgpsubcn 
 |-  ( G e. TopGrp -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
33 32 ad2antrr 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
34 8 30 28 33 cnmpt12f 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) e. ( J Cn J ) )
35 17 cnclsi 
 |-  ( ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) e. ( J Cn J ) /\ S C_ U. J ) -> ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " ( ( cls ` J ) ` S ) ) C_ ( ( cls ` J ) ` ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " S ) ) )
36 34 16 35 syl2anc 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " ( ( cls ` J ) ` S ) ) C_ ( ( cls ` J ) ` ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " S ) ) )
37 df-ima 
 |-  ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " S ) = ran ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) |` S )
38 13 resmptd 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) |` S ) = ( y e. S |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) )
39 38 rneqd 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ran ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) |` S ) = ran ( y e. S |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) )
40 37 39 eqtrid 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " S ) = ran ( y e. S |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) )
41 6 24 31 nsgconj 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ x e. ( Base ` G ) /\ y e. S ) -> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. S )
42 41 ad4ant234 
 |-  ( ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) /\ y e. S ) -> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. S )
43 42 fmpttd 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( y e. S |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) : S --> S )
44 43 frnd 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ran ( y e. S |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) C_ S )
45 40 44 eqsstrd 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " S ) C_ S )
46 17 clsss 
 |-  ( ( J e. Top /\ S C_ U. J /\ ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " S ) C_ S ) -> ( ( cls ` J ) ` ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " S ) ) C_ ( ( cls ` J ) ` S ) )
47 10 16 45 46 syl3anc 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( ( cls ` J ) ` ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " S ) ) C_ ( ( cls ` J ) ` S ) )
48 36 47 sstrd 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( ( y e. ( Base ` G ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) " ( ( cls ` J ) ` S ) ) C_ ( ( cls ` J ) ` S ) )
49 23 48 eqsstrrd 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ran ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) C_ ( ( cls ` J ) ` S ) )
50 ovex 
 |-  ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. _V
51 eqid 
 |-  ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) = ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) )
52 50 51 fnmpti 
 |-  ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) Fn ( ( cls ` J ) ` S )
53 df-f 
 |-  ( ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) : ( ( cls ` J ) ` S ) --> ( ( cls ` J ) ` S ) <-> ( ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) Fn ( ( cls ` J ) ` S ) /\ ran ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) C_ ( ( cls ` J ) ` S ) ) )
54 52 53 mpbiran 
 |-  ( ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) : ( ( cls ` J ) ` S ) --> ( ( cls ` J ) ` S ) <-> ran ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) C_ ( ( cls ` J ) ` S ) )
55 49 54 sylibr 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) : ( ( cls ` J ) ` S ) --> ( ( cls ` J ) ` S ) )
56 51 fmpt 
 |-  ( A. y e. ( ( cls ` J ) ` S ) ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. ( ( cls ` J ) ` S ) <-> ( y e. ( ( cls ` J ) ` S ) |-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) ) : ( ( cls ` J ) ` S ) --> ( ( cls ` J ) ` S ) )
57 55 56 sylibr 
 |-  ( ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) /\ x e. ( Base ` G ) ) -> A. y e. ( ( cls ` J ) ` S ) ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. ( ( cls ` J ) ` S ) )
58 57 ralrimiva 
 |-  ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) -> A. x e. ( Base ` G ) A. y e. ( ( cls ` J ) ` S ) ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. ( ( cls ` J ) ` S ) )
59 6 24 31 isnsg3 
 |-  ( ( ( cls ` J ) ` S ) e. ( NrmSGrp ` G ) <-> ( ( ( cls ` J ) ` S ) e. ( SubGrp ` G ) /\ A. x e. ( Base ` G ) A. y e. ( ( cls ` J ) ` S ) ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. ( ( cls ` J ) ` S ) ) )
60 4 58 59 sylanbrc 
 |-  ( ( G e. TopGrp /\ S e. ( NrmSGrp ` G ) ) -> ( ( cls ` J ) ` S ) e. ( NrmSGrp ` G ) )