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 ` G )
ngprcan.d 
|- D = ( dist ` G )
Assertion ngplcan 
|- ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( C .+ A ) D ( C .+ B ) ) = ( A D B ) )

Proof

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