qustgphaus

Description: The quotient of a topological group by a closed normal subgroup is a Hausdorff topological group. In particular, the quotient by the closure of the identity is a Hausdorff topological group, isomorphic to both the Kolmogorov quotient and the Hausdorff quotient operations on topological spaces (because T0 and Hausdorff coincide for topological groups). (Contributed by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	qustgp.h	$⊢ H = G /_{𝑠} (G ~_{QG} Y)$
	qustgphaus.j	$⊢ J = TopOpen (G)$
	qustgphaus.k	$⊢ K = TopOpen (H)$
Assertion	qustgphaus	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to K \in Haus$

Proof

Step	Hyp	Ref	Expression
1		qustgp.h	$⊢ H = G /_{𝑠} (G ~_{QG} Y)$
2		qustgphaus.j	$⊢ J = TopOpen (G)$
3		qustgphaus.k	$⊢ K = TopOpen (H)$
4		eqid	$⊢ 0_{G} = 0_{G}$
5	1 4	qus0	$⊢ Y \in NrmSGrp (G) \to [0_{G}] (G ~_{QG} Y) = 0_{H}$
6	5	3ad2ant2	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to [0_{G}] (G ~_{QG} Y) = 0_{H}$
7		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
8	7	3ad2ant1	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to G \in Grp$
9		eqid	$⊢ {Base}_{G} = {Base}_{G}$
10	9 4	grpidcl	$⊢ G \in Grp \to 0_{G} \in {Base}_{G}$
11	8 10	syl	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to 0_{G} \in {Base}_{G}$
12		ovex	$⊢ G ~_{QG} Y \in V$
13	12	ecelqsi	$⊢ 0_{G} \in {Base}_{G} \to [0_{G}] (G ~_{QG} Y) \in ({Base}_{G} / (G ~_{QG} Y))$
14	11 13	syl	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to [0_{G}] (G ~_{QG} Y) \in ({Base}_{G} / (G ~_{QG} Y))$
15	6 14	eqeltrrd	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to 0_{H} \in ({Base}_{G} / (G ~_{QG} Y))$
16	15	snssd	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to \{0_{H}\} \subseteq {Base}_{G} / (G ~_{QG} Y)$
17		eqid	$⊢ (x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y)) = (x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y))$
18	17	mptpreima	$⊢ {(x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y))}^{-1} [\{0_{H}\}] = \{x \in {Base}_{G} \| [x] (G ~_{QG} Y) \in \{0_{H}\}\}$
19		nsgsubg	$⊢ Y \in NrmSGrp (G) \to Y \in SubGrp (G)$
20	19	3ad2ant2	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to Y \in SubGrp (G)$
21		eqid	$⊢ G ~_{QG} Y = G ~_{QG} Y$
22	9 21 4	eqgid	$⊢ Y \in SubGrp (G) \to [0_{G}] (G ~_{QG} Y) = Y$
23	20 22	syl	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to [0_{G}] (G ~_{QG} Y) = Y$
24	9	subgss	$⊢ Y \in SubGrp (G) \to Y \subseteq {Base}_{G}$
25	20 24	syl	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to Y \subseteq {Base}_{G}$
26	23 25	eqsstrd	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to [0_{G}] (G ~_{QG} Y) \subseteq {Base}_{G}$
27		sseqin2	$⊢ [0_{G}] (G ~_{QG} Y) \subseteq {Base}_{G} \leftrightarrow {Base}_{G} \cap [0_{G}] (G ~_{QG} Y) = [0_{G}] (G ~_{QG} Y)$
28	26 27	sylib	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to {Base}_{G} \cap [0_{G}] (G ~_{QG} Y) = [0_{G}] (G ~_{QG} Y)$
29	9 21	eqger	$⊢ Y \in SubGrp (G) \to (G ~_{QG} Y) Er {Base}_{G}$
30	20 29	syl	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to (G ~_{QG} Y) Er {Base}_{G}$
31	30 11	erth	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to (0_{G} (G ~_{QG} Y) x \leftrightarrow [0_{G}] (G ~_{QG} Y) = [x] (G ~_{QG} Y))$
32	31	adantr	$⊢ ((G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \land x \in {Base}_{G}) \to (0_{G} (G ~_{QG} Y) x \leftrightarrow [0_{G}] (G ~_{QG} Y) = [x] (G ~_{QG} Y))$
33	6	adantr	$⊢ ((G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \land x \in {Base}_{G}) \to [0_{G}] (G ~_{QG} Y) = 0_{H}$
34	33	eqeq1d	$⊢ ((G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \land x \in {Base}_{G}) \to ([0_{G}] (G ~_{QG} Y) = [x] (G ~_{QG} Y) \leftrightarrow 0_{H} = [x] (G ~_{QG} Y))$
35	32 34	bitrd	$⊢ ((G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \land x \in {Base}_{G}) \to (0_{G} (G ~_{QG} Y) x \leftrightarrow 0_{H} = [x] (G ~_{QG} Y))$
36		vex	$⊢ x \in V$
37		fvex	$⊢ 0_{G} \in V$
38	36 37	elec	$⊢ x \in [0_{G}] (G ~_{QG} Y) \leftrightarrow 0_{G} (G ~_{QG} Y) x$
39		fvex	$⊢ 0_{H} \in V$
40	39	elsn2	$⊢ [x] (G ~_{QG} Y) \in \{0_{H}\} \leftrightarrow [x] (G ~_{QG} Y) = 0_{H}$
41		eqcom	$⊢ [x] (G ~_{QG} Y) = 0_{H} \leftrightarrow 0_{H} = [x] (G ~_{QG} Y)$
42	40 41	bitri	$⊢ [x] (G ~_{QG} Y) \in \{0_{H}\} \leftrightarrow 0_{H} = [x] (G ~_{QG} Y)$
43	35 38 42	3bitr4g	$⊢ ((G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \land x \in {Base}_{G}) \to (x \in [0_{G}] (G ~_{QG} Y) \leftrightarrow [x] (G ~_{QG} Y) \in \{0_{H}\})$
44	43	rabbi2dva	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to {Base}_{G} \cap [0_{G}] (G ~_{QG} Y) = \{x \in {Base}_{G} \| [x] (G ~_{QG} Y) \in \{0_{H}\}\}$
45	28 44 23	3eqtr3d	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to \{x \in {Base}_{G} \| [x] (G ~_{QG} Y) \in \{0_{H}\}\} = Y$
46	18 45	syl5eq	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to {(x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y))}^{-1} [\{0_{H}\}] = Y$
47		simp3	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to Y \in Clsd (J)$
48	46 47	eqeltrd	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to {(x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y))}^{-1} [\{0_{H}\}] \in Clsd (J)$
49	2 9	tgptopon	$⊢ G \in TopGrp \to J \in TopOn ({Base}_{G})$
50	49	3ad2ant1	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to J \in TopOn ({Base}_{G})$
51	1	a1i	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to H = G /_{𝑠} (G ~_{QG} Y)$
52		eqidd	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to {Base}_{G} = {Base}_{G}$
53	12	a1i	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to G ~_{QG} Y \in V$
54		simp1	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to G \in TopGrp$
55	51 52 17 53 54	quslem	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to (x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y)) : {Base}_{G} \underset{onto}{⟶} {Base}_{G} / (G ~_{QG} Y)$
56		qtopcld	$⊢ (J \in TopOn ({Base}_{G}) \land (x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y)) : {Base}_{G} \underset{onto}{⟶} {Base}_{G} / (G ~_{QG} Y)) \to (\{0_{H}\} \in Clsd (J qTop (x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y))) \leftrightarrow (\{0_{H}\} \subseteq {Base}_{G} / (G ~_{QG} Y) \land {(x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y))}^{-1} [\{0_{H}\}] \in Clsd (J)))$
57	50 55 56	syl2anc	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to (\{0_{H}\} \in Clsd (J qTop (x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y))) \leftrightarrow (\{0_{H}\} \subseteq {Base}_{G} / (G ~_{QG} Y) \land {(x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y))}^{-1} [\{0_{H}\}] \in Clsd (J)))$
58	16 48 57	mpbir2and	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to \{0_{H}\} \in Clsd (J qTop (x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y)))$
59	51 52 17 53 54	qusval	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to H = (x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y)) “_{𝑠} G$
60	59 52 55 54 2 3	imastopn	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to K = J qTop (x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y))$
61	60	fveq2d	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to Clsd (K) = Clsd (J qTop (x \in {Base}_{G} ⟼ [x] (G ~_{QG} Y)))$
62	58 61	eleqtrrd	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to \{0_{H}\} \in Clsd (K)$
63	1	qustgp	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G)) \to H \in TopGrp$
64	63	3adant3	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to H \in TopGrp$
65		eqid	$⊢ 0_{H} = 0_{H}$
66	65 3	tgphaus	$⊢ H \in TopGrp \to (K \in Haus \leftrightarrow \{0_{H}\} \in Clsd (K))$
67	64 66	syl	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to (K \in Haus \leftrightarrow \{0_{H}\} \in Clsd (K))$
68	62 67	mpbird	$⊢ (G \in TopGrp \land Y \in NrmSGrp (G) \land Y \in Clsd (J)) \to K \in Haus$

Metamath Proof Explorer

Theorem qustgphaus

Proof