abladdsub4

Description: Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014)

	Ref	Expression
Hypotheses	ablsubadd.b	$⊢ B = {Base}_{G}$
	ablsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
	ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
Assertion	abladdsub4	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{+} Y = Z \underset{˙}{+} W \leftrightarrow X \underset{˙}{-} Z = W \underset{˙}{-} Y)$

Proof

Step	Hyp	Ref	Expression
1		ablsubadd.b	$⊢ B = {Base}_{G}$
2		ablsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4		ablgrp	$⊢ G \in Abel \to G \in Grp$
5	4	3ad2ant1	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to G \in Grp$
6		simp2l	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to X \in B$
7		simp2r	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Y \in B$
8	1 2	grpcl	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
9	5 6 7 8	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to X \underset{˙}{+} Y \in B$
10		simp3l	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Z \in B$
11		simp3r	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to W \in B$
12	1 2	grpcl	$⊢ (G \in Grp \land Z \in B \land W \in B) \to Z \underset{˙}{+} W \in B$
13	5 10 11 12	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Z \underset{˙}{+} W \in B$
14	1 2	grpcl	$⊢ (G \in Grp \land Z \in B \land Y \in B) \to Z \underset{˙}{+} Y \in B$
15	5 10 7 14	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Z \underset{˙}{+} Y \in B$
16	1 3	grpsubrcan	$⊢ (G \in Grp \land (X \underset{˙}{+} Y \in B \land Z \underset{˙}{+} W \in B \land Z \underset{˙}{+} Y \in B)) \to ((X \underset{˙}{+} Y) \underset{˙}{-} (Z \underset{˙}{+} Y) = (Z \underset{˙}{+} W) \underset{˙}{-} (Z \underset{˙}{+} Y) \leftrightarrow X \underset{˙}{+} Y = Z \underset{˙}{+} W)$
17	5 9 13 15 16	syl13anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to ((X \underset{˙}{+} Y) \underset{˙}{-} (Z \underset{˙}{+} Y) = (Z \underset{˙}{+} W) \underset{˙}{-} (Z \underset{˙}{+} Y) \leftrightarrow X \underset{˙}{+} Y = Z \underset{˙}{+} W)$
18		simp1	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to G \in Abel$
19	1 2 3	ablsub4	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land Y \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{-} (Z \underset{˙}{+} Y) = (X \underset{˙}{-} Z) \underset{˙}{+} (Y \underset{˙}{-} Y)$
20	18 6 7 10 7 19	syl122anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{-} (Z \underset{˙}{+} Y) = (X \underset{˙}{-} Z) \underset{˙}{+} (Y \underset{˙}{-} Y)$
21		eqid	$⊢ 0_{G} = 0_{G}$
22	1 21 3	grpsubid	$⊢ (G \in Grp \land Y \in B) \to Y \underset{˙}{-} Y = 0_{G}$
23	5 7 22	syl2anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Y \underset{˙}{-} Y = 0_{G}$
24	23	oveq2d	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{-} Z) \underset{˙}{+} (Y \underset{˙}{-} Y) = (X \underset{˙}{-} Z) \underset{˙}{+} 0_{G}$
25	1 3	grpsubcl	$⊢ (G \in Grp \land X \in B \land Z \in B) \to X \underset{˙}{-} Z \in B$
26	5 6 10 25	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to X \underset{˙}{-} Z \in B$
27	1 2 21	grprid	$⊢ (G \in Grp \land X \underset{˙}{-} Z \in B) \to (X \underset{˙}{-} Z) \underset{˙}{+} 0_{G} = X \underset{˙}{-} Z$
28	5 26 27	syl2anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{-} Z) \underset{˙}{+} 0_{G} = X \underset{˙}{-} Z$
29	20 24 28	3eqtrd	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{-} (Z \underset{˙}{+} Y) = X \underset{˙}{-} Z$
30	1 2 3	ablsub4	$⊢ (G \in Abel \land (Z \in B \land W \in B) \land (Z \in B \land Y \in B)) \to (Z \underset{˙}{+} W) \underset{˙}{-} (Z \underset{˙}{+} Y) = (Z \underset{˙}{-} Z) \underset{˙}{+} (W \underset{˙}{-} Y)$
31	18 10 11 10 7 30	syl122anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (Z \underset{˙}{+} W) \underset{˙}{-} (Z \underset{˙}{+} Y) = (Z \underset{˙}{-} Z) \underset{˙}{+} (W \underset{˙}{-} Y)$
32	1 21 3	grpsubid	$⊢ (G \in Grp \land Z \in B) \to Z \underset{˙}{-} Z = 0_{G}$
33	5 10 32	syl2anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Z \underset{˙}{-} Z = 0_{G}$
34	33	oveq1d	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (Z \underset{˙}{-} Z) \underset{˙}{+} (W \underset{˙}{-} Y) = 0_{G} \underset{˙}{+} (W \underset{˙}{-} Y)$
35	1 3	grpsubcl	$⊢ (G \in Grp \land W \in B \land Y \in B) \to W \underset{˙}{-} Y \in B$
36	5 11 7 35	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to W \underset{˙}{-} Y \in B$
37	1 2 21	grplid	$⊢ (G \in Grp \land W \underset{˙}{-} Y \in B) \to 0_{G} \underset{˙}{+} (W \underset{˙}{-} Y) = W \underset{˙}{-} Y$
38	5 36 37	syl2anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to 0_{G} \underset{˙}{+} (W \underset{˙}{-} Y) = W \underset{˙}{-} Y$
39	31 34 38	3eqtrd	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (Z \underset{˙}{+} W) \underset{˙}{-} (Z \underset{˙}{+} Y) = W \underset{˙}{-} Y$
40	29 39	eqeq12d	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to ((X \underset{˙}{+} Y) \underset{˙}{-} (Z \underset{˙}{+} Y) = (Z \underset{˙}{+} W) \underset{˙}{-} (Z \underset{˙}{+} Y) \leftrightarrow X \underset{˙}{-} Z = W \underset{˙}{-} Y)$
41	17 40	bitr3d	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{+} Y = Z \underset{˙}{+} W \leftrightarrow X \underset{˙}{-} Z = W \underset{˙}{-} Y)$

Metamath Proof Explorer

Theorem abladdsub4

Proof