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

Proof

Step Hyp Ref Expression
1 ngpsubcan.x 
 |-  X = ( Base ` G )
2 ngpsubcan.m 
 |-  .- = ( -g ` G )
3 ngpsubcan.d 
 |-  D = ( dist ` G )
4 simpr1 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> A e. X )
5 simpr3 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> C e. X )
6 eqid 
 |-  ( +g ` G ) = ( +g ` G )
7 eqid 
 |-  ( invg ` G ) = ( invg ` G )
8 1 6 7 2 grpsubval 
 |-  ( ( A e. X /\ C e. X ) -> ( A .- C ) = ( A ( +g ` G ) ( ( invg ` G ) ` C ) ) )
9 4 5 8 syl2anc 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A .- C ) = ( A ( +g ` G ) ( ( invg ` G ) ` C ) ) )
10 simpr2 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> B e. X )
11 1 6 7 2 grpsubval 
 |-  ( ( B e. X /\ C e. X ) -> ( B .- C ) = ( B ( +g ` G ) ( ( invg ` G ) ` C ) ) )
12 10 5 11 syl2anc 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B .- C ) = ( B ( +g ` G ) ( ( invg ` G ) ` C ) ) )
13 9 12 oveq12d 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A .- C ) D ( B .- C ) ) = ( ( A ( +g ` G ) ( ( invg ` G ) ` C ) ) D ( B ( +g ` G ) ( ( invg ` G ) ` C ) ) ) )
14 simpl 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> G e. NrmGrp )
15 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
16 1 7 grpinvcl 
 |-  ( ( G e. Grp /\ C e. X ) -> ( ( invg ` G ) ` C ) e. X )
17 15 5 16 syl2an2r 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( invg ` G ) ` C ) e. X )
18 1 6 3 ngprcan 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ ( ( invg ` G ) ` C ) e. X ) ) -> ( ( A ( +g ` G ) ( ( invg ` G ) ` C ) ) D ( B ( +g ` G ) ( ( invg ` G ) ` C ) ) ) = ( A D B ) )
19 14 4 10 17 18 syl13anc 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A ( +g ` G ) ( ( invg ` G ) ` C ) ) D ( B ( +g ` G ) ( ( invg ` G ) ` C ) ) ) = ( A D B ) )
20 13 19 eqtrd 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A .- C ) D ( B .- C ) ) = ( A D B ) )