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

Metamath Proof Explorer

Theorem tgpconncomp

Description: The identity component, the connected component containing the identity element, is a closed ( conncompcld ) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypotheses tgpconncomp.x 
|- X = ( Base ` G )
tgpconncomp.z 
|- .0. = ( 0g ` G )
tgpconncomp.j 
|- J = ( TopOpen ` G )
tgpconncomp.s 
|- S = U. { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) }
Assertion tgpconncomp 
|- ( G e. TopGrp -> S e. ( NrmSGrp ` G ) )

Proof

Step Hyp Ref Expression
1 tgpconncomp.x 
 |-  X = ( Base ` G )
2 tgpconncomp.z 
 |-  .0. = ( 0g ` G )
3 tgpconncomp.j 
 |-  J = ( TopOpen ` G )
4 tgpconncomp.s 
 |-  S = U. { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) }
5 ssrab2 
 |-  { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) } C_ ~P X
6 sspwuni 
 |-  ( { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) } C_ ~P X <-> U. { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) } C_ X )
7 5 6 mpbi 
 |-  U. { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) } C_ X
8 4 7 eqsstri 
 |-  S C_ X
9 8 a1i 
 |-  ( G e. TopGrp -> S C_ X )
10 3 1 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` X ) )
11 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
12 1 2 grpidcl 
 |-  ( G e. Grp -> .0. e. X )
13 11 12 syl 
 |-  ( G e. TopGrp -> .0. e. X )
14 4 conncompid 
 |-  ( ( J e. ( TopOn ` X ) /\ .0. e. X ) -> .0. e. S )
15 10 13 14 syl2anc 
 |-  ( G e. TopGrp -> .0. e. S )
16 15 ne0d 
 |-  ( G e. TopGrp -> S =/= (/) )
17 df-ima 
 |-  ( ( z e. X |-> ( y ( -g ` G ) z ) ) " S ) = ran ( ( z e. X |-> ( y ( -g ` G ) z ) ) |` S )
