This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- .- = ( -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 ) )