Theorem quseccl

Description: Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypotheses	qusgrp.h	|- H = ( G /s ( G ~QG S ) )
	qusadd.v	|- V = ( Base ` G )
	quseccl.b	|- B = ( Base ` H )
Assertion	quseccl	|- ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> [ X ] ( G ~QG S ) e. B )

Proof

Step	Hyp	Ref	Expression
1		qusgrp.h	|- H = ( G /s ( G ~QG S ) )
2		qusadd.v	|- V = ( Base ` G )
3		quseccl.b	|- B = ( Base ` H )
4		ovex	|- ( G ~QG S ) e. _V
5	4	ecelqsi	|- ( X e. V -> [ X ] ( G ~QG S ) e. ( V /. ( G ~QG S ) ) )
6	5	adantl	|- ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> [ X ] ( G ~QG S ) e. ( V /. ( G ~QG S ) ) )
7	1	a1i	|- ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> H = ( G /s ( G ~QG S ) ) )
8	2	a1i	|- ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> V = ( Base ` G ) )
9	4	a1i	|- ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> ( G ~QG S ) e. _V )
10		nsgsubg	|- ( S e. ( NrmSGrp ` G ) -> S e. ( SubGrp ` G ) )
11		subgrcl	|- ( S e. ( SubGrp ` G ) -> G e. Grp )
12	10 11	syl	|- ( S e. ( NrmSGrp ` G ) -> G e. Grp )
13	12	adantr	|- ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> G e. Grp )
14	7 8 9 13	qusbas	|- ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> ( V /. ( G ~QG S ) ) = ( Base ` H ) )
15	14 3	eqtr4di	|- ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> ( V /. ( G ~QG S ) ) = B )
16	6 15	eleqtrd	|- ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> [ X ] ( G ~QG S ) e. B )