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

Metamath Proof Explorer

Theorem qustgpopn

Description: A quotient map in a topological group is an open map. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses qustgp.h 
|- H = ( G /s ( G ~QG Y ) )
qustgpopn.x 
|- X = ( Base ` G )
qustgpopn.j 
|- J = ( TopOpen ` G )
qustgpopn.k 
|- K = ( TopOpen ` H )
qustgpopn.f 
|- F = ( x e. X |-> [ x ] ( G ~QG Y ) )
Assertion qustgpopn 
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> ( F " S ) e. K )

Proof

Step Hyp Ref Expression
1 qustgp.h 
 |-  H = ( G /s ( G ~QG Y ) )
2 qustgpopn.x 
 |-  X = ( Base ` G )
3 qustgpopn.j 
 |-  J = ( TopOpen ` G )
4 qustgpopn.k 
 |-  K = ( TopOpen ` H )
5 qustgpopn.f 
 |-  F = ( x e. X |-> [ x ] ( G ~QG Y ) )
6 imassrn 
 |-  ( F " S ) C_ ran F
7 1 a1i 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> H = ( G /s ( G ~QG Y ) ) )
8 2 a1i 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> X = ( Base ` G ) )
9 ovex 
 |-  ( G ~QG Y ) e. _V
10 9 a1i 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> ( G ~QG Y ) e. _V )
11 simp1 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> G e. TopGrp )
12 7 8 5 10 11 quslem 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> F : X -onto-> ( X /. ( G ~QG Y ) ) )
13 forn 
 |-  ( F : X -onto-> ( X /. ( G ~QG Y ) ) -> ran F = ( X /. ( G ~QG Y ) ) )
14 12 13 syl 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> ran F = ( X /. ( G ~QG Y ) ) )
15 6 14 sseqtrid 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> ( F " S ) C_ ( X /. ( G ~QG Y ) ) )
16 eceq1 
 |-  ( x = y -> [ x ] ( G ~QG Y ) = [ y ] ( G ~QG Y ) )
17 16 cbvmptv 
 |-  ( x e. X |-> [ x ] ( G ~QG Y ) ) = ( y e. X |-> [ y ] ( G ~QG Y ) )
18 5 17 eqtri 
 |-  F = ( y e. X |-> [ y ] ( G ~QG Y ) )
19 18 mptpreima 
 |-  ( `' F " ( F " S ) ) = { y e. X | [ y ] ( G ~QG Y ) e. ( F " S ) }
20 19 reqabi 
 |-  ( y e. ( `' F " ( F " S ) ) <-> ( y e. X /\ [ y ] ( G ~QG Y ) e. ( F " S ) ) )
21 5 funmpt2 
 |-  Fun F
22 fvelima 
 |-  ( ( Fun F /\ [ y ] ( G ~QG Y ) e. ( F " S ) ) -> E. z e. S ( F ` z ) = [ y ] ( G ~QG Y ) )
23 21 22 mpan 
 |-  ( [ y ] ( G ~QG Y ) e. ( F " S ) -> E. z e. S ( F ` z ) = [ y ] ( G ~QG Y ) )
24 3 2 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` X ) )
25 11 24 syl 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> J e. ( TopOn ` X ) )
26 simp3 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> S e. J )
27 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ S e. J ) -> S C_ X )
28 25 26 27 syl2anc 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> S C_ X )
29 28 adantr 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) -> S C_ X )
30 29 sselda 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> z e. X )
31 eceq1 
 |-  ( x = z -> [ x ] ( G ~QG Y ) = [ z ] ( G ~QG Y ) )
32 ecexg 
 |-  ( ( G ~QG Y ) e. _V -> [ z ] ( G ~QG Y ) e. _V )
33 9 32 ax-mp 
 |-  [ z ] ( G ~QG Y ) e. _V
34 31 5 33 fvmpt 
 |-  ( z e. X -> ( F ` z ) = [ z ] ( G ~QG Y ) )
35 30 34 syl 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> ( F ` z ) = [ z ] ( G ~QG Y ) )
36 35 eqeq1d 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> ( ( F ` z ) = [ y ] ( G ~QG Y ) <-> [ z ] ( G ~QG Y ) = [ y ] ( G ~QG Y ) ) )
37 eqcom 
 |-  ( [ z ] ( G ~QG Y ) = [ y ] ( G ~QG Y ) <-> [ y ] ( G ~QG Y ) = [ z ] ( G ~QG Y ) )
38 36 37 bitrdi 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> ( ( F ` z ) = [ y ] ( G ~QG Y ) <-> [ y ] ( G ~QG Y ) = [ z ] ( G ~QG Y ) ) )
39 nsgsubg 
 |-  ( Y e. ( NrmSGrp ` G ) -> Y e. ( SubGrp ` G ) )
