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	⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑌 ) )
Assertion	qustgp	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐻 ∈ TopGrp )

Proof

Step	Hyp	Ref	Expression
1		qustgp.h	⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑌 ) )
2		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3		eqid	⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
4		eqid	⊢ ( TopOpen ‘ 𝐻 ) = ( TopOpen ‘ 𝐻 )
5		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) )
6		eqid	⊢ ( 𝑧 ∈ ( Base ‘ 𝐺 ) , 𝑤 ∈ ( Base ‘ 𝐺 ) ↦ [ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ] ( 𝐺 ~QG 𝑌 ) ) = ( 𝑧 ∈ ( Base ‘ 𝐺 ) , 𝑤 ∈ ( Base ‘ 𝐺 ) ↦ [ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ] ( 𝐺 ~QG 𝑌 ) )
7	1 2 3 4 5 6	qustgplem	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐻 ∈ TopGrp )