eqgcpbl

Description: The subgroup coset equivalence relation is compatible with addition when the subgroup is normal. (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	eqger.x	$⊢ X = {Base}_{G}$
	eqger.r	$⊢ \underset{˙}{\sim} = G ~_{QG} Y$
	eqgcpbl.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	eqgcpbl	$⊢ Y \in NrmSGrp (G) \to ((A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D) \to (A \underset{˙}{+} B) \underset{˙}{\sim} (C \underset{˙}{+} D))$

Proof

Step	Hyp	Ref	Expression
1		eqger.x	$⊢ X = {Base}_{G}$
2		eqger.r	$⊢ \underset{˙}{\sim} = G ~_{QG} Y$
3		eqgcpbl.p	$⊢ \underset{˙}{+} = +_{G}$
4		nsgsubg	$⊢ Y \in NrmSGrp (G) \to Y \in SubGrp (G)$
5	4	adantr	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to Y \in SubGrp (G)$
6		subgrcl	$⊢ Y \in SubGrp (G) \to G \in Grp$
7	5 6	syl	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to G \in Grp$
8		simprl	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to A \underset{˙}{\sim} C$
9	1	subgss	$⊢ Y \in SubGrp (G) \to Y \subseteq X$
10	5 9	syl	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to Y \subseteq X$
11		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
12	1 11 3 2	eqgval	$⊢ (G \in Grp \land Y \subseteq X) \to (A \underset{˙}{\sim} C \leftrightarrow (A \in X \land C \in X \land {inv}_{g} (G) (A) \underset{˙}{+} C \in Y))$
13	7 10 12	syl2anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to (A \underset{˙}{\sim} C \leftrightarrow (A \in X \land C \in X \land {inv}_{g} (G) (A) \underset{˙}{+} C \in Y))$
14	8 13	mpbid	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to (A \in X \land C \in X \land {inv}_{g} (G) (A) \underset{˙}{+} C \in Y)$
15	14	simp1d	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to A \in X$
16		simprr	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to B \underset{˙}{\sim} D$
17	1 11 3 2	eqgval	$⊢ (G \in Grp \land Y \subseteq X) \to (B \underset{˙}{\sim} D \leftrightarrow (B \in X \land D \in X \land {inv}_{g} (G) (B) \underset{˙}{+} D \in Y))$
18	7 10 17	syl2anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to (B \underset{˙}{\sim} D \leftrightarrow (B \in X \land D \in X \land {inv}_{g} (G) (B) \underset{˙}{+} D \in Y))$
19	16 18	mpbid	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to (B \in X \land D \in X \land {inv}_{g} (G) (B) \underset{˙}{+} D \in Y)$
20	19	simp1d	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to B \in X$
21	1 3	grpcl	$⊢ (G \in Grp \land A \in X \land B \in X) \to A \underset{˙}{+} B \in X$
22	7 15 20 21	syl3anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to A \underset{˙}{+} B \in X$
23	14	simp2d	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to C \in X$
24	19	simp2d	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to D \in X$
25	1 3	grpcl	$⊢ (G \in Grp \land C \in X \land D \in X) \to C \underset{˙}{+} D \in X$
26	7 23 24 25	syl3anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to C \underset{˙}{+} D \in X$
27	1 3 11	grpinvadd	$⊢ (G \in Grp \land A \in X \land B \in X) \to {inv}_{g} (G) (A \underset{˙}{+} B) = {inv}_{g} (G) (B) \underset{˙}{+} {inv}_{g} (G) (A)$
28	7 15 20 27	syl3anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to {inv}_{g} (G) (A \underset{˙}{+} B) = {inv}_{g} (G) (B) \underset{˙}{+} {inv}_{g} (G) (A)$
29	28	oveq1d	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to {inv}_{g} (G) (A \underset{˙}{+} B) \underset{˙}{+} (C \underset{˙}{+} D) = ({inv}_{g} (G) (B) \underset{˙}{+} {inv}_{g} (G) (A)) \underset{˙}{+} (C \underset{˙}{+} D)$
30	1 11	grpinvcl	$⊢ (G \in Grp \land B \in X) \to {inv}_{g} (G) (B) \in X$
31	7 20 30	syl2anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to {inv}_{g} (G) (B) \in X$
32	1 11	grpinvcl	$⊢ (G \in Grp \land A \in X) \to {inv}_{g} (G) (A) \in X$
33	7 15 32	syl2anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to {inv}_{g} (G) (A) \in X$
34	1 3	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (B) \in X \land {inv}_{g} (G) (A) \in X \land C \underset{˙}{+} D \in X)) \to ({inv}_{g} (G) (B) \underset{˙}{+} {inv}_{g} (G) (A)) \underset{˙}{+} (C \underset{˙}{+} D) = {inv}_{g} (G) (B) \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D))$
35	7 31 33 26 34	syl13anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to ({inv}_{g} (G) (B) \underset{˙}{+} {inv}_{g} (G) (A)) \underset{˙}{+} (C \underset{˙}{+} D) = {inv}_{g} (G) (B) \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D))$
36	29 35	eqtrd	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to {inv}_{g} (G) (A \underset{˙}{+} B) \underset{˙}{+} (C \underset{˙}{+} D) = {inv}_{g} (G) (B) \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D))$
37	1 3	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (A) \in X \land C \in X \land D \in X)) \to ({inv}_{g} (G) (A) \underset{˙}{+} C) \underset{˙}{+} D = {inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D)$
38	7 33 23 24 37	syl13anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to ({inv}_{g} (G) (A) \underset{˙}{+} C) \underset{˙}{+} D = {inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D)$
39	38	oveq1d	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to (({inv}_{g} (G) (A) \underset{˙}{+} C) \underset{˙}{+} D) \underset{˙}{+} {inv}_{g} (G) (B) = ({inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D)) \underset{˙}{+} {inv}_{g} (G) (B)$
40	1 3	grpcl	$⊢ (G \in Grp \land {inv}_{g} (G) (A) \in X \land C \in X) \to {inv}_{g} (G) (A) \underset{˙}{+} C \in X$
41	7 33 23 40	syl3anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to {inv}_{g} (G) (A) \underset{˙}{+} C \in X$
42	1 3	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (A) \underset{˙}{+} C \in X \land D \in X \land {inv}_{g} (G) (B) \in X)) \to (({inv}_{g} (G) (A) \underset{˙}{+} C) \underset{˙}{+} D) \underset{˙}{+} {inv}_{g} (G) (B) = ({inv}_{g} (G) (A) \underset{˙}{+} C) \underset{˙}{+} (D \underset{˙}{+} {inv}_{g} (G) (B))$
43	7 41 24 31 42	syl13anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to (({inv}_{g} (G) (A) \underset{˙}{+} C) \underset{˙}{+} D) \underset{˙}{+} {inv}_{g} (G) (B) = ({inv}_{g} (G) (A) \underset{˙}{+} C) \underset{˙}{+} (D \underset{˙}{+} {inv}_{g} (G) (B))$
44	39 43	eqtr3d	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to ({inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D)) \underset{˙}{+} {inv}_{g} (G) (B) = ({inv}_{g} (G) (A) \underset{˙}{+} C) \underset{˙}{+} (D \underset{˙}{+} {inv}_{g} (G) (B))$
45	14	simp3d	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to {inv}_{g} (G) (A) \underset{˙}{+} C \in Y$
46	19	simp3d	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to {inv}_{g} (G) (B) \underset{˙}{+} D \in Y$
47		simpl	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to Y \in NrmSGrp (G)$
48	1 3	nsgbi	$⊢ (Y \in NrmSGrp (G) \land {inv}_{g} (G) (B) \in X \land D \in X) \to ({inv}_{g} (G) (B) \underset{˙}{+} D \in Y \leftrightarrow D \underset{˙}{+} {inv}_{g} (G) (B) \in Y)$
49	47 31 24 48	syl3anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to ({inv}_{g} (G) (B) \underset{˙}{+} D \in Y \leftrightarrow D \underset{˙}{+} {inv}_{g} (G) (B) \in Y)$
50	46 49	mpbid	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to D \underset{˙}{+} {inv}_{g} (G) (B) \in Y$
51	3	subgcl	$⊢ (Y \in SubGrp (G) \land {inv}_{g} (G) (A) \underset{˙}{+} C \in Y \land D \underset{˙}{+} {inv}_{g} (G) (B) \in Y) \to ({inv}_{g} (G) (A) \underset{˙}{+} C) \underset{˙}{+} (D \underset{˙}{+} {inv}_{g} (G) (B)) \in Y$
52	5 45 50 51	syl3anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to ({inv}_{g} (G) (A) \underset{˙}{+} C) \underset{˙}{+} (D \underset{˙}{+} {inv}_{g} (G) (B)) \in Y$
53	44 52	eqeltrd	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to ({inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D)) \underset{˙}{+} {inv}_{g} (G) (B) \in Y$
54	1 3	grpcl	$⊢ (G \in Grp \land {inv}_{g} (G) (A) \in X \land C \underset{˙}{+} D \in X) \to {inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D) \in X$
55	7 33 26 54	syl3anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to {inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D) \in X$
56	1 3	nsgbi	$⊢ (Y \in NrmSGrp (G) \land {inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D) \in X \land {inv}_{g} (G) (B) \in X) \to (({inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D)) \underset{˙}{+} {inv}_{g} (G) (B) \in Y \leftrightarrow {inv}_{g} (G) (B) \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D)) \in Y)$
57	47 55 31 56	syl3anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to (({inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D)) \underset{˙}{+} {inv}_{g} (G) (B) \in Y \leftrightarrow {inv}_{g} (G) (B) \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D)) \in Y)$
58	53 57	mpbid	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to {inv}_{g} (G) (B) \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (C \underset{˙}{+} D)) \in Y$
59	36 58	eqeltrd	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to {inv}_{g} (G) (A \underset{˙}{+} B) \underset{˙}{+} (C \underset{˙}{+} D) \in Y$
60	1 11 3 2	eqgval	$⊢ (G \in Grp \land Y \subseteq X) \to ((A \underset{˙}{+} B) \underset{˙}{\sim} (C \underset{˙}{+} D) \leftrightarrow (A \underset{˙}{+} B \in X \land C \underset{˙}{+} D \in X \land {inv}_{g} (G) (A \underset{˙}{+} B) \underset{˙}{+} (C \underset{˙}{+} D) \in Y))$
61	7 10 60	syl2anc	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to ((A \underset{˙}{+} B) \underset{˙}{\sim} (C \underset{˙}{+} D) \leftrightarrow (A \underset{˙}{+} B \in X \land C \underset{˙}{+} D \in X \land {inv}_{g} (G) (A \underset{˙}{+} B) \underset{˙}{+} (C \underset{˙}{+} D) \in Y))$
62	22 26 59 61	mpbir3and	$⊢ (Y \in NrmSGrp (G) \land (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D)) \to (A \underset{˙}{+} B) \underset{˙}{\sim} (C \underset{˙}{+} D)$
63	62	ex	$⊢ Y \in NrmSGrp (G) \to ((A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D) \to (A \underset{˙}{+} B) \underset{˙}{\sim} (C \underset{˙}{+} D))$

Metamath Proof Explorer

Theorem eqgcpbl

Proof