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 /s ( G ~QG Y ) )
Assertion qustgp 
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H e. TopGrp )

Proof

Step Hyp Ref Expression
1 qustgp.h 
 |-  H = ( G /s ( G ~QG Y ) )
2 eqid 
 |-  ( Base ` G ) = ( Base ` G )
3 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
4 eqid 
 |-  ( TopOpen ` H ) = ( TopOpen ` H )
5 eqid 
 |-  ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) = ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) )
6 eqid 
 |-  ( z e. ( Base ` G ) , w e. ( Base ` G ) |-> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) ) = ( z e. ( Base ` G ) , w e. ( Base ` G ) |-> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) )
7 1 2 3 4 5 6 qustgplem 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H e. TopGrp )