# Metamath Proof Explorer

## Theorem abvtri

Description: An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abvf.a ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
abvf.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
abvtri.p
Assertion abvtri

### Proof

Step Hyp Ref Expression
1 abvf.a ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
2 abvf.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 abvtri.p
4 1 abvrcl ${⊢}{F}\in {A}\to {R}\in \mathrm{Ring}$
5 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
6 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
7 1 2 3 5 6 isabv
8 4 7 syl
9 8 ibi
10 simpr
11 10 ralimi
13 12 ralimi
14 9 13 simpl2im
15 fvoveq1
16 fveq2 ${⊢}{x}={X}\to {F}\left({x}\right)={F}\left({X}\right)$
17 16 oveq1d ${⊢}{x}={X}\to {F}\left({x}\right)+{F}\left({y}\right)={F}\left({X}\right)+{F}\left({y}\right)$
18 15 17 breq12d
19 oveq2
20 19 fveq2d
21 fveq2 ${⊢}{y}={Y}\to {F}\left({y}\right)={F}\left({Y}\right)$
22 21 oveq2d ${⊢}{y}={Y}\to {F}\left({X}\right)+{F}\left({y}\right)={F}\left({X}\right)+{F}\left({Y}\right)$
23 20 22 breq12d
24 18 23 rspc2v
25 14 24 syl5com
26 25 3impib