This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )