qustgpopn

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

	Ref	Expression
Hypotheses	qustgp.h	$⊢ H = G /_{𝑠} (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))$
Assertion	qustgpopn	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land S \in J) \to F [S] \in K$

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

Metamath Proof Explorer

Theorem qustgpopn

Proof