ablsubaddsub

Description: Double subtraction and addition in abelian groups. ( cnambpcma analog.) (Contributed by AV, 3-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ablsubadd.b	$⊢ B = {Base}_{G}$
2		ablsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4	1 2 3	ablsubadd23	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Y) \underset{˙}{+} Z = X \underset{˙}{+} (Z \underset{˙}{-} Y)$
5	4	oveq1d	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{-} Y) \underset{˙}{+} Z) \underset{˙}{-} X = (X \underset{˙}{+} (Z \underset{˙}{-} Y)) \underset{˙}{-} X$
6		simpl	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to G \in Abel$
7		simpr1	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
8		ablgrp	$⊢ G \in Abel \to G \in Grp$
9	8	adantr	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to G \in Grp$
10		simpr3	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
11		simpr2	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
12	1 3	grpsubcl	$⊢ (G \in Grp \land Z \in B \land Y \in B) \to Z \underset{˙}{-} Y \in B$
13	9 10 11 12	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to Z \underset{˙}{-} Y \in B$
14	1 2	ablcom	$⊢ (G \in Abel \land X \in B \land Z \underset{˙}{-} Y \in B) \to X \underset{˙}{+} (Z \underset{˙}{-} Y) = (Z \underset{˙}{-} Y) \underset{˙}{+} X$
15	6 7 13 14	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{+} (Z \underset{˙}{-} Y) = (Z \underset{˙}{-} Y) \underset{˙}{+} X$
16	15	oveq1d	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} (Z \underset{˙}{-} Y)) \underset{˙}{-} X = ((Z \underset{˙}{-} Y) \underset{˙}{+} X) \underset{˙}{-} X$
17	1 2 3	grpaddsubass	$⊢ (G \in Grp \land (Z \underset{˙}{-} Y \in B \land X \in B \land X \in B)) \to ((Z \underset{˙}{-} Y) \underset{˙}{+} X) \underset{˙}{-} X = (Z \underset{˙}{-} Y) \underset{˙}{+} (X \underset{˙}{-} X)$
18	9 13 7 7 17	syl13anc	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to ((Z \underset{˙}{-} Y) \underset{˙}{+} X) \underset{˙}{-} X = (Z \underset{˙}{-} Y) \underset{˙}{+} (X \underset{˙}{-} X)$
19		eqid	$⊢ 0_{G} = 0_{G}$
20	1 19 3	grpsubid	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{-} X = 0_{G}$
21	9 7 20	syl2anc	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{-} X = 0_{G}$
22	21	oveq2d	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to (Z \underset{˙}{-} Y) \underset{˙}{+} (X \underset{˙}{-} X) = (Z \underset{˙}{-} Y) \underset{˙}{+} 0_{G}$
23	1 2 19 9 13	grpridd	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to (Z \underset{˙}{-} Y) \underset{˙}{+} 0_{G} = Z \underset{˙}{-} Y$
24	18 22 23	3eqtrd	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to ((Z \underset{˙}{-} Y) \underset{˙}{+} X) \underset{˙}{-} X = Z \underset{˙}{-} Y$
25	5 16 24	3eqtrd	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{-} Y) \underset{˙}{+} Z) \underset{˙}{-} X = Z \underset{˙}{-} Y$

Metamath Proof Explorer

Theorem ablsubaddsub

Proof