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 ) )