Metamath Proof Explorer

Theorem ngplcan

Description: Cancel left addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015)

		Ref	Expression
	Hypotheses	ngprcan.x	$⊢ X = {Base}_{G}$
		ngprcan.p	$⊢ \underset{˙}{+} = +_{G}$
		ngprcan.d	$⊢ D = dist (G)$
	Assertion	ngplcan	$⊢ ((G \in NrmGrp \land G \in Abel) \land (A \in X \land B \in X \land C \in X)) \to (C \underset{˙}{+} A) D (C \underset{˙}{+} B) = A D B$

Proof

Step	Hyp	Ref	Expression
1		ngprcan.x	$⊢ X = {Base}_{G}$
2		ngprcan.p	$⊢ \underset{˙}{+} = +_{G}$
3		ngprcan.d	$⊢ D = dist (G)$
4		simplr	$⊢ ((G \in NrmGrp \land G \in Abel) \land (A \in X \land B \in X \land C \in X)) \to G \in Abel$
5		simpr3	$⊢ ((G \in NrmGrp \land G \in Abel) \land (A \in X \land B \in X \land C \in X)) \to C \in X$
6		simpr1	$⊢ ((G \in NrmGrp \land G \in Abel) \land (A \in X \land B \in X \land C \in X)) \to A \in X$
7	1 2	ablcom	$⊢ (G \in Abel \land C \in X \land A \in X) \to C \underset{˙}{+} A = A \underset{˙}{+} C$
8	4 5 6 7	syl3anc	$⊢ ((G \in NrmGrp \land G \in Abel) \land (A \in X \land B \in X \land C \in X)) \to C \underset{˙}{+} A = A \underset{˙}{+} C$
9		simpr2	$⊢ ((G \in NrmGrp \land G \in Abel) \land (A \in X \land B \in X \land C \in X)) \to B \in X$
10	1 2	ablcom	$⊢ (G \in Abel \land C \in X \land B \in X) \to C \underset{˙}{+} B = B \underset{˙}{+} C$
11	4 5 9 10	syl3anc	$⊢ ((G \in NrmGrp \land G \in Abel) \land (A \in X \land B \in X \land C \in X)) \to C \underset{˙}{+} B = B \underset{˙}{+} C$
12	8 11	oveq12d	$⊢ ((G \in NrmGrp \land G \in Abel) \land (A \in X \land B \in X \land C \in X)) \to (C \underset{˙}{+} A) D (C \underset{˙}{+} B) = (A \underset{˙}{+} C) D (B \underset{˙}{+} C)$
13	1 2 3	ngprcan	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to (A \underset{˙}{+} C) D (B \underset{˙}{+} C) = A D B$
14	13	adantlr	$⊢ ((G \in NrmGrp \land G \in Abel) \land (A \in X \land B \in X \land C \in X)) \to (A \underset{˙}{+} C) D (B \underset{˙}{+} C) = A D B$
15	12 14	eqtrd	$⊢ ((G \in NrmGrp \land G \in Abel) \land (A \in X \land B \in X \land C \in X)) \to (C \underset{˙}{+} A) D (C \underset{˙}{+} B) = A D B$