Metamath Proof Explorer


Theorem ngpds3

Description: Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses ngpds2.x X = Base G
ngpds2.z 0 ˙ = 0 G
ngpds2.m - ˙ = - G
ngpds2.d D = dist G
Assertion ngpds3 G NrmGrp A X B X A D B = 0 ˙ D A - ˙ B

Proof

Step Hyp Ref Expression
1 ngpds2.x X = Base G
2 ngpds2.z 0 ˙ = 0 G
3 ngpds2.m - ˙ = - G
4 ngpds2.d D = dist G
5 1 2 3 4 ngpds2 G NrmGrp A X B X A D B = A - ˙ B D 0 ˙
6 ngpxms G NrmGrp G ∞MetSp
7 6 3ad2ant1 G NrmGrp A X B X G ∞MetSp
8 ngpgrp G NrmGrp G Grp
9 1 3 grpsubcl G Grp A X B X A - ˙ B X
10 8 9 syl3an1 G NrmGrp A X B X A - ˙ B X
11 8 3ad2ant1 G NrmGrp A X B X G Grp
12 1 2 grpidcl G Grp 0 ˙ X
13 11 12 syl G NrmGrp A X B X 0 ˙ X
14 1 4 xmssym G ∞MetSp A - ˙ B X 0 ˙ X A - ˙ B D 0 ˙ = 0 ˙ D A - ˙ B
15 7 10 13 14 syl3anc G NrmGrp A X B X A - ˙ B D 0 ˙ = 0 ˙ D A - ˙ B
16 5 15 eqtrd G NrmGrp A X B X A D B = 0 ˙ D A - ˙ B