18 resmpt 
 |-  ( S C_ X -> ( ( z e. X |-> ( y ( -g ` G ) z ) ) |` S ) = ( z e. S |-> ( y ( -g ` G ) z ) ) )
19 8 18 ax-mp 
 |-  ( ( z e. X |-> ( y ( -g ` G ) z ) ) |` S ) = ( z e. S |-> ( y ( -g ` G ) z ) )
20 19 rneqi 
 |-  ran ( ( z e. X |-> ( y ( -g ` G ) z ) ) |` S ) = ran ( z e. S |-> ( y ( -g ` G ) z ) )
21 17 20 eqtri 
 |-  ( ( z e. X |-> ( y ( -g ` G ) z ) ) " S ) = ran ( z e. S |-> ( y ( -g ` G ) z ) )
22 imassrn 
 |-  ( ( z e. X |-> ( y ( -g ` G ) z ) ) " S ) C_ ran ( z e. X |-> ( y ( -g ` G ) z ) )
23 11 adantr 
 |-  ( ( G e. TopGrp /\ y e. S ) -> G e. Grp )
24 23 adantr 
 |-  ( ( ( G e. TopGrp /\ y e. S ) /\ z e. X ) -> G e. Grp )
25 9 sselda 
 |-  ( ( G e. TopGrp /\ y e. S ) -> y e. X )
26 25 adantr 
 |-  ( ( ( G e. TopGrp /\ y e. S ) /\ z e. X ) -> y e. X )
27 simpr 
 |-  ( ( ( G e. TopGrp /\ y e. S ) /\ z e. X ) -> z e. X )
28 eqid 
 |-  ( -g ` G ) = ( -g ` G )
29 1 28 grpsubcl 
 |-  ( ( G e. Grp /\ y e. X /\ z e. X ) -> ( y ( -g ` G ) z ) e. X )
30 24 26 27 29 syl3anc 
 |-  ( ( ( G e. TopGrp /\ y e. S ) /\ z e. X ) -> ( y ( -g ` G ) z ) e. X )
31 30 fmpttd 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( z e. X |-> ( y ( -g ` G ) z ) ) : X --> X )
32 31 frnd 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ran ( z e. X |-> ( y ( -g ` G ) z ) ) C_ X )
33 22 32 sstrid 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( ( z e. X |-> ( y ( -g ` G ) z ) ) " S ) C_ X )
34 1 2 28 grpsubid 
 |-  ( ( G e. Grp /\ y e. X ) -> ( y ( -g ` G ) y ) = .0. )
35 23 25 34 syl2anc 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( y ( -g ` G ) y ) = .0. )
36 simpr 
 |-  ( ( G e. TopGrp /\ y e. S ) -> y e. S )
37 ovex 
 |-  ( y ( -g ` G ) y ) e. _V
38 eqid 
 |-  ( z e. S |-> ( y ( -g ` G ) z ) ) = ( z e. S |-> ( y ( -g ` G ) z ) )
39 oveq2 
 |-  ( z = y -> ( y ( -g ` G ) z ) = ( y ( -g ` G ) y ) )
40 38 39 elrnmpt1s 
 |-  ( ( y e. S /\ ( y ( -g ` G ) y ) e. _V ) -> ( y ( -g ` G ) y ) e. ran ( z e. S |-> ( y ( -g ` G ) z ) ) )
41 36 37 40 sylancl 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( y ( -g ` G ) y ) e. ran ( z e. S |-> ( y ( -g ` G ) z ) ) )
42 35 41 eqeltrrd 
 |-  ( ( G e. TopGrp /\ y e. S ) -> .0. e. ran ( z e. S |-> ( y ( -g ` G ) z ) ) )
43 42 21 eleqtrrdi 
 |-  ( ( G e. TopGrp /\ y e. S ) -> .0. e. ( ( z e. X |-> ( y ( -g ` G ) z ) ) " S ) )
44 eqid 
 |-  U. J = U. J
45 eqid 
 |-  ( +g ` G ) = ( +g ` G )
46 eqid 
 |-  ( invg ` G ) = ( invg ` G )
47 1 45 46 28 grpsubval 
 |-  ( ( y e. X /\ z e. X ) -> ( y ( -g ` G ) z ) = ( y ( +g ` G ) ( ( invg ` G ) ` z ) ) )
48 25 47 sylan 
 |-  ( ( ( G e. TopGrp /\ y e. S ) /\ z e. X ) -> ( y ( -g ` G ) z ) = ( y ( +g ` G ) ( ( invg ` G ) ` z ) ) )
49 48 mpteq2dva 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( z e. X |-> ( y ( -g ` G ) z ) ) = ( z e. X |-> ( y ( +g ` G ) ( ( invg ` G ) ` z ) ) ) )
50 1 46 grpinvcl 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( invg ` G ) ` z ) e. X )
51 23 50 sylan 
 |-  ( ( ( G e. TopGrp /\ y e. S ) /\ z e. X ) -> ( ( invg ` G ) ` z ) e. X )
52 1 46 grpinvf 
 |-  ( G e. Grp -> ( invg ` G ) : X --> X )
53 11 52 syl 
 |-  ( G e. TopGrp -> ( invg ` G ) : X --> X )
54 53 adantr 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( invg ` G ) : X --> X )
55 54 feqmptd 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( invg ` G ) = ( z e. X |-> ( ( invg ` G ) ` z ) ) )
56 eqidd 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( w e. X |-> ( y ( +g ` G ) w ) ) = ( w e. X |-> ( y ( +g ` G ) w ) ) )
57 oveq2 
 |-  ( w = ( ( invg ` G ) ` z ) -> ( y ( +g ` G ) w ) = ( y ( +g ` G ) ( ( invg ` G ) ` z ) ) )
58 51 55 56 57 fmptco 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( ( w e. X |-> ( y ( +g ` G ) w ) ) o. ( invg ` G ) ) = ( z e. X |-> ( y ( +g ` G ) ( ( invg ` G ) ` z ) ) ) )
59 49 58 eqtr4d 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( z e. X |-> ( y ( -g ` G ) z ) ) = ( ( w e. X |-> ( y ( +g ` G ) w ) ) o. ( invg ` G ) ) )
60 3 46 grpinvhmeo 
 |-  ( G e. TopGrp -> ( invg ` G ) e. ( J Homeo J ) )
61 60 adantr 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( invg ` G ) e. ( J Homeo J ) )
62 eqid 
 |-  ( w e. X |-> ( y ( +g ` G ) w ) ) = ( w e. X |-> ( y ( +g ` G ) w ) )
63 62 1 45 3 tgplacthmeo 
 |-  ( ( G e. TopGrp /\ y e. X ) -> ( w e. X |-> ( y ( +g ` G ) w ) ) e. ( J Homeo J ) )
