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	⊢ 𝑋 = ( Base ‘ 𝑅 )
	abvmet.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
	abvmet.m	⊢ − = ( -g ‘ 𝑅 )
Assertion	abvmet	⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ∘ − ) ∈ ( Met ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		abvmet.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
2		abvmet.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
3		abvmet.m	⊢ − = ( -g ‘ 𝑅 )
4		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
5	2	abvrcl	⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Ring )
6		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
7	5 6	syl	⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Grp )
8	2 1	abvf	⊢ ( 𝐹 ∈ 𝐴 → 𝐹 : 𝑋 ⟶ ℝ )
9	2 1 4	abveq0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑅 ) ) )
10	2 1 3	abvsubtri	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
11	10	3expb	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
12	1 3 4 7 8 9 11	nrmmetd	⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ∘ − ) ∈ ( Met ‘ 𝑋 ) )