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 ) |