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