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	|- .- = ( -g ` R )
Assertion	abvmet	|- ( F e. A -> ( F o. .- ) e. ( Met ` X ) )

Proof

Step	Hyp	Ref	Expression
1		abvmet.x	|- X = ( Base ` R )
2		abvmet.a	|- A = ( AbsVal ` R )
3		abvmet.m	|- .- = ( -g ` R )
4		eqid	|- ( 0g ` R ) = ( 0g ` R )
5	2	abvrcl	|- ( F e. A -> R e. Ring )
6		ringgrp	|- ( R e. Ring -> R e. Grp )
7	5 6	syl	|- ( F e. A -> R e. Grp )
8	2 1	abvf	|- ( F e. A -> F : X --> RR )
9	2 1 4	abveq0	|- ( ( F e. A /\ x e. X ) -> ( ( F ` x ) = 0 <-> x = ( 0g ` R ) ) )
10	2 1 3	abvsubtri	|- ( ( F e. A /\ x e. X /\ y e. X ) -> ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
11	10	3expb	|- ( ( F e. A /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
12	1 3 4 7 8 9 11	nrmmetd	|- ( F e. A -> ( F o. .- ) e. ( Met ` X ) )