qussub

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

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

Proof

Step	Hyp	Ref	Expression
1		qusgrp.h	$⊢ H = G /_{𝑠} (G ~_{QG} S)$
2		qusinv.v	$⊢ V = {Base}_{G}$
3		qussub.p	$⊢ \underset{˙}{-} = -_{G}$
4		qussub.a	$⊢ N = -_{H}$
5		eqid	$⊢ {Base}_{H} = {Base}_{H}$
6	1 2 5	quseccl	$⊢ (S \in NrmSGrp (G) \land X \in V) \to [X] (G ~_{QG} S) \in {Base}_{H}$
7	6	3adant3	$⊢ (S \in NrmSGrp (G) \land X \in V \land Y \in V) \to [X] (G ~_{QG} S) \in {Base}_{H}$
8	1 2 5	quseccl	$⊢ (S \in NrmSGrp (G) \land Y \in V) \to [Y] (G ~_{QG} S) \in {Base}_{H}$
9		eqid	$⊢ +_{H} = +_{H}$
10		eqid	$⊢ {inv}_{g} (H) = {inv}_{g} (H)$
11	5 9 10 4	grpsubval	$⊢ ([X] (G ~_{QG} S) \in {Base}_{H} \land [Y] (G ~_{QG} S) \in {Base}_{H}) \to [X] (G ~_{QG} S) N [Y] (G ~_{QG} S) = [X] (G ~_{QG} S) +_{H} {inv}_{g} (H) ([Y] (G ~_{QG} S))$
12	7 8 11	3imp3i2an	$⊢ (S \in NrmSGrp (G) \land X \in V \land Y \in V) \to [X] (G ~_{QG} S) N [Y] (G ~_{QG} S) = [X] (G ~_{QG} S) +_{H} {inv}_{g} (H) ([Y] (G ~_{QG} S))$
13		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
14	1 2 13 10	qusinv	$⊢ (S \in NrmSGrp (G) \land Y \in V) \to {inv}_{g} (H) ([Y] (G ~_{QG} S)) = [{inv}_{g} (G) (Y)] (G ~_{QG} S)$
15	14	3adant2	$⊢ (S \in NrmSGrp (G) \land X \in V \land Y \in V) \to {inv}_{g} (H) ([Y] (G ~_{QG} S)) = [{inv}_{g} (G) (Y)] (G ~_{QG} S)$
16	15	oveq2d	$⊢ (S \in NrmSGrp (G) \land X \in V \land Y \in V) \to [X] (G ~_{QG} S) +_{H} {inv}_{g} (H) ([Y] (G ~_{QG} S)) = [X] (G ~_{QG} S) +_{H} [{inv}_{g} (G) (Y)] (G ~_{QG} S)$
17		nsgsubg	$⊢ S \in NrmSGrp (G) \to S \in SubGrp (G)$
18		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
19	17 18	syl	$⊢ S \in NrmSGrp (G) \to G \in Grp$
20	2 13	grpinvcl	$⊢ (G \in Grp \land Y \in V) \to {inv}_{g} (G) (Y) \in V$
21	19 20	sylan	$⊢ (S \in NrmSGrp (G) \land Y \in V) \to {inv}_{g} (G) (Y) \in V$
22	21	3adant2	$⊢ (S \in NrmSGrp (G) \land X \in V \land Y \in V) \to {inv}_{g} (G) (Y) \in V$
23		eqid	$⊢ +_{G} = +_{G}$
24	1 2 23 9	qusadd	$⊢ (S \in NrmSGrp (G) \land X \in V \land {inv}_{g} (G) (Y) \in V) \to [X] (G ~_{QG} S) +_{H} [{inv}_{g} (G) (Y)] (G ~_{QG} S) = [(X +_{G} {inv}_{g} (G) (Y))] (G ~_{QG} S)$
25	22 24	syld3an3	$⊢ (S \in NrmSGrp (G) \land X \in V \land Y \in V) \to [X] (G ~_{QG} S) +_{H} [{inv}_{g} (G) (Y)] (G ~_{QG} S) = [(X +_{G} {inv}_{g} (G) (Y))] (G ~_{QG} S)$
26	2 23 13 3	grpsubval	$⊢ (X \in V \land Y \in V) \to X \underset{˙}{-} Y = X +_{G} {inv}_{g} (G) (Y)$
27	26	3adant1	$⊢ (S \in NrmSGrp (G) \land X \in V \land Y \in V) \to X \underset{˙}{-} Y = X +_{G} {inv}_{g} (G) (Y)$
28	27	eceq1d	$⊢ (S \in NrmSGrp (G) \land X \in V \land Y \in V) \to [(X \underset{˙}{-} Y)] (G ~_{QG} S) = [(X +_{G} {inv}_{g} (G) (Y))] (G ~_{QG} S)$
29	25 28	eqtr4d	$⊢ (S \in NrmSGrp (G) \land X \in V \land Y \in V) \to [X] (G ~_{QG} S) +_{H} [{inv}_{g} (G) (Y)] (G ~_{QG} S) = [(X \underset{˙}{-} Y)] (G ~_{QG} S)$
30	12 16 29	3eqtrd	$⊢ (S \in NrmSGrp (G) \land X \in V \land Y \in V) \to [X] (G ~_{QG} S) N [Y] (G ~_{QG} S) = [(X \underset{˙}{-} Y)] (G ~_{QG} S)$

Metamath Proof Explorer

Theorem qussub

Proof