Metamath Proof Explorer

Theorem quseccl

Description: Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015) (Proof shortened by AV, 9-Mar-2025)

	Ref	Expression
Hypotheses	qusgrp.h	$⊢ H = G /_{𝑠} (G ~_{QG} S)$
	qusadd.v	$⊢ V = {Base}_{G}$
	quseccl.b	$⊢ B = {Base}_{H}$
Assertion	quseccl	$⊢ (S \in NrmSGrp (G) \land X \in V) \to [X] (G ~_{QG} S) \in B$

Step	Hyp	Ref	Expression
1		qusgrp.h	$⊢ H = G /_{𝑠} (G ~_{QG} S)$
2		qusadd.v	$⊢ V = {Base}_{G}$
3		quseccl.b	$⊢ B = {Base}_{H}$
4		nsgsubg	$⊢ S \in NrmSGrp (G) \to S \in SubGrp (G)$
5		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
6	4 5	syl	$⊢ S \in NrmSGrp (G) \to G \in Grp$
7		eqid	$⊢ G ~_{QG} S = G ~_{QG} S$
8	7 1 2 3	quseccl0	$⊢ (G \in Grp \land X \in V) \to [X] (G ~_{QG} S) \in B$
9	6 8	sylan	$⊢ (S \in NrmSGrp (G) \land X \in V) \to [X] (G ~_{QG} S) \in B$