qusadd

Description: Value of the group operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypotheses	qusgrp.h	$⊢ H = G /_{𝑠} (G ~_{QG} S)$
	qusadd.v	$⊢ V = {Base}_{G}$
	qusadd.p	$⊢ \underset{˙}{+} = +_{G}$
	qusadd.a	$⊢ \underset{˙}{✚} = +_{H}$
Assertion	qusadd	$⊢ (S \in NrmSGrp (G) \land X \in V \land Y \in V) \to [X] (G ~_{QG} S) \underset{˙}{✚} [Y] (G ~_{QG} S) = [(X \underset{˙}{+} Y)] (G ~_{QG} S)$

Step	Hyp	Ref	Expression
1		qusgrp.h	$⊢ H = G /_{𝑠} (G ~_{QG} S)$
2		qusadd.v	$⊢ V = {Base}_{G}$
3		qusadd.p	$⊢ \underset{˙}{+} = +_{G}$
4		qusadd.a	$⊢ \underset{˙}{✚} = +_{H}$
5	1	a1i	$⊢ S \in NrmSGrp (G) \to H = G /_{𝑠} (G ~_{QG} S)$
6	2	a1i	$⊢ S \in NrmSGrp (G) \to V = {Base}_{G}$
7		nsgsubg	$⊢ S \in NrmSGrp (G) \to S \in SubGrp (G)$
8		eqid	$⊢ G ~_{QG} S = G ~_{QG} S$
9	2 8	eqger	$⊢ S \in SubGrp (G) \to (G ~_{QG} S) Er V$
10	7 9	syl	$⊢ S \in NrmSGrp (G) \to (G ~_{QG} S) Er V$
11		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
12	7 11	syl	$⊢ S \in NrmSGrp (G) \to G \in Grp$
13	2 8 3	eqgcpbl	$⊢ S \in NrmSGrp (G) \to ((a (G ~_{QG} S) p \land b (G ~_{QG} S) q) \to (a \underset{˙}{+} b) (G ~_{QG} S) (p \underset{˙}{+} q))$
14	2 3	grpcl	$⊢ (G \in Grp \land p \in V \land q \in V) \to p \underset{˙}{+} q \in V$
15	14	3expb	$⊢ (G \in Grp \land (p \in V \land q \in V)) \to p \underset{˙}{+} q \in V$
16	12 15	sylan	$⊢ (S \in NrmSGrp (G) \land (p \in V \land q \in V)) \to p \underset{˙}{+} q \in V$
17	5 6 10 12 13 16 3 4	qusaddval	$⊢ (S \in NrmSGrp (G) \land X \in V \land Y \in V) \to [X] (G ~_{QG} S) \underset{˙}{✚} [Y] (G ~_{QG} S) = [(X \underset{˙}{+} Y)] (G ~_{QG} S)$

Metamath Proof Explorer