64 25 63 syldan 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( w e. X |-> ( y ( +g ` G ) w ) ) e. ( J Homeo J ) )
65 hmeoco 
 |-  ( ( ( invg ` G ) e. ( J Homeo J ) /\ ( w e. X |-> ( y ( +g ` G ) w ) ) e. ( J Homeo J ) ) -> ( ( w e. X |-> ( y ( +g ` G ) w ) ) o. ( invg ` G ) ) e. ( J Homeo J ) )
66 61 64 65 syl2anc 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( ( w e. X |-> ( y ( +g ` G ) w ) ) o. ( invg ` G ) ) e. ( J Homeo J ) )
67 59 66 eqeltrd 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( z e. X |-> ( y ( -g ` G ) z ) ) e. ( J Homeo J ) )
68 hmeocn 
 |-  ( ( z e. X |-> ( y ( -g ` G ) z ) ) e. ( J Homeo J ) -> ( z e. X |-> ( y ( -g ` G ) z ) ) e. ( J Cn J ) )
69 67 68 syl 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( z e. X |-> ( y ( -g ` G ) z ) ) e. ( J Cn J ) )
70 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
71 10 70 syl 
 |-  ( G e. TopGrp -> X = U. J )
72 71 adantr 
 |-  ( ( G e. TopGrp /\ y e. S ) -> X = U. J )
73 8 72 sseqtrid 
 |-  ( ( G e. TopGrp /\ y e. S ) -> S C_ U. J )
74 4 conncompconn 
 |-  ( ( J e. ( TopOn ` X ) /\ .0. e. X ) -> ( J |`t S ) e. Conn )
75 10 13 74 syl2anc 
 |-  ( G e. TopGrp -> ( J |`t S ) e. Conn )
76 75 adantr 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( J |`t S ) e. Conn )
77 44 69 73 76 connima 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( J |`t ( ( z e. X |-> ( y ( -g ` G ) z ) ) " S ) ) e. Conn )
78 4 conncompss 
 |-  ( ( ( ( z e. X |-> ( y ( -g ` G ) z ) ) " S ) C_ X /\ .0. e. ( ( z e. X |-> ( y ( -g ` G ) z ) ) " S ) /\ ( J |`t ( ( z e. X |-> ( y ( -g ` G ) z ) ) " S ) ) e. Conn ) -> ( ( z e. X |-> ( y ( -g ` G ) z ) ) " S ) C_ S )
79 33 43 77 78 syl3anc 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( ( z e. X |-> ( y ( -g ` G ) z ) ) " S ) C_ S )
80 21 79 eqsstrrid 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ran ( z e. S |-> ( y ( -g ` G ) z ) ) C_ S )
81 ovex 
 |-  ( y ( -g ` G ) z ) e. _V
82 81 38 fnmpti 
 |-  ( z e. S |-> ( y ( -g ` G ) z ) ) Fn S
83 df-f 
 |-  ( ( z e. S |-> ( y ( -g ` G ) z ) ) : S --> S <-> ( ( z e. S |-> ( y ( -g ` G ) z ) ) Fn S /\ ran ( z e. S |-> ( y ( -g ` G ) z ) ) C_ S ) )
84 82 83 mpbiran 
 |-  ( ( z e. S |-> ( y ( -g ` G ) z ) ) : S --> S <-> ran ( z e. S |-> ( y ( -g ` G ) z ) ) C_ S )
85 80 84 sylibr 
 |-  ( ( G e. TopGrp /\ y e. S ) -> ( z e. S |-> ( y ( -g ` G ) z ) ) : S --> S )
86 38 fmpt 
 |-  ( A. z e. S ( y ( -g ` G ) z ) e. S <-> ( z e. S |-> ( y ( -g ` G ) z ) ) : S --> S )
87 85 86 sylibr 
 |-  ( ( G e. TopGrp /\ y e. S ) -> A. z e. S ( y ( -g ` G ) z ) e. S )
88 87 ralrimiva 
 |-  ( G e. TopGrp -> A. y e. S A. z e. S ( y ( -g ` G ) z ) e. S )
