Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ngpds Structured version   Visualization version   Unicode version

Theorem ngpds 21617
 Description: Value of the distance function in terms of the norm of a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypotheses
Ref Expression
ngpds.n
ngpds.x
ngpds.m
ngpds.d
Assertion
Ref Expression
ngpds NrmGrp

Proof of Theorem ngpds
StepHypRef Expression
1 ngpds.n . . . . . 6
2 ngpds.m . . . . . 6
3 ngpds.d . . . . . 6
4 ngpds.x . . . . . 6
5 eqid 2451 . . . . . 6
61, 2, 3, 4, 5isngp2 21611 . . . . 5 NrmGrp
76simp3bi 1025 . . . 4 NrmGrp
873ad2ant1 1029 . . 3 NrmGrp
98oveqd 6307 . 2 NrmGrp
10 ngpgrp 21613 . . . . . 6 NrmGrp
114, 2grpsubf 16733 . . . . . 6
1210, 11syl 17 . . . . 5 NrmGrp
13123ad2ant1 1029 . . . 4 NrmGrp
14 opelxpi 4866 . . . . 5
15143adant1 1026 . . . 4 NrmGrp
16 fvco3 5942 . . . 4
1713, 15, 16syl2anc 667 . . 3 NrmGrp
18 df-ov 6293 . . 3
19 df-ov 6293 . . . 4
2019fveq2i 5868 . . 3
2117, 18, 203eqtr4g 2510 . 2 NrmGrp
22 ovres 6436 . . 3