This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grppnpcan2

Description: Cancellation law for mixed addition and subtraction. ( pnpcan2 analog.) (Contributed by NM, 15-Feb-2008) (Revised by Mario Carneiro, 2-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		grpsubadd.b	$⊢ B = {Base}_{G}$
2		grpsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4		simpl	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to G \in Grp$
5	1 2	grpcl	$⊢ (G \in Grp \land X \in B \land Z \in B) \to X \underset{˙}{+} Z \in B$
6	5	3adant3r2	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{+} Z \in B$
7		simpr3	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
8		simpr2	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
9	1 2 3	grpsubsub4	$⊢ (G \in Grp \land (X \underset{˙}{+} Z \in B \land Z \in B \land Y \in B)) \to ((X \underset{˙}{+} Z) \underset{˙}{-} Z) \underset{˙}{-} Y = (X \underset{˙}{+} Z) \underset{˙}{-} (Y \underset{˙}{+} Z)$
10	4 6 7 8 9	syl13anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{+} Z) \underset{˙}{-} Z) \underset{˙}{-} Y = (X \underset{˙}{+} Z) \underset{˙}{-} (Y \underset{˙}{+} Z)$
11	1 2 3	grppncan	$⊢ (G \in Grp \land X \in B \land Z \in B) \to (X \underset{˙}{+} Z) \underset{˙}{-} Z = X$
12	11	3adant3r2	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Z) \underset{˙}{-} Z = X$
13	12	oveq1d	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{+} Z) \underset{˙}{-} Z) \underset{˙}{-} Y = X \underset{˙}{-} Y$
14	10 13	eqtr3d	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Z) \underset{˙}{-} (Y \underset{˙}{+} Z) = X \underset{˙}{-} Y$