89 1 28 issubg4 
 |-  ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> ( S C_ X /\ S =/= (/) /\ A. y e. S A. z e. S ( y ( -g ` G ) z ) e. S ) ) )
90 11 89 syl 
 |-  ( G e. TopGrp -> ( S e. ( SubGrp ` G ) <-> ( S C_ X /\ S =/= (/) /\ A. y e. S A. z e. S ( y ( -g ` G ) z ) e. S ) ) )
91 9 16 88 90 mpbir3and 
 |-  ( G e. TopGrp -> S e. ( SubGrp ` G ) )
92 11 adantr 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> G e. Grp )
93 eqid 
 |-  ( oppG ` G ) = ( oppG ` G )
94 93 46 oppginv 
 |-  ( G e. Grp -> ( invg ` G ) = ( invg ` ( oppG ` G ) ) )
95 92 94 syl 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( invg ` G ) = ( invg ` ( oppG ` G ) ) )
96 95 fveq1d 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` y ) ) = ( ( invg ` ( oppG ` G ) ) ` ( ( invg ` G ) ` y ) ) )
97 simprll 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> y e. X )
98 1 46 grpinvinv 
 |-  ( ( G e. Grp /\ y e. X ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` y ) ) = y )
99 92 97 98 syl2anc 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` y ) ) = y )
100 96 99 eqtr3d 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( invg ` ( oppG ` G ) ) ` ( ( invg ` G ) ` y ) ) = y )
101 100 oveq1d 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( ( invg ` ( oppG ` G ) ) ` ( ( invg ` G ) ` y ) ) ( +g ` ( oppG ` G ) ) z ) = ( y ( +g ` ( oppG ` G ) ) z ) )
102 eqid 
 |-  ( +g ` ( oppG ` G ) ) = ( +g ` ( oppG ` G ) )
103 45 93 102 oppgplus 
 |-  ( y ( +g ` ( oppG ` G ) ) z ) = ( z ( +g ` G ) y )
104 101 103 eqtrdi 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( ( invg ` ( oppG ` G ) ) ` ( ( invg ` G ) ` y ) ) ( +g ` ( oppG ` G ) ) z ) = ( z ( +g ` G ) y ) )
105 1 46 grpinvcl 
 |-  ( ( G e. Grp /\ y e. X ) -> ( ( invg ` G ) ` y ) e. X )
106 92 97 105 syl2anc 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( invg ` G ) ` y ) e. X )
107 simprlr 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> z e. X )
108 99 oveq1d 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( ( invg ` G ) ` ( ( invg ` G ) ` y ) ) ( +g ` G ) z ) = ( y ( +g ` G ) z ) )
109 simprr 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( y ( +g ` G ) z ) e. S )
110 108 109 eqeltrd 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( ( invg ` G ) ` ( ( invg ` G ) ` y ) ) ( +g ` G ) z ) e. S )
111 eqid 
 |-  ( G ~QG S ) = ( G ~QG S )
112 1 46 45 111 eqgval 
 |-  ( ( G e. Grp /\ S C_ X ) -> ( ( ( invg ` G ) ` y ) ( G ~QG S ) z <-> ( ( ( invg ` G ) ` y ) e. X /\ z e. X /\ ( ( ( invg ` G ) ` ( ( invg ` G ) ` y ) ) ( +g ` G ) z ) e. S ) ) )
113 92 8 112 sylancl 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( ( invg ` G ) ` y ) ( G ~QG S ) z <-> ( ( ( invg ` G ) ` y ) e. X /\ z e. X /\ ( ( ( invg ` G ) ` ( ( invg ` G ) ` y ) ) ( +g ` G ) z ) e. S ) ) )
114 106 107 110 113 mpbir3and 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( invg ` G ) ` y ) ( G ~QG S ) z )
115 1 2 3 4 111 tgpconncompeqg 
 |-  ( ( G e. TopGrp /\ ( ( invg ` G ) ` y ) e. X ) -> [ ( ( invg ` G ) ` y ) ] ( G ~QG S ) = U. { x e. ~P X | ( ( ( invg ` G ) ` y ) e. x /\ ( J |`t x ) e. Conn ) } )
