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 + ˙ = + G
ngprcan.d D = dist G
Assertion ngplcan G NrmGrp G Abel A X B X C X C + ˙ A D C + ˙ B = A D B

Proof

Step Hyp Ref Expression
1 ngprcan.x X = Base G
2 ngprcan.p + ˙ = + G
3 ngprcan.d D = dist G
4 simplr G NrmGrp G Abel A X B X C X G Abel
5 simpr3 G NrmGrp G Abel A X B X C X C X
6 simpr1 G NrmGrp G Abel A X B X C X A X
7 1 2 ablcom G Abel C X A X C + ˙ A = A + ˙ C
8 4 5 6 7 syl3anc G NrmGrp G Abel A X B X C X C + ˙ A = A + ˙ C
9 simpr2 G NrmGrp G Abel A X B X C X B X
10 1 2 ablcom G Abel C X B X C + ˙ B = B + ˙ C
11 4 5 9 10 syl3anc G NrmGrp G Abel A X B X C X C + ˙ B = B + ˙ C
12 8 11 oveq12d G NrmGrp G Abel A X B X C X C + ˙ A D C + ˙ B = A + ˙ C D B + ˙ C
13 1 2 3 ngprcan G NrmGrp A X B X C X A + ˙ C D B + ˙ C = A D B
14 13 adantlr G NrmGrp G Abel A X B X C X A + ˙ C D B + ˙ C = A D B
15 12 14 eqtrd G NrmGrp G Abel A X B X C X C + ˙ A D C + ˙ B = A D B