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 = inv g G
ngpinvds.d D = dist G
Assertion ngpinvds G NrmGrp G Abel A X B X I A D I B = A D B

Proof

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