qustgplem

	Ref	Expression
Hypotheses	qustgp.h	$⊢ H = G /_{𝑠} (G ~_{QG} Y)$
	qustgpopn.x	$⊢ X = {Base}_{G}$
	qustgpopn.j	$⊢ J = TopOpen (G)$
	qustgpopn.k	$⊢ K = TopOpen (H)$
	qustgpopn.f	$⊢ F = (x \in X ⟼ [x] (G ~_{QG} Y))$
	qustgplem.m	$⊢ \underset{˙}{-} = (z \in X, w \in X ⟼ [(z -_{G} w)] (G ~_{QG} Y))$
Assertion	qustgplem	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G)) \to H \in TopGrp$

Proof

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

Metamath Proof Explorer

Theorem qustgplem

Proof