Theorem qustgp

Description: The quotient of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015)

	Ref	Expression
Hypothesis	qustgp.h	$$⊢H=G{/}_{𝑠}\left(G{~}_{\mathit{QG}}Y\right)$$
Assertion	qustgp	$$⊢\left(G\in \mathrm{TopGrp}\wedge Y\in \mathrm{NrmSGrp}\left(G\right)\right)\to H\in \mathrm{TopGrp}$$

Proof

Step	Hyp	Ref	Expression
1		qustgp.h	$$⊢H=G{/}_{𝑠}\left(G{~}_{\mathit{QG}}Y\right)$$
2		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
3		eqid	$$⊢\mathrm{TopOpen}\left(G\right)=\mathrm{TopOpen}\left(G\right)$$
4		eqid	$$⊢\mathrm{TopOpen}\left(H\right)=\mathrm{TopOpen}\left(H\right)$$
5		eqid	$$⊢\left(x\in {\mathrm{Base}}_G⟼\left[x\right]\left(G{~}_{\mathit{QG}}Y\right)\right)=\left(x\in {\mathrm{Base}}_G⟼\left[x\right]\left(G{~}_{\mathit{QG}}Y\right)\right)$$
6		eqid	$$⊢\left(z\in {\mathrm{Base}}_G,w\in {\mathrm{Base}}_G⟼\left[\left(z{-}_{G}w\right)\right]\left(G{~}_{\mathit{QG}}Y\right)\right)=\left(z\in {\mathrm{Base}}_G,w\in {\mathrm{Base}}_G⟼\left[\left(z{-}_{G}w\right)\right]\left(G{~}_{\mathit{QG}}Y\right)\right)$$
7	1 2 3 4 5 6	qustgplem	$$⊢\left(G\in \mathrm{TopGrp}\wedge Y\in \mathrm{NrmSGrp}\left(G\right)\right)\to H\in \mathrm{TopGrp}$$