ngpsubcan

Description: Cancel right subtraction inside a distance calculation. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	ngpsubcan.x	$⊢ X = {Base}_{G}$
	ngpsubcan.m	$⊢ \underset{˙}{-} = -_{G}$
	ngpsubcan.d	$⊢ D = dist (G)$
Assertion	ngpsubcan	$⊢ (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		ngpsubcan.x	$⊢ X = {Base}_{G}$
2		ngpsubcan.m	$⊢ \underset{˙}{-} = -_{G}$
3		ngpsubcan.d	$⊢ D = dist (G)$
4		simpr1	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to A \in X$
5		simpr3	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to C \in X$
6		eqid	$⊢ +_{G} = +_{G}$
7		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
8	1 6 7 2	grpsubval	$⊢ (A \in X \land C \in X) \to A \underset{˙}{-} C = A +_{G} {inv}_{g} (G) (C)$
9	4 5 8	syl2anc	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to A \underset{˙}{-} C = A +_{G} {inv}_{g} (G) (C)$
10		simpr2	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to B \in X$
11	1 6 7 2	grpsubval	$⊢ (B \in X \land C \in X) \to B \underset{˙}{-} C = B +_{G} {inv}_{g} (G) (C)$
12	10 5 11	syl2anc	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to B \underset{˙}{-} C = B +_{G} {inv}_{g} (G) (C)$
13	9 12	oveq12d	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to (A \underset{˙}{-} C) D (B \underset{˙}{-} C) = (A +_{G} {inv}_{g} (G) (C)) D (B +_{G} {inv}_{g} (G) (C))$
14		simpl	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to G \in NrmGrp$
15		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
16	1 7	grpinvcl	$⊢ (G \in Grp \land C \in X) \to {inv}_{g} (G) (C) \in X$
17	15 5 16	syl2an2r	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to {inv}_{g} (G) (C) \in X$
18	1 6 3	ngprcan	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land {inv}_{g} (G) (C) \in X)) \to (A +_{G} {inv}_{g} (G) (C)) D (B +_{G} {inv}_{g} (G) (C)) = A D B$
19	14 4 10 17 18	syl13anc	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to (A +_{G} {inv}_{g} (G) (C)) D (B +_{G} {inv}_{g} (G) (C)) = A D B$
20	13 19	eqtrd	$⊢ (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 ngpsubcan

Proof