ablpnpcan

Description: Cancellation law for mixed addition and subtraction. ( pnpcan analog.) (Contributed by NM, 29-May-2015)

	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$
	ablpnpcan.g	$⊢ φ \to G \in Abel$
	ablpnpcan.x	$⊢ φ \to X \in B$
	ablpnpcan.y	$⊢ φ \to Y \in B$
	ablpnpcan.z	$⊢ φ \to Z \in B$
Assertion	ablpnpcan	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{-} (X \underset{˙}{+} Z) = Y \underset{˙}{-} Z$

Proof

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		ablpnpcan.g	$⊢ φ \to G \in Abel$
9		ablpnpcan.x	$⊢ φ \to X \in B$
10		ablpnpcan.y	$⊢ φ \to Y \in B$
11		ablpnpcan.z	$⊢ φ \to Z \in B$
12	1 2 3	ablsub4	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (X \in B \land Z \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{-} (X \underset{˙}{+} Z) = (X \underset{˙}{-} X) \underset{˙}{+} (Y \underset{˙}{-} Z)$
13	4 5 6 5 7 12	syl122anc	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{-} (X \underset{˙}{+} Z) = (X \underset{˙}{-} X) \underset{˙}{+} (Y \underset{˙}{-} Z)$
14		ablgrp	$⊢ G \in Abel \to G \in Grp$
15	4 14	syl	$⊢ φ \to G \in Grp$
16		eqid	$⊢ 0_{G} = 0_{G}$
17	1 16 3	grpsubid	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{-} X = 0_{G}$
18	15 5 17	syl2anc	$⊢ φ \to X \underset{˙}{-} X = 0_{G}$
19	18	oveq1d	$⊢ φ \to (X \underset{˙}{-} X) \underset{˙}{+} (Y \underset{˙}{-} Z) = 0_{G} \underset{˙}{+} (Y \underset{˙}{-} Z)$
20	1 3	grpsubcl	$⊢ (G \in Grp \land Y \in B \land Z \in B) \to Y \underset{˙}{-} Z \in B$
21	15 6 7 20	syl3anc	$⊢ φ \to Y \underset{˙}{-} Z \in B$
22	1 2 16	grplid	$⊢ (G \in Grp \land Y \underset{˙}{-} Z \in B) \to 0_{G} \underset{˙}{+} (Y \underset{˙}{-} Z) = Y \underset{˙}{-} Z$
23	15 21 22	syl2anc	$⊢ φ \to 0_{G} \underset{˙}{+} (Y \underset{˙}{-} Z) = Y \underset{˙}{-} Z$
24	13 19 23	3eqtrd	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{-} (X \underset{˙}{+} Z) = Y \underset{˙}{-} Z$

Metamath Proof Explorer

Theorem ablpnpcan

Proof