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 ⊢ H = G / 𝑠 G ~ QG Y
Assertion qustgp ⊢ G ∈ TopGrp ∧ Y ∈ NrmSGrp ⁡ G → H ∈ TopGrp

Proof

Step Hyp Ref Expression
1 qustgp.h ⊢ H = G / 𝑠 G ~ QG Y
2 eqid ⊢ Base G = Base G
3 eqid ⊢ TopOpen ⁡ G = TopOpen ⁡ G
4 eqid ⊢ TopOpen ⁡ H = TopOpen ⁡ H
5 eqid ⊢ x ∈ Base G ⟼ x G ~ QG Y = x ∈ Base G ⟼ x G ~ QG Y
6 eqid ⊢ z ∈ Base G , w ∈ Base G ⟼ z - G w G ~ QG Y = z ∈ Base G , w ∈ Base G ⟼ z - G w G ~ QG Y
7 1 2 3 4 5 6 qustgplem ⊢ G ∈ TopGrp ∧ Y ∈ NrmSGrp ⁡ G → H ∈ TopGrp