Metamath Proof Explorer

Theorem ngprcan

Description: Cancel right 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 ngprcan 
|- ( ( 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 ngprcan.x 
 |-  X = ( Base ` G )
2 ngprcan.p 
 |-  .+ = ( +g ` G )
3 ngprcan.d 
 |-  D = ( dist ` G )
4 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
5 eqid 
 |-  ( -g ` G ) = ( -g ` G )
6 1 2 5 grppnpcan2 
 |-  ( ( G e. Grp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A .+ C ) ( -g ` G ) ( B .+ C ) ) = ( A ( -g ` G ) B ) )
7 4 6 sylan 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A .+ C ) ( -g ` G ) ( B .+ C ) ) = ( A ( -g ` G ) B ) )
8 7 fveq2d 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( norm ` G ) ` ( ( A .+ C ) ( -g ` G ) ( B .+ C ) ) ) = ( ( norm ` G ) ` ( A ( -g ` G ) B ) ) )
9 simpl 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> G e. NrmGrp )
10 4 adantr 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> G e. Grp )
11 simpr1 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> A e. X )
12 simpr3 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> C e. X )
13 1 2 grpcl 
 |-  ( ( G e. Grp /\ A e. X /\ C e. X ) -> ( A .+ C ) e. X )
14 10 11 12 13 syl3anc 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A .+ C ) e. X )
15 simpr2 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> B e. X )
16 1 2 grpcl 
 |-  ( ( G e. Grp /\ B e. X /\ C e. X ) -> ( B .+ C ) e. X )
17 10 15 12 16 syl3anc 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B .+ C ) e. X )
18 eqid 
 |-  ( norm ` G ) = ( norm ` G )
19 18 1 5 3 ngpds 
 |-  ( ( G e. NrmGrp /\ ( A .+ C ) e. X /\ ( B .+ C ) e. X ) -> ( ( A .+ C ) D ( B .+ C ) ) = ( ( norm ` G ) ` ( ( A .+ C ) ( -g ` G ) ( B .+ C ) ) ) )
20 9 14 17 19 syl3anc 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A .+ C ) D ( B .+ C ) ) = ( ( norm ` G ) ` ( ( A .+ C ) ( -g ` G ) ( B .+ C ) ) ) )
21 18 1 5 3 ngpds 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( ( norm ` G ) ` ( A ( -g ` G ) B ) ) )
22 9 11 15 21 syl3anc 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) = ( ( norm ` G ) ` ( A ( -g ` G ) B ) ) )
23 8 20 22 3eqtr4d 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A .+ C ) D ( B .+ C ) ) = ( A D B ) )