Metamath Proof Explorer

Theorem 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 ⊢ - ˙ = - G
ngpsubcan.d ⊢ D = dist ⁡ G
Assertion ngpsubcan ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A - ˙ C D B - ˙ C = A D B

Proof

Step Hyp Ref Expression
1 ngpsubcan.x ⊢ X = Base G
2 ngpsubcan.m ⊢ - ˙ = - G
3 ngpsubcan.d ⊢ D = dist ⁡ G
4 simpr1 ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A ∈ X
5 simpr3 ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C ∈ X
6 eqid ⊢ + G = + G
7 eqid ⊢ inv g ⁡ G = inv g ⁡ G
8 1 6 7 2 grpsubval ⊢ A ∈ X ∧ C ∈ X → A - ˙ C = A + G inv g ⁡ G ⁡ C
9 4 5 8 syl2anc ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A - ˙ C = A + G inv g ⁡ G ⁡ C
10 simpr2 ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B ∈ X
11 1 6 7 2 grpsubval ⊢ B ∈ X ∧ C ∈ X → B - ˙ C = B + G inv g ⁡ G ⁡ C
12 10 5 11 syl2anc ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B - ˙ C = B + G inv g ⁡ G ⁡ C
13 9 12 oveq12d ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A - ˙ C D B - ˙ C = A + G inv g ⁡ G ⁡ C D B + G inv g ⁡ G ⁡ C
14 simpl ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → G ∈ NrmGrp
15 ngpgrp ⊢ G ∈ NrmGrp → G ∈ Grp
16 1 7 grpinvcl ⊢ G ∈ Grp ∧ C ∈ X → inv g ⁡ G ⁡ C ∈ X
17 15 5 16 syl2an2r ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → inv g ⁡ G ⁡ C ∈ X
18 1 6 3 ngprcan ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X ∧ inv g ⁡ G ⁡ C ∈ X → A + G inv g ⁡ G ⁡ C D B + G inv g ⁡ G ⁡ C = A D B
19 14 4 10 17 18 syl13anc ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A + G inv g ⁡ G ⁡ C D B + G inv g ⁡ G ⁡ C = A D B
20 13 19 eqtrd ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A - ˙ C D B - ˙ C = A D B