Theorem quseccl

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

	Ref	Expression
Hypotheses	qusgrp.h	⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
	qusadd.v	⊢ 𝑉 = ( Base ‘ 𝐺 )
	quseccl.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
Assertion	quseccl	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		qusgrp.h	⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
2		qusadd.v	⊢ 𝑉 = ( Base ‘ 𝐺 )
3		quseccl.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
4		ovex	⊢ ( 𝐺 ~QG 𝑆 ) ∈ V
5	4	ecelqsi	⊢ ( 𝑋 ∈ 𝑉 → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ∈ ( 𝑉 / ( 𝐺 ~QG 𝑆 ) ) )
6	5	adantl	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ∈ ( 𝑉 / ( 𝐺 ~QG 𝑆 ) ) )
7	1	a1i	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) ) )
8	2	a1i	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → 𝑉 = ( Base ‘ 𝐺 ) )
9	4	a1i	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ~QG 𝑆 ) ∈ V )
10		nsgsubg	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
11		subgrcl	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
12	10 11	syl	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
13	12	adantr	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → 𝐺 ∈ Grp )
14	7 8 9 13	qusbas	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑉 / ( 𝐺 ~QG 𝑆 ) ) = ( Base ‘ 𝐻 ) )
15	14 3	eqtr4di	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑉 / ( 𝐺 ~QG 𝑆 ) ) = 𝐵 )
16	6 15	eleqtrd	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ∈ 𝐵 )