Metamath Proof Explorer


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 )