qustgplem

	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 ) )
	qustgplem.m	\|- .- = ( z e. X , w e. X \|-> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) )
Assertion	qustgplem	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H e. TopGrp )

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		qustgplem.m	\|- .- = ( z e. X , w e. X \|-> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) )
7	1	qusgrp	\|- ( Y e. ( NrmSGrp ` G ) -> H e. Grp )
8	7	adantl	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H e. Grp )
9	1	a1i	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H = ( G /s ( G ~QG Y ) ) )
10	2	a1i	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> X = ( Base ` G ) )
11		ovex	\|- ( G ~QG Y ) e. _V
12	11	a1i	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( G ~QG Y ) e. _V )
13		simpl	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> G e. TopGrp )
14	9 10 5 12 13	qusval	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H = ( F "s G ) )
15	9 10 5 12 13	quslem	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> F : X -onto-> ( X /. ( G ~QG Y ) ) )
16	14 10 15 13 3 4	imastopn	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> K = ( J qTop F ) )
17	3 2	tgptopon	\|- ( G e. TopGrp -> J e. ( TopOn ` X ) )
18	17	adantr	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> J e. ( TopOn ` X ) )
19		qtoptopon	\|- ( ( J e. ( TopOn ` X ) /\ F : X -onto-> ( X /. ( G ~QG Y ) ) ) -> ( J qTop F ) e. ( TopOn ` ( X /. ( G ~QG Y ) ) ) )
20	18 15 19	syl2anc	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( J qTop F ) e. ( TopOn ` ( X /. ( G ~QG Y ) ) ) )
21	16 20	eqeltrd	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> K e. ( TopOn ` ( X /. ( G ~QG Y ) ) ) )
22	9 10 12 13	qusbas	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( X /. ( G ~QG Y ) ) = ( Base ` H ) )
23	22	fveq2d	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( TopOn ` ( X /. ( G ~QG Y ) ) ) = ( TopOn ` ( Base ` H ) ) )
24	21 23	eleqtrd	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> K e. ( TopOn ` ( Base ` H ) ) )
25		eqid	\|- ( Base ` H ) = ( Base ` H )
26	25 4	istps	\|- ( H e. TopSp <-> K e. ( TopOn ` ( Base ` H ) ) )
27	24 26	sylibr	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H e. TopSp )
28		eqid	\|- ( -g ` H ) = ( -g ` H )
29	25 28	grpsubf	\|- ( H e. Grp -> ( -g ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) )
30	8 29	syl	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( -g ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) )
31		cnvimass	\|- ( `' ( -g ` H ) " u ) C_ dom ( -g ` H )
32	30	fdmd	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> dom ( -g ` H ) = ( ( Base ` H ) X. ( Base ` H ) ) )
33	32	adantr	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> dom ( -g ` H ) = ( ( Base ` H ) X. ( Base ` H ) ) )
34	31 33	sseqtrid	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( `' ( -g ` H ) " u ) C_ ( ( Base ` H ) X. ( Base ` H ) ) )
35		relxp	\|- Rel ( ( Base ` H ) X. ( Base ` H ) )
36		relss	\|- ( ( `' ( -g ` H ) " u ) C_ ( ( Base ` H ) X. ( Base ` H ) ) -> ( Rel ( ( Base ` H ) X. ( Base ` H ) ) -> Rel ( `' ( -g ` H ) " u ) ) )
37	34 35 36	mpisyl	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> Rel ( `' ( -g ` H ) " u ) )
38	34	sseld	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> <. x , y >. e. ( ( Base ` H ) X. ( Base ` H ) ) ) )
39		vex	\|- x e. _V
40	39	elqs	\|- ( x e. ( X /. ( G ~QG Y ) ) <-> E. a e. X x = [ a ] ( G ~QG Y ) )
41	22	adantr	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( X /. ( G ~QG Y ) ) = ( Base ` H ) )
42	41	eleq2d	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( x e. ( X /. ( G ~QG Y ) ) <-> x e. ( Base ` H ) ) )
43	40 42	bitr3id	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( E. a e. X x = [ a ] ( G ~QG Y ) <-> x e. ( Base ` H ) ) )
44		vex	\|- y e. _V
45	44	elqs	\|- ( y e. ( X /. ( G ~QG Y ) ) <-> E. b e. X y = [ b ] ( G ~QG Y ) )
46	41	eleq2d	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( y e. ( X /. ( G ~QG Y ) ) <-> y e. ( Base ` H ) ) )
47	45 46	bitr3id	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( E. b e. X y = [ b ] ( G ~QG Y ) <-> y e. ( Base ` H ) ) )
48	43 47	anbi12d	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( ( E. a e. X x = [ a ] ( G ~QG Y ) /\ E. b e. X y = [ b ] ( G ~QG Y ) ) <-> ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) )
49		reeanv	\|- ( E. a e. X E. b e. X ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) <-> ( E. a e. X x = [ a ] ( G ~QG Y ) /\ E. b e. X y = [ b ] ( G ~QG Y ) ) )
50		opelxp	\|- ( <. x , y >. e. ( ( Base ` H ) X. ( Base ` H ) ) <-> ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) )
51	48 49 50	3bitr4g	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( E. a e. X E. b e. X ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) <-> <. x , y >. e. ( ( Base ` H ) X. ( Base ` H ) ) ) )
52	8	ad2antrr	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> H e. Grp )
53	52 29	syl	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( -g ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) )
54		ffn	\|- ( ( -g ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) -> ( -g ` H ) Fn ( ( Base ` H ) X. ( Base ` H ) ) )
55		elpreima	\|- ( ( -g ` H ) Fn ( ( Base ` H ) X. ( Base ` H ) ) -> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) <-> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) /\ ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. ) e. u ) ) )
56	53 54 55	3syl	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) <-> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) /\ ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. ) e. u ) ) )
57		df-ov	\|- ( [ a ] ( G ~QG Y ) ( -g ` H ) [ b ] ( G ~QG Y ) ) = ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. )
58		simpllr	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> Y e. ( NrmSGrp ` G ) )
59		simprl	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> a e. X )
60		simprr	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> b e. X )
61		eqid	\|- ( -g ` G ) = ( -g ` G )
62	1 2 61 28	qussub	\|- ( ( Y e. ( NrmSGrp ` G ) /\ a e. X /\ b e. X ) -> ( [ a ] ( G ~QG Y ) ( -g ` H ) [ b ] ( G ~QG Y ) ) = [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) )
63	58 59 60 62	syl3anc	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( [ a ] ( G ~QG Y ) ( -g ` H ) [ b ] ( G ~QG Y ) ) = [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) )
64	57 63	eqtr3id	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. ) = [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) )
65	64	eleq1d	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. ) e. u <-> [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u ) )
66		simpr	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( a e. X /\ b e. X ) )
67		tgpgrp	\|- ( G e. TopGrp -> G e. Grp )
68	67	adantr	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> G e. Grp )
69	2 61	grpsubf	\|- ( G e. Grp -> ( -g ` G ) : ( X X. X ) --> X )
70		ffn	\|- ( ( -g ` G ) : ( X X. X ) --> X -> ( -g ` G ) Fn ( X X. X ) )
71	68 69 70	3syl	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( -g ` G ) Fn ( X X. X ) )
72		fnov	\|- ( ( -g ` G ) Fn ( X X. X ) <-> ( -g ` G ) = ( z e. X , w e. X \|-> ( z ( -g ` G ) w ) ) )
73	71 72	sylib	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( -g ` G ) = ( z e. X , w e. X \|-> ( z ( -g ` G ) w ) ) )
74	3 61	tgpsubcn	\|- ( G e. TopGrp -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
75	74	adantr	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
76	73 75	eqeltrrd	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( z e. X , w e. X \|-> ( z ( -g ` G ) w ) ) e. ( ( J tX J ) Cn J ) )
77		ecexg	\|- ( ( G ~QG Y ) e. _V -> [ x ] ( G ~QG Y ) e. _V )
78	11 77	ax-mp	\|- [ x ] ( G ~QG Y ) e. _V
79	78 5	fnmpti	\|- F Fn X
80		qtopid	\|- ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> F e. ( J Cn ( J qTop F ) ) )
81	18 79 80	sylancl	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> F e. ( J Cn ( J qTop F ) ) )
82	16	oveq2d	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( J Cn K ) = ( J Cn ( J qTop F ) ) )
83	81 82	eleqtrrd	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> F e. ( J Cn K ) )
84	5 83	eqeltrrid	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( x e. X \|-> [ x ] ( G ~QG Y ) ) e. ( J Cn K ) )
85		eceq1	\|- ( x = ( z ( -g ` G ) w ) -> [ x ] ( G ~QG Y ) = [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) )
86	18 18 76 18 84 85	cnmpt21	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( z e. X , w e. X \|-> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) ) e. ( ( J tX J ) Cn K ) )
87	6 86	eqeltrid	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> .- e. ( ( J tX J ) Cn K ) )
88	87	ad2antrr	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> .- e. ( ( J tX J ) Cn K ) )
89		simplr	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> u e. K )
90		cnima	\|- ( ( .- e. ( ( J tX J ) Cn K ) /\ u e. K ) -> ( `' .- " u ) e. ( J tX J ) )
91	88 89 90	syl2anc	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( `' .- " u ) e. ( J tX J ) )
92	18	ad2antrr	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> J e. ( TopOn ` X ) )
93		eltx	\|- ( ( J e. ( TopOn ` X ) /\ J e. ( TopOn ` X ) ) -> ( ( `' .- " u ) e. ( J tX J ) <-> A. t e. ( `' .- " u ) E. c e. J E. d e. J ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
94	92 92 93	syl2anc	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( `' .- " u ) e. ( J tX J ) <-> A. t e. ( `' .- " u ) E. c e. J E. d e. J ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
95	91 94	mpbid	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> A. t e. ( `' .- " u ) E. c e. J E. d e. J ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) )
96		ecexg	\|- ( ( G ~QG Y ) e. _V -> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) e. _V )
97	11 96	ax-mp	\|- [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) e. _V
98	6 97	fnmpoi	\|- .- Fn ( X X. X )
99		elpreima	\|- ( .- Fn ( X X. X ) -> ( <. a , b >. e. ( `' .- " u ) <-> ( <. a , b >. e. ( X X. X ) /\ ( .- ` <. a , b >. ) e. u ) ) )
100	98 99	ax-mp	\|- ( <. a , b >. e. ( `' .- " u ) <-> ( <. a , b >. e. ( X X. X ) /\ ( .- ` <. a , b >. ) e. u ) )
101		opelxp	\|- ( <. a , b >. e. ( X X. X ) <-> ( a e. X /\ b e. X ) )
102	101	anbi1i	\|- ( ( <. a , b >. e. ( X X. X ) /\ ( .- ` <. a , b >. ) e. u ) <-> ( ( a e. X /\ b e. X ) /\ ( .- ` <. a , b >. ) e. u ) )
103		df-ov	\|- ( a .- b ) = ( .- ` <. a , b >. )
104		oveq12	\|- ( ( z = a /\ w = b ) -> ( z ( -g ` G ) w ) = ( a ( -g ` G ) b ) )
105	104	eceq1d	\|- ( ( z = a /\ w = b ) -> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) = [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) )
106		ecexg	\|- ( ( G ~QG Y ) e. _V -> [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. _V )
107	11 106	ax-mp	\|- [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. _V
108	105 6 107	ovmpoa	\|- ( ( a e. X /\ b e. X ) -> ( a .- b ) = [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) )
109	103 108	eqtr3id	\|- ( ( a e. X /\ b e. X ) -> ( .- ` <. a , b >. ) = [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) )
110	109	eleq1d	\|- ( ( a e. X /\ b e. X ) -> ( ( .- ` <. a , b >. ) e. u <-> [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u ) )
111	110	pm5.32i	\|- ( ( ( a e. X /\ b e. X ) /\ ( .- ` <. a , b >. ) e. u ) <-> ( ( a e. X /\ b e. X ) /\ [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u ) )
112	100 102 111	3bitri	\|- ( <. a , b >. e. ( `' .- " u ) <-> ( ( a e. X /\ b e. X ) /\ [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u ) )
113		eleq1	\|- ( t = <. a , b >. -> ( t e. ( c X. d ) <-> <. a , b >. e. ( c X. d ) ) )
114		opelxp	\|- ( <. a , b >. e. ( c X. d ) <-> ( a e. c /\ b e. d ) )
115	113 114	bitrdi	\|- ( t = <. a , b >. -> ( t e. ( c X. d ) <-> ( a e. c /\ b e. d ) ) )
116	115	anbi1d	\|- ( t = <. a , b >. -> ( ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) <-> ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
117	116	2rexbidv	\|- ( t = <. a , b >. -> ( E. c e. J E. d e. J ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) <-> E. c e. J E. d e. J ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
118	117	rspccv	\|- ( A. t e. ( `' .- " u ) E. c e. J E. d e. J ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) -> ( <. a , b >. e. ( `' .- " u ) -> E. c e. J E. d e. J ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
119	112 118	biimtrrid	\|- ( A. t e. ( `' .- " u ) E. c e. J E. d e. J ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) -> ( ( ( a e. X /\ b e. X ) /\ [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u ) -> E. c e. J E. d e. J ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
120	95 119	syl	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( ( a e. X /\ b e. X ) /\ [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u ) -> E. c e. J E. d e. J ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
121	66 120	mpand	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u -> E. c e. J E. d e. J ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
122		simp-4l	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> G e. TopGrp )
123	58	adantr	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> Y e. ( NrmSGrp ` G ) )
124		simprll	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> c e. J )
125	1 2 3 4 5	qustgpopn	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ c e. J ) -> ( F " c ) e. K )
126	122 123 124 125	syl3anc	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( F " c ) e. K )
127		simprlr	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> d e. J )
128	1 2 3 4 5	qustgpopn	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ d e. J ) -> ( F " d ) e. K )
129	122 123 127 128	syl3anc	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( F " d ) e. K )
130	59	adantr	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> a e. X )
131		eceq1	\|- ( x = a -> [ x ] ( G ~QG Y ) = [ a ] ( G ~QG Y ) )
132	131 5 78	fvmpt3i	\|- ( a e. X -> ( F ` a ) = [ a ] ( G ~QG Y ) )
133	130 132	syl	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( F ` a ) = [ a ] ( G ~QG Y ) )
134	122 17	syl	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> J e. ( TopOn ` X ) )
135		toponss	\|- ( ( J e. ( TopOn ` X ) /\ c e. J ) -> c C_ X )
136	134 124 135	syl2anc	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> c C_ X )
137		simprrl	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( a e. c /\ b e. d ) )
138	137	simpld	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> a e. c )
139		fnfvima	\|- ( ( F Fn X /\ c C_ X /\ a e. c ) -> ( F ` a ) e. ( F " c ) )
140	79 136 138 139	mp3an2i	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( F ` a ) e. ( F " c ) )
141	133 140	eqeltrrd	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> [ a ] ( G ~QG Y ) e. ( F " c ) )
142	60	adantr	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> b e. X )
143		eceq1	\|- ( x = b -> [ x ] ( G ~QG Y ) = [ b ] ( G ~QG Y ) )
144	143 5 78	fvmpt3i	\|- ( b e. X -> ( F ` b ) = [ b ] ( G ~QG Y ) )
145	142 144	syl	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( F ` b ) = [ b ] ( G ~QG Y ) )
146		toponss	\|- ( ( J e. ( TopOn ` X ) /\ d e. J ) -> d C_ X )
147	134 127 146	syl2anc	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> d C_ X )
148	137	simprd	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> b e. d )
149		fnfvima	\|- ( ( F Fn X /\ d C_ X /\ b e. d ) -> ( F ` b ) e. ( F " d ) )
150	79 147 148 149	mp3an2i	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( F ` b ) e. ( F " d ) )
151	145 150	eqeltrrd	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> [ b ] ( G ~QG Y ) e. ( F " d ) )
152	141 151	opelxpd	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. ( F " d ) ) )
153	136	sselda	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ p e. c ) -> p e. X )
154	147	sselda	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ q e. d ) -> q e. X )
155	153 154	anim12dan	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( p e. X /\ q e. X ) )
156		eceq1	\|- ( x = p -> [ x ] ( G ~QG Y ) = [ p ] ( G ~QG Y ) )
157	156 5 78	fvmpt3i	\|- ( p e. X -> ( F ` p ) = [ p ] ( G ~QG Y ) )
158		eceq1	\|- ( x = q -> [ x ] ( G ~QG Y ) = [ q ] ( G ~QG Y ) )
159	158 5 78	fvmpt3i	\|- ( q e. X -> ( F ` q ) = [ q ] ( G ~QG Y ) )
160		opeq12	\|- ( ( ( F ` p ) = [ p ] ( G ~QG Y ) /\ ( F ` q ) = [ q ] ( G ~QG Y ) ) -> <. ( F ` p ) , ( F ` q ) >. = <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. )
161	157 159 160	syl2an	\|- ( ( p e. X /\ q e. X ) -> <. ( F ` p ) , ( F ` q ) >. = <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. )
162	155 161	syl	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> <. ( F ` p ) , ( F ` q ) >. = <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. )
163	123	adantr	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> Y e. ( NrmSGrp ` G ) )
164	1 2 25	quseccl	\|- ( ( Y e. ( NrmSGrp ` G ) /\ p e. X ) -> [ p ] ( G ~QG Y ) e. ( Base ` H ) )
165	1 2 25	quseccl	\|- ( ( Y e. ( NrmSGrp ` G ) /\ q e. X ) -> [ q ] ( G ~QG Y ) e. ( Base ` H ) )
166	164 165	anim12dan	\|- ( ( Y e. ( NrmSGrp ` G ) /\ ( p e. X /\ q e. X ) ) -> ( [ p ] ( G ~QG Y ) e. ( Base ` H ) /\ [ q ] ( G ~QG Y ) e. ( Base ` H ) ) )
167	163 155 166	syl2anc	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( [ p ] ( G ~QG Y ) e. ( Base ` H ) /\ [ q ] ( G ~QG Y ) e. ( Base ` H ) ) )
168		opelxpi	\|- ( ( [ p ] ( G ~QG Y ) e. ( Base ` H ) /\ [ q ] ( G ~QG Y ) e. ( Base ` H ) ) -> <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) )
169	167 168	syl	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) )
170	1 2 61 28	qussub	\|- ( ( Y e. ( NrmSGrp ` G ) /\ p e. X /\ q e. X ) -> ( [ p ] ( G ~QG Y ) ( -g ` H ) [ q ] ( G ~QG Y ) ) = [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) )
171	170	3expb	\|- ( ( Y e. ( NrmSGrp ` G ) /\ ( p e. X /\ q e. X ) ) -> ( [ p ] ( G ~QG Y ) ( -g ` H ) [ q ] ( G ~QG Y ) ) = [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) )
172	163 155 171	syl2anc	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( [ p ] ( G ~QG Y ) ( -g ` H ) [ q ] ( G ~QG Y ) ) = [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) )
173		oveq12	\|- ( ( z = p /\ w = q ) -> ( z ( -g ` G ) w ) = ( p ( -g ` G ) q ) )
174	173	eceq1d	\|- ( ( z = p /\ w = q ) -> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) = [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) )
175		ecexg	\|- ( ( G ~QG Y ) e. _V -> [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) e. _V )
176	11 175	ax-mp	\|- [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) e. _V
177	174 6 176	ovmpoa	\|- ( ( p e. X /\ q e. X ) -> ( p .- q ) = [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) )
178	155 177	syl	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( p .- q ) = [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) )
179	172 178	eqtr4d	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( [ p ] ( G ~QG Y ) ( -g ` H ) [ q ] ( G ~QG Y ) ) = ( p .- q ) )
180		df-ov	\|- ( [ p ] ( G ~QG Y ) ( -g ` H ) [ q ] ( G ~QG Y ) ) = ( ( -g ` H ) ` <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. )
181		df-ov	\|- ( p .- q ) = ( .- ` <. p , q >. )
182	179 180 181	3eqtr3g	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( ( -g ` H ) ` <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. ) = ( .- ` <. p , q >. ) )
183		opelxpi	\|- ( ( p e. c /\ q e. d ) -> <. p , q >. e. ( c X. d ) )
184		simprrr	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( c X. d ) C_ ( `' .- " u ) )
185	184	sselda	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ <. p , q >. e. ( c X. d ) ) -> <. p , q >. e. ( `' .- " u ) )
186	183 185	sylan2	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> <. p , q >. e. ( `' .- " u ) )
187		elpreima	\|- ( .- Fn ( X X. X ) -> ( <. p , q >. e. ( `' .- " u ) <-> ( <. p , q >. e. ( X X. X ) /\ ( .- ` <. p , q >. ) e. u ) ) )
188	98 187	ax-mp	\|- ( <. p , q >. e. ( `' .- " u ) <-> ( <. p , q >. e. ( X X. X ) /\ ( .- ` <. p , q >. ) e. u ) )
189	188	simprbi	\|- ( <. p , q >. e. ( `' .- " u ) -> ( .- ` <. p , q >. ) e. u )
190	186 189	syl	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( .- ` <. p , q >. ) e. u )
191	182 190	eqeltrd	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( ( -g ` H ) ` <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. ) e. u )
192	53 54	syl	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( -g ` H ) Fn ( ( Base ` H ) X. ( Base ` H ) ) )
193	192	ad2antrr	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( -g ` H ) Fn ( ( Base ` H ) X. ( Base ` H ) ) )
194		elpreima	\|- ( ( -g ` H ) Fn ( ( Base ` H ) X. ( Base ` H ) ) -> ( <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) <-> ( <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) /\ ( ( -g ` H ) ` <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. ) e. u ) ) )
195	193 194	syl	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) <-> ( <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) /\ ( ( -g ` H ) ` <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. ) e. u ) ) )
196	169 191 195	mpbir2and	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) )
197	162 196	eqeltrd	\|- ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) )
198	197	ralrimivva	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> A. p e. c A. q e. d <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) )
199		opeq1	\|- ( z = ( F ` p ) -> <. z , w >. = <. ( F ` p ) , w >. )
200	199	eleq1d	\|- ( z = ( F ` p ) -> ( <. z , w >. e. ( `' ( -g ` H ) " u ) <-> <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) ) )
201	200	ralbidv	\|- ( z = ( F ` p ) -> ( A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) <-> A. w e. ( F " d ) <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) ) )
202	201	ralima	\|- ( ( F Fn X /\ c C_ X ) -> ( A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) <-> A. p e. c A. w e. ( F " d ) <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) ) )
203	79 202	mpan	\|- ( c C_ X -> ( A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) <-> A. p e. c A. w e. ( F " d ) <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) ) )
204		opeq2	\|- ( w = ( F ` q ) -> <. ( F ` p ) , w >. = <. ( F ` p ) , ( F ` q ) >. )
205	204	eleq1d	\|- ( w = ( F ` q ) -> ( <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) <-> <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) ) )
206	205	ralima	\|- ( ( F Fn X /\ d C_ X ) -> ( A. w e. ( F " d ) <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) <-> A. q e. d <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) ) )
207	79 206	mpan	\|- ( d C_ X -> ( A. w e. ( F " d ) <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) <-> A. q e. d <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) ) )
208	207	ralbidv	\|- ( d C_ X -> ( A. p e. c A. w e. ( F " d ) <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) <-> A. p e. c A. q e. d <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) ) )
209	203 208	sylan9bb	\|- ( ( c C_ X /\ d C_ X ) -> ( A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) <-> A. p e. c A. q e. d <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) ) )
210	136 147 209	syl2anc	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) <-> A. p e. c A. q e. d <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) ) )
211	198 210	mpbird	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) )
212		dfss3	\|- ( ( ( F " c ) X. ( F " d ) ) C_ ( `' ( -g ` H ) " u ) <-> A. y e. ( ( F " c ) X. ( F " d ) ) y e. ( `' ( -g ` H ) " u ) )
213		eleq1	\|- ( y = <. z , w >. -> ( y e. ( `' ( -g ` H ) " u ) <-> <. z , w >. e. ( `' ( -g ` H ) " u ) ) )
214	213	ralxp	\|- ( A. y e. ( ( F " c ) X. ( F " d ) ) y e. ( `' ( -g ` H ) " u ) <-> A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) )
215	212 214	bitri	\|- ( ( ( F " c ) X. ( F " d ) ) C_ ( `' ( -g ` H ) " u ) <-> A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) )
216	211 215	sylibr	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( ( F " c ) X. ( F " d ) ) C_ ( `' ( -g ` H ) " u ) )
217		xpeq1	\|- ( r = ( F " c ) -> ( r X. s ) = ( ( F " c ) X. s ) )
218	217	eleq2d	\|- ( r = ( F " c ) -> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) <-> <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. s ) ) )
219	217	sseq1d	\|- ( r = ( F " c ) -> ( ( r X. s ) C_ ( `' ( -g ` H ) " u ) <-> ( ( F " c ) X. s ) C_ ( `' ( -g ` H ) " u ) ) )
220	218 219	anbi12d	\|- ( r = ( F " c ) -> ( ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) <-> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. s ) /\ ( ( F " c ) X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
221		xpeq2	\|- ( s = ( F " d ) -> ( ( F " c ) X. s ) = ( ( F " c ) X. ( F " d ) ) )
222	221	eleq2d	\|- ( s = ( F " d ) -> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. s ) <-> <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. ( F " d ) ) ) )
223	221	sseq1d	\|- ( s = ( F " d ) -> ( ( ( F " c ) X. s ) C_ ( `' ( -g ` H ) " u ) <-> ( ( F " c ) X. ( F " d ) ) C_ ( `' ( -g ` H ) " u ) ) )
224	222 223	anbi12d	\|- ( s = ( F " d ) -> ( ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. s ) /\ ( ( F " c ) X. s ) C_ ( `' ( -g ` H ) " u ) ) <-> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. ( F " d ) ) /\ ( ( F " c ) X. ( F " d ) ) C_ ( `' ( -g ` H ) " u ) ) ) )
225	220 224	rspc2ev	\|- ( ( ( F " c ) e. K /\ ( F " d ) e. K /\ ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. ( F " d ) ) /\ ( ( F " c ) X. ( F " d ) ) C_ ( `' ( -g ` H ) " u ) ) ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) )
226	126 129 152 216 225	syl112anc	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) )
227	226	expr	\|- ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
228	227	rexlimdvva	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( E. c e. J E. d e. J ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
229	121 228	syld	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
230	65 229	sylbid	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. ) e. u -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
231	230	adantld	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) /\ ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. ) e. u ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
232	56 231	sylbid	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
233		opeq12	\|- ( ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> <. x , y >. = <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. )
234	233	eleq1d	\|- ( ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) <-> <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) ) )
235	233	eleq1d	\|- ( ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> ( <. x , y >. e. { w \| E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } <-> <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. { w \| E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) )
236		opex	\|- <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. _V
237		eleq1	\|- ( w = <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. -> ( w e. ( r X. s ) <-> <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) ) )
238	237	anbi1d	\|- ( w = <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. -> ( ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) <-> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
239	238	2rexbidv	\|- ( w = <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. -> ( E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) <-> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
240	236 239	elab	\|- ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. { w \| E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } <-> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) )
241	235 240	bitrdi	\|- ( ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> ( <. x , y >. e. { w \| E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } <-> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
242	234 241	imbi12d	\|- ( ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> ( ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> <. x , y >. e. { w \| E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) <-> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) ) )
243	232 242	syl5ibrcom	\|- ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> <. x , y >. e. { w \| E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) ) )
244	243	rexlimdvva	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( E. a e. X E. b e. X ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> <. x , y >. e. { w \| E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) ) )
245	51 244	sylbird	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( <. x , y >. e. ( ( Base ` H ) X. ( Base ` H ) ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> <. x , y >. e. { w \| E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) ) )
246	245	com23	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> ( <. x , y >. e. ( ( Base ` H ) X. ( Base ` H ) ) -> <. x , y >. e. { w \| E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) ) )
247	38 246	mpdd	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> <. x , y >. e. { w \| E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) )
248	37 247	relssdv	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( `' ( -g ` H ) " u ) C_ { w \| E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } )
249		ssabral	\|- ( ( `' ( -g ` H ) " u ) C_ { w \| E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } <-> A. w e. ( `' ( -g ` H ) " u ) E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) )
250	248 249	sylib	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> A. w e. ( `' ( -g ` H ) " u ) E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) )
251		eltx	\|- ( ( K e. ( TopOn ` ( Base ` H ) ) /\ K e. ( TopOn ` ( Base ` H ) ) ) -> ( ( `' ( -g ` H ) " u ) e. ( K tX K ) <-> A. w e. ( `' ( -g ` H ) " u ) E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
252	24 24 251	syl2anc	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( ( `' ( -g ` H ) " u ) e. ( K tX K ) <-> A. w e. ( `' ( -g ` H ) " u ) E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
253	252	adantr	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( ( `' ( -g ` H ) " u ) e. ( K tX K ) <-> A. w e. ( `' ( -g ` H ) " u ) E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
254	250 253	mpbird	\|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( `' ( -g ` H ) " u ) e. ( K tX K ) )
255	254	ralrimiva	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> A. u e. K ( `' ( -g ` H ) " u ) e. ( K tX K ) )
256		txtopon	\|- ( ( K e. ( TopOn ` ( Base ` H ) ) /\ K e. ( TopOn ` ( Base ` H ) ) ) -> ( K tX K ) e. ( TopOn ` ( ( Base ` H ) X. ( Base ` H ) ) ) )
257	24 24 256	syl2anc	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( K tX K ) e. ( TopOn ` ( ( Base ` H ) X. ( Base ` H ) ) ) )
258		iscn	\|- ( ( ( K tX K ) e. ( TopOn ` ( ( Base ` H ) X. ( Base ` H ) ) ) /\ K e. ( TopOn ` ( Base ` H ) ) ) -> ( ( -g ` H ) e. ( ( K tX K ) Cn K ) <-> ( ( -g ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) /\ A. u e. K ( `' ( -g ` H ) " u ) e. ( K tX K ) ) ) )
259	257 24 258	syl2anc	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( ( -g ` H ) e. ( ( K tX K ) Cn K ) <-> ( ( -g ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) /\ A. u e. K ( `' ( -g ` H ) " u ) e. ( K tX K ) ) ) )
260	30 255 259	mpbir2and	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( -g ` H ) e. ( ( K tX K ) Cn K ) )
261	4 28	istgp2	\|- ( H e. TopGrp <-> ( H e. Grp /\ H e. TopSp /\ ( -g ` H ) e. ( ( K tX K ) Cn K ) ) )
262	8 27 260 261	syl3anbrc	\|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H e. TopGrp )

Metamath Proof Explorer

Theorem qustgplem

Proof