40 39 3ad2ant2 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> Y e. ( SubGrp ` G ) )
41 40 ad2antrr 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> Y e. ( SubGrp ` G ) )
42 eqid 
 |-  ( G ~QG Y ) = ( G ~QG Y )
43 2 42 eqger 
 |-  ( Y e. ( SubGrp ` G ) -> ( G ~QG Y ) Er X )
44 41 43 syl 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> ( G ~QG Y ) Er X )
45 simplr 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> y e. X )
46 44 45 erth 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> ( y ( G ~QG Y ) z <-> [ y ] ( G ~QG Y ) = [ z ] ( G ~QG Y ) ) )
47 11 ad2antrr 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> G e. TopGrp )
48 2 subgss 
 |-  ( Y e. ( SubGrp ` G ) -> Y C_ X )
49 41 48 syl 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> Y C_ X )
50 eqid 
 |-  ( invg ` G ) = ( invg ` G )
51 eqid 
 |-  ( +g ` G ) = ( +g ` G )
52 2 50 51 42 eqgval 
 |-  ( ( G e. TopGrp /\ Y C_ X ) -> ( y ( G ~QG Y ) z <-> ( y e. X /\ z e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) ) )
53 47 49 52 syl2anc 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> ( y ( G ~QG Y ) z <-> ( y e. X /\ z e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) ) )
54 38 46 53 3bitr2d 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> ( ( F ` z ) = [ y ] ( G ~QG Y ) <-> ( y e. X /\ z e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) ) )
55 eqid 
 |-  ( oppG ` G ) = ( oppG ` G )
56 eqid 
 |-  ( +g ` ( oppG ` G ) ) = ( +g ` ( oppG ` G ) )
57 51 55 56 oppgplus 
 |-  ( ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ( +g ` ( oppG ` G ) ) a ) = ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) )
58 57 mpteq2i 
 |-  ( a e. X |-> ( ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ( +g ` ( oppG ` G ) ) a ) ) = ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) )
59 47 adantr 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> G e. TopGrp )
60 55 oppgtgp 
 |-  ( G e. TopGrp -> ( oppG ` G ) e. TopGrp )
61 59 60 syl 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( oppG ` G ) e. TopGrp )
62 49 sselda 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. X )
63 eqid 
 |-  ( a e. X |-> ( ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ( +g ` ( oppG ` G ) ) a ) ) = ( a e. X |-> ( ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ( +g ` ( oppG ` G ) ) a ) )
64 55 2 oppgbas 
 |-  X = ( Base ` ( oppG ` G ) )
65 55 3 oppgtopn 
 |-  J = ( TopOpen ` ( oppG ` G ) )
66 63 64 56 65 tgplacthmeo 
 |-  ( ( ( oppG ` G ) e. TopGrp /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. X ) -> ( a e. X |-> ( ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ( +g ` ( oppG ` G ) ) a ) ) e. ( J Homeo J ) )
67 61 62 66 syl2anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( a e. X |-> ( ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ( +g ` ( oppG ` G ) ) a ) ) e. ( J Homeo J ) )
68 58 67 eqeltrrid 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) e. ( J Homeo J ) )
69 hmeocn 
 |-  ( ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) e. ( J Homeo J ) -> ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) e. ( J Cn J ) )
70 68 69 syl 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) e. ( J Cn J ) )
71 26 ad3antrrr 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> S e. J )
72 cnima 
 |-  ( ( ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) e. ( J Cn J ) /\ S e. J ) -> ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) e. J )
73 70 71 72 syl2anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) e. J )
74 45 adantr 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> y e. X )
75 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
76 59 75 syl 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> G e. Grp )
77 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
78 2 51 77 50 grprinv 
 |-  ( ( G e. Grp /\ y e. X ) -> ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) = ( 0g ` G ) )
79 76 74 78 syl2anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) = ( 0g ` G ) )
80 79 oveq1d 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) ( +g ` G ) z ) = ( ( 0g ` G ) ( +g ` G ) z ) )
81 2 50 grpinvcl 
 |-  ( ( G e. Grp /\ y e. X ) -> ( ( invg ` G ) ` y ) e. X )
82 76 74 81 syl2anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( ( invg ` G ) ` y ) e. X )
83 30 adantr 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> z e. X )
84 2 51 grpass 
 |-  ( ( G e. Grp /\ ( y e. X /\ ( ( invg ` G ) ` y ) e. X /\ z e. X ) ) -> ( ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) ( +g ` G ) z ) = ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) )
