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={\mathrm{Base}}_R$$
	abvmet.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
	abvmet.m	$$⊢\underset{\dot{}}{-}={-}_R$$
Assertion	abvmet	$$⊢F\in A\to F\circ \underset{\dot{}}{-}\in \mathrm{Met}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		abvmet.x	$$⊢X={\mathrm{Base}}_R$$
2		abvmet.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
3		abvmet.m	$$⊢\underset{\dot{}}{-}={-}_R$$
4		eqid	$$⊢0_R=0_R$$
5	2	abvrcl	$$⊢F\in A\to R\in \mathrm{Ring}$$
6		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
7	5 6	syl	$$⊢F\in A\to R\in \mathrm{Grp}$$
8	2 1	abvf	$$⊢F\in A\to F:X⟶ℝ$$
9	2 1 4	abveq0	$$⊢\left(F\in A\wedge x\in X\right)\to \left(F\left(x\right)=0\leftrightarrow x=0_R\right)$$
10	2 1 3	abvsubtri	$$⊢\left(F\in A\wedge x\in X\wedge y\in X\right)\to F\left(x\underset{\dot{}}{-}y\right)\le F\left(x\right)+F\left(y\right)$$
11	10	3expb	$$⊢\left(F\in A\wedge \left(x\in X\wedge y\in X\right)\right)\to F\left(x\underset{\dot{}}{-}y\right)\le F\left(x\right)+F\left(y\right)$$
12	1 3 4 7 8 9 11	nrmmetd	$$⊢F\in A\to F\circ \underset{\dot{}}{-}\in \mathrm{Met}\left(X\right)$$