Metamath Proof Explorer


Theorem abvmet

Description: An absolute value F generates a metric defined by d ( x , y ) = F ( x - y ) , analogously to cnmet . (In fact, the ring structure is not needed at all; the group properties abveq0 and abvtri , abvneg are sufficient.) (Contributed by Mario Carneiro, 9-Sep-2014) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses abvmet.x X = Base R
abvmet.a A = AbsVal R
abvmet.m - ˙ = - R
Assertion abvmet F A F - ˙ Met X

Proof

Step Hyp Ref Expression
1 abvmet.x X = Base R
2 abvmet.a A = AbsVal R
3 abvmet.m - ˙ = - R
4 eqid 0 R = 0 R
5 2 abvrcl F A R Ring
6 ringgrp R Ring R Grp
7 5 6 syl F A R Grp
8 2 1 abvf F A F : X
9 2 1 4 abveq0 F A x X F x = 0 x = 0 R
10 2 1 3 abvsubtri F A x X y X F x - ˙ y F x + F y
11 10 3expb F A x X y X F x - ˙ y F x + F y
12 1 3 4 7 8 9 11 nrmmetd F A F - ˙ Met X