85 76 74 82 83 84 syl13anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) ( +g ` G ) z ) = ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) )
86 2 51 77 grplid 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( 0g ` G ) ( +g ` G ) z ) = z )
87 76 83 86 syl2anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( ( 0g ` G ) ( +g ` G ) z ) = z )
88 80 85 87 3eqtr3d 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) = z )
89 simplr 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> z e. S )
90 88 89 eqeltrd 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. S )
91 oveq1 
 |-  ( a = y -> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) = ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) )
92 91 eleq1d 
 |-  ( a = y -> ( ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. S <-> ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. S ) )
93 eqid 
 |-  ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) = ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) )
94 93 mptpreima 
 |-  ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) = { a e. X | ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. S }
95 92 94 elrab2 
 |-  ( y e. ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) <-> ( y e. X /\ ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. S ) )
96 74 90 95 sylanbrc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> y e. ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) )
97 ecexg 
 |-  ( ( G ~QG Y ) e. _V -> [ x ] ( G ~QG Y ) e. _V )
98 9 97 ax-mp 
 |-  [ x ] ( G ~QG Y ) e. _V
99 98 5 fnmpti 
 |-  F Fn X
100 29 ad3antrrr 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> S C_ X )
101 fnfvima 
 |-  ( ( F Fn X /\ S C_ X /\ ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. S ) -> ( F ` ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) e. ( F " S ) )
102 101 3expia 
 |-  ( ( F Fn X /\ S C_ X ) -> ( ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. S -> ( F ` ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) e. ( F " S ) ) )
103 99 100 102 sylancr 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. S -> ( F ` ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) e. ( F " S ) ) )
104 76 adantr 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> G e. Grp )
105 simpr 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> a e. X )
106 62 adantr 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. X )
107 2 51 grpcl 
 |-  ( ( G e. Grp /\ a e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. X ) -> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. X )
108 104 105 106 107 syl3anc 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. X )
109 eceq1 
 |-  ( x = ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) -> [ x ] ( G ~QG Y ) = [ ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ] ( G ~QG Y ) )
110 109 5 98 fvmpt3i 
 |-  ( ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. X -> ( F ` ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) = [ ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ] ( G ~QG Y ) )
111 108 110 syl 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( F ` ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) = [ ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ] ( G ~QG Y ) )
112 44 ad2antrr 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( G ~QG Y ) Er X )
113 2 51 77 50 grplinv 
 |-  ( ( G e. Grp /\ a e. X ) -> ( ( ( invg ` G ) ` a ) ( +g ` G ) a ) = ( 0g ` G ) )
114 104 105 113 syl2anc 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( ( ( invg ` G ) ` a ) ( +g ` G ) a ) = ( 0g ` G ) )
115 114 oveq1d 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( ( ( ( invg ` G ) ` a ) ( +g ` G ) a ) ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) = ( ( 0g ` G ) ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) )
116 2 50 grpinvcl 
 |-  ( ( G e. Grp /\ a e. X ) -> ( ( invg ` G ) ` a ) e. X )
117 104 105 116 syl2anc 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( ( invg ` G ) ` a ) e. X )
118 2 51 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` a ) e. X /\ a e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. X ) ) -> ( ( ( ( invg ` G ) ` a ) ( +g ` G ) a ) ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) = ( ( ( invg ` G ) ` a ) ( +g ` G ) ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) )
119 104 117 105 106 118 syl13anc 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( ( ( ( invg ` G ) ` a ) ( +g ` G ) a ) ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) = ( ( ( invg ` G ) ` a ) ( +g ` G ) ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) )
120 2 51 77 grplid 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. X ) -> ( ( 0g ` G ) ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) = ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) )
121 104 106 120 syl2anc 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( ( 0g ` G ) ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) = ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) )
122 115 119 121 3eqtr3d 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( ( ( invg ` G ) ` a ) ( +g ` G ) ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) = ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) )
123 simplr 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y )
124 122 123 eqeltrd 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( ( ( invg ` G ) ` a ) ( +g ` G ) ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) e. Y )
125 49 ad2antrr 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> Y C_ X )
126 2 50 51 42 eqgval 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( a ( G ~QG Y ) ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) <-> ( a e. X /\ ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. X /\ ( ( ( invg ` G ) ` a ) ( +g ` G ) ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) e. Y ) ) )
127 104 125 126 syl2anc 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( a ( G ~QG Y ) ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) <-> ( a e. X /\ ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. X /\ ( ( ( invg ` G ) ` a ) ( +g ` G ) ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) e. Y ) ) )
128 105 108 124 127 mpbir3and 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> a ( G ~QG Y ) ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) )
129 112 128 erthi 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> [ a ] ( G ~QG Y ) = [ ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ] ( G ~QG Y ) )
130 111 129 eqtr4d 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( F ` ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) = [ a ] ( G ~QG Y ) )
131 130 eleq1d 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( ( F ` ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) e. ( F " S ) <-> [ a ] ( G ~QG Y ) e. ( F " S ) ) )
132 103 131 sylibd 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) /\ a e. X ) -> ( ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. S -> [ a ] ( G ~QG Y ) e. ( F " S ) ) )
133 132 ss2rabdv 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> { a e. X | ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. S } C_ { a e. X | [ a ] ( G ~QG Y ) e. ( F " S ) } )
134 eceq1 
 |-  ( x = a -> [ x ] ( G ~QG Y ) = [ a ] ( G ~QG Y ) )
135 134 cbvmptv 
 |-  ( x e. X |-> [ x ] ( G ~QG Y ) ) = ( a e. X |-> [ a ] ( G ~QG Y ) )
136 5 135 eqtri 
 |-  F = ( a e. X |-> [ a ] ( G ~QG Y ) )
137 136 mptpreima 
 |-  ( `' F " ( F " S ) ) = { a e. X | [ a ] ( G ~QG Y ) e. ( F " S ) }
138 133 94 137 3sstr4g 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) C_ ( `' F " ( F " S ) ) )
139 eleq2 
 |-  ( u = ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) -> ( y e. u <-> y e. ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) ) )
140 sseq1 
 |-  ( u = ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) -> ( u C_ ( `' F " ( F " S ) ) <-> ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) C_ ( `' F " ( F " S ) ) ) )