116 106 115 syldan 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> [ ( ( invg ` G ) ` y ) ] ( G ~QG S ) = U. { x e. ~P X | ( ( ( invg ` G ) ` y ) e. x /\ ( J |`t x ) e. Conn ) } )
117 93 oppgtgp 
 |-  ( G e. TopGrp -> ( oppG ` G ) e. TopGrp )
118 117 adantr 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( oppG ` G ) e. TopGrp )
119 93 1 oppgbas 
 |-  X = ( Base ` ( oppG ` G ) )
120 93 2 oppgid 
 |-  .0. = ( 0g ` ( oppG ` G ) )
121 93 3 oppgtopn 
 |-  J = ( TopOpen ` ( oppG ` G ) )
122 eqid 
 |-  ( ( oppG ` G ) ~QG S ) = ( ( oppG ` G ) ~QG S )
123 119 120 121 4 122 tgpconncompeqg 
 |-  ( ( ( oppG ` G ) e. TopGrp /\ ( ( invg ` G ) ` y ) e. X ) -> [ ( ( invg ` G ) ` y ) ] ( ( oppG ` G ) ~QG S ) = U. { x e. ~P X | ( ( ( invg ` G ) ` y ) e. x /\ ( J |`t x ) e. Conn ) } )
124 118 106 123 syl2anc 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> [ ( ( invg ` G ) ` y ) ] ( ( oppG ` G ) ~QG S ) = U. { x e. ~P X | ( ( ( invg ` G ) ` y ) e. x /\ ( J |`t x ) e. Conn ) } )
125 116 124 eqtr4d 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> [ ( ( invg ` G ) ` y ) ] ( G ~QG S ) = [ ( ( invg ` G ) ` y ) ] ( ( oppG ` G ) ~QG S ) )
126 125 eleq2d 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( z e. [ ( ( invg ` G ) ` y ) ] ( G ~QG S ) <-> z e. [ ( ( invg ` G ) ` y ) ] ( ( oppG ` G ) ~QG S ) ) )
127 vex 
 |-  z e. _V
128 fvex 
 |-  ( ( invg ` G ) ` y ) e. _V
129 127 128 elec 
 |-  ( z e. [ ( ( invg ` G ) ` y ) ] ( G ~QG S ) <-> ( ( invg ` G ) ` y ) ( G ~QG S ) z )
130 127 128 elec 
 |-  ( z e. [ ( ( invg ` G ) ` y ) ] ( ( oppG ` G ) ~QG S ) <-> ( ( invg ` G ) ` y ) ( ( oppG ` G ) ~QG S ) z )
131 126 129 130 3bitr3g 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( ( invg ` G ) ` y ) ( G ~QG S ) z <-> ( ( invg ` G ) ` y ) ( ( oppG ` G ) ~QG S ) z ) )
132 114 131 mpbid 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( invg ` G ) ` y ) ( ( oppG ` G ) ~QG S ) z )
133 eqid 
 |-  ( invg ` ( oppG ` G ) ) = ( invg ` ( oppG ` G ) )
134 119 133 102 122 eqgval 
 |-  ( ( ( oppG ` G ) e. TopGrp /\ S C_ X ) -> ( ( ( invg ` G ) ` y ) ( ( oppG ` G ) ~QG S ) z <-> ( ( ( invg ` G ) ` y ) e. X /\ z e. X /\ ( ( ( invg ` ( oppG ` G ) ) ` ( ( invg ` G ) ` y ) ) ( +g ` ( oppG ` G ) ) z ) e. S ) ) )
135 118 8 134 sylancl 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( ( invg ` G ) ` y ) ( ( oppG ` G ) ~QG S ) z <-> ( ( ( invg ` G ) ` y ) e. X /\ z e. X /\ ( ( ( invg ` ( oppG ` G ) ) ` ( ( invg ` G ) ` y ) ) ( +g ` ( oppG ` G ) ) z ) e. S ) ) )
136 132 135 mpbid 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( ( invg ` G ) ` y ) e. X /\ z e. X /\ ( ( ( invg ` ( oppG ` G ) ) ` ( ( invg ` G ) ` y ) ) ( +g ` ( oppG ` G ) ) z ) e. S ) )
137 136 simp3d 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( ( ( invg ` ( oppG ` G ) ) ` ( ( invg ` G ) ` y ) ) ( +g ` ( oppG ` G ) ) z ) e. S )
138 104 137 eqeltrrd 
 |-  ( ( G e. TopGrp /\ ( ( y e. X /\ z e. X ) /\ ( y ( +g ` G ) z ) e. S ) ) -> ( z ( +g ` G ) y ) e. S )
139 138 expr 
 |-  ( ( G e. TopGrp /\ ( y e. X /\ z e. X ) ) -> ( ( y ( +g ` G ) z ) e. S -> ( z ( +g ` G ) y ) e. S ) )
140 139 ralrimivva 
 |-  ( G e. TopGrp -> A. y e. X A. z e. X ( ( y ( +g ` G ) z ) e. S -> ( z ( +g ` G ) y ) e. S ) )
141 1 45 isnsg2 
 |-  ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. y e. X A. z e. X ( ( y ( +g ` G ) z ) e. S -> ( z ( +g ` G ) y ) e. S ) ) )
142 91 140 141 sylanbrc 
 |-  ( G e. TopGrp -> S e. ( NrmSGrp ` G ) )