Metamath Proof Explorer

Theorem ngpinvds

Description: Two elements are the same distance apart as their inverses. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses ngpinvds.x 
|- X = ( Base ` G )
ngpinvds.i 
|- I = ( invg ` G )
ngpinvds.d 
|- D = ( dist ` G )
Assertion ngpinvds 
|- ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> ( ( I ` A ) D ( I ` B ) ) = ( A D B ) )

Proof

Step Hyp Ref Expression
1 ngpinvds.x 
 |-  X = ( Base ` G )
2 ngpinvds.i 
 |-  I = ( invg ` G )
3 ngpinvds.d 
 |-  D = ( dist ` G )
4 eqid 
 |-  ( -g ` G ) = ( -g ` G )
5 simplr 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> G e. Abel )
6 simprr 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> B e. X )
7 simprl 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> A e. X )
8 1 4 2 5 6 7 ablsub2inv 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> ( ( I ` B ) ( -g ` G ) ( I ` A ) ) = ( A ( -g ` G ) B ) )
9 8 fveq2d 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> ( ( norm ` G ) ` ( ( I ` B ) ( -g ` G ) ( I ` A ) ) ) = ( ( norm ` G ) ` ( A ( -g ` G ) B ) ) )
10 simpll 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> G e. NrmGrp )
11 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
12 10 11 syl 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> G e. Grp )
13 1 2 grpinvcl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( I ` A ) e. X )
14 12 7 13 syl2anc 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> ( I ` A ) e. X )
15 1 2 grpinvcl 
 |-  ( ( G e. Grp /\ B e. X ) -> ( I ` B ) e. X )
16 12 6 15 syl2anc 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> ( I ` B ) e. X )
17 eqid 
 |-  ( norm ` G ) = ( norm ` G )
18 17 1 4 3 ngpdsr 
 |-  ( ( G e. NrmGrp /\ ( I ` A ) e. X /\ ( I ` B ) e. X ) -> ( ( I ` A ) D ( I ` B ) ) = ( ( norm ` G ) ` ( ( I ` B ) ( -g ` G ) ( I ` A ) ) ) )
19 10 14 16 18 syl3anc 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> ( ( I ` A ) D ( I ` B ) ) = ( ( norm ` G ) ` ( ( I ` B ) ( -g ` G ) ( I ` A ) ) ) )
20 17 1 4 3 ngpds 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( ( norm ` G ) ` ( A ( -g ` G ) B ) ) )
21 10 7 6 20 syl3anc 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> ( A D B ) = ( ( norm ` G ) ` ( A ( -g ` G ) B ) ) )
22 9 19 21 3eqtr4d 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> ( ( I ` A ) D ( I ` B ) ) = ( A D B ) )