141 139 140 anbi12d 
 |-  ( u = ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) -> ( ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) <-> ( y e. ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) /\ ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) C_ ( `' F " ( F " S ) ) ) ) )
142 141 rspcev 
 |-  ( ( ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) e. J /\ ( y e. ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) /\ ( `' ( a e. X |-> ( a ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) " S ) C_ ( `' F " ( F " S ) ) ) ) -> E. u e. J ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) )
143 73 96 138 142 syl12anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> E. u e. J ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) )
144 143 3ad2antr3 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) /\ ( y e. X /\ z e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) ) -> E. u e. J ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) )
145 144 ex 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> ( ( y e. X /\ z e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> E. u e. J ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) ) )
146 54 145 sylbid 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) /\ z e. S ) -> ( ( F ` z ) = [ y ] ( G ~QG Y ) -> E. u e. J ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) ) )
147 146 rexlimdva 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) -> ( E. z e. S ( F ` z ) = [ y ] ( G ~QG Y ) -> E. u e. J ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) ) )
148 23 147 syl5 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) /\ y e. X ) -> ( [ y ] ( G ~QG Y ) e. ( F " S ) -> E. u e. J ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) ) )
149 148 expimpd 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> ( ( y e. X /\ [ y ] ( G ~QG Y ) e. ( F " S ) ) -> E. u e. J ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) ) )
150 20 149 biimtrid 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> ( y e. ( `' F " ( F " S ) ) -> E. u e. J ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) ) )
151 150 ralrimiv 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> A. y e. ( `' F " ( F " S ) ) E. u e. J ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) )
152 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
153 eltop2 
 |-  ( J e. Top -> ( ( `' F " ( F " S ) ) e. J <-> A. y e. ( `' F " ( F " S ) ) E. u e. J ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) ) )
154 25 152 153 3syl 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> ( ( `' F " ( F " S ) ) e. J <-> A. y e. ( `' F " ( F " S ) ) E. u e. J ( y e. u /\ u C_ ( `' F " ( F " S ) ) ) ) )
155 151 154 mpbird 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> ( `' F " ( F " S ) ) e. J )
156 elqtop3 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> ( X /. ( G ~QG Y ) ) ) -> ( ( F " S ) e. ( J qTop F ) <-> ( ( F " S ) C_ ( X /. ( G ~QG Y ) ) /\ ( `' F " ( F " S ) ) e. J ) ) )
157 25 12 156 syl2anc 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> ( ( F " S ) e. ( J qTop F ) <-> ( ( F " S ) C_ ( X /. ( G ~QG Y ) ) /\ ( `' F " ( F " S ) ) e. J ) ) )
158 15 155 157 mpbir2and 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> ( F " S ) e. ( J qTop F ) )
159 7 8 5 10 11 qusval 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> H = ( F "s G ) )
160 159 8 12 11 3 4 imastopn 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> K = ( J qTop F ) )
161 158 160 eleqtrrd 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ S e. J ) -> ( F " S ) e. K )