ablsubsub

	Ref	Expression
Hypotheses	ablsubadd.b	$⊢ B = {Base}_{G}$
	ablsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
	ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
	ablsubsub.g	$⊢ φ \to G \in Abel$
	ablsubsub.x	$⊢ φ \to X \in B$
	ablsubsub.y	$⊢ φ \to Y \in B$
	ablsubsub.z	$⊢ φ \to Z \in B$
Assertion	ablsubsub	$⊢ φ \to X \underset{˙}{-} (Y \underset{˙}{-} Z) = (X \underset{˙}{-} Y) \underset{˙}{+} Z$

Step	Hyp	Ref	Expression
1		ablsubadd.b	$⊢ B = {Base}_{G}$
2		ablsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4		ablsubsub.g	$⊢ φ \to G \in Abel$
5		ablsubsub.x	$⊢ φ \to X \in B$
6		ablsubsub.y	$⊢ φ \to Y \in B$
7		ablsubsub.z	$⊢ φ \to Z \in B$
8		ablgrp	$⊢ G \in Abel \to G \in Grp$
9	4 8	syl	$⊢ φ \to G \in Grp$
10	1 2 3	grpsubsub	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{-} (Y \underset{˙}{-} Z) = X \underset{˙}{+} (Z \underset{˙}{-} Y)$
11	9 5 6 7 10	syl13anc	$⊢ φ \to X \underset{˙}{-} (Y \underset{˙}{-} Z) = X \underset{˙}{+} (Z \underset{˙}{-} Y)$
12	1 2 3	grpaddsubass	$⊢ (G \in Grp \land (X \in B \land Z \in B \land Y \in B)) \to (X \underset{˙}{+} Z) \underset{˙}{-} Y = X \underset{˙}{+} (Z \underset{˙}{-} Y)$
13	9 5 7 6 12	syl13anc	$⊢ φ \to (X \underset{˙}{+} Z) \underset{˙}{-} Y = X \underset{˙}{+} (Z \underset{˙}{-} Y)$
14	1 2 3	abladdsub	$⊢ (G \in Abel \land (X \in B \land Z \in B \land Y \in B)) \to (X \underset{˙}{+} Z) \underset{˙}{-} Y = (X \underset{˙}{-} Y) \underset{˙}{+} Z$
15	4 5 7 6 14	syl13anc	$⊢ φ \to (X \underset{˙}{+} Z) \underset{˙}{-} Y = (X \underset{˙}{-} Y) \underset{˙}{+} Z$
16	11 13 15	3eqtr2d	$⊢ φ \to X \underset{˙}{-} (Y \underset{˙}{-} Z) = (X \underset{˙}{-} Y) \underset{˙}{+} Z$

Metamath Proof Explorer