ngprcan

Description: Cancel right 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	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$

Proof

Step	Hyp	Ref	Expression
1		ngprcan.x	$⊢ X = {Base}_{G}$
2		ngprcan.p	$⊢ \underset{˙}{+} = +_{G}$
3		ngprcan.d	$⊢ D = dist (G)$
4		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
5		eqid	$⊢ -_{G} = -_{G}$
6	1 2 5	grppnpcan2	$⊢ (G \in Grp \land (A \in X \land B \in X \land C \in X)) \to (A \underset{˙}{+} C) -_{G} (B \underset{˙}{+} C) = A -_{G} B$
7	4 6	sylan	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to (A \underset{˙}{+} C) -_{G} (B \underset{˙}{+} C) = A -_{G} B$
8	7	fveq2d	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to norm (G) ((A \underset{˙}{+} C) -_{G} (B \underset{˙}{+} C)) = norm (G) (A -_{G} B)$
9		simpl	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to G \in NrmGrp$
10	4	adantr	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to G \in Grp$
11		simpr1	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to A \in X$
12		simpr3	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to C \in X$
13	1 2	grpcl	$⊢ (G \in Grp \land A \in X \land C \in X) \to A \underset{˙}{+} C \in X$
14	10 11 12 13	syl3anc	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to A \underset{˙}{+} C \in X$
15		simpr2	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to B \in X$
16	1 2	grpcl	$⊢ (G \in Grp \land B \in X \land C \in X) \to B \underset{˙}{+} C \in X$
17	10 15 12 16	syl3anc	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to B \underset{˙}{+} C \in X$
18		eqid	$⊢ norm (G) = norm (G)$
19	18 1 5 3	ngpds	$⊢ (G \in NrmGrp \land A \underset{˙}{+} C \in X \land B \underset{˙}{+} C \in X) \to (A \underset{˙}{+} C) D (B \underset{˙}{+} C) = norm (G) ((A \underset{˙}{+} C) -_{G} (B \underset{˙}{+} C))$
20	9 14 17 19	syl3anc	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to (A \underset{˙}{+} C) D (B \underset{˙}{+} C) = norm (G) ((A \underset{˙}{+} C) -_{G} (B \underset{˙}{+} C))$
21	18 1 5 3	ngpds	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = norm (G) (A -_{G} B)$
22	9 11 15 21	syl3anc	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to A D B = norm (G) (A -_{G} B)$
23	8 20 22	3eqtr4d	$⊢ (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$

Metamath Proof Explorer

Theorem ngprcan

Proof