# Metamath Proof Explorer

## Theorem abvsubtri

Description: An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 4-Oct-2015)

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

### Proof

Step Hyp Ref Expression
1 abv0.a ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
2 abvneg.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 abvsubtri.p
4 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
5 eqid ${⊢}{inv}_{g}\left({R}\right)={inv}_{g}\left({R}\right)$
6 2 4 5 3 grpsubval
8 7 fveq2d
9 1 abvrcl ${⊢}{F}\in {A}\to {R}\in \mathrm{Ring}$
10 9 3ad2ant1 ${⊢}\left({F}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {R}\in \mathrm{Ring}$
11 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
12 10 11 syl ${⊢}\left({F}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {R}\in \mathrm{Grp}$
13 simp3 ${⊢}\left({F}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in {B}$
14 2 5 grpinvcl ${⊢}\left({R}\in \mathrm{Grp}\wedge {Y}\in {B}\right)\to {inv}_{g}\left({R}\right)\left({Y}\right)\in {B}$
15 12 13 14 syl2anc ${⊢}\left({F}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {inv}_{g}\left({R}\right)\left({Y}\right)\in {B}$
16 1 2 4 abvtri ${⊢}\left({F}\in {A}\wedge {X}\in {B}\wedge {inv}_{g}\left({R}\right)\left({Y}\right)\in {B}\right)\to {F}\left({X}{+}_{{R}}{inv}_{g}\left({R}\right)\left({Y}\right)\right)\le {F}\left({X}\right)+{F}\left({inv}_{g}\left({R}\right)\left({Y}\right)\right)$
17 15 16 syld3an3 ${⊢}\left({F}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {F}\left({X}{+}_{{R}}{inv}_{g}\left({R}\right)\left({Y}\right)\right)\le {F}\left({X}\right)+{F}\left({inv}_{g}\left({R}\right)\left({Y}\right)\right)$
18 1 2 5 abvneg ${⊢}\left({F}\in {A}\wedge {Y}\in {B}\right)\to {F}\left({inv}_{g}\left({R}\right)\left({Y}\right)\right)={F}\left({Y}\right)$
19 18 3adant2 ${⊢}\left({F}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {F}\left({inv}_{g}\left({R}\right)\left({Y}\right)\right)={F}\left({Y}\right)$
20 19 oveq2d ${⊢}\left({F}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {F}\left({X}\right)+{F}\left({inv}_{g}\left({R}\right)\left({Y}\right)\right)={F}\left({X}\right)+{F}\left({Y}\right)$
21 17 20 breqtrd ${⊢}\left({F}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {F}\left({X}{+}_{{R}}{inv}_{g}\left({R}\right)\left({Y}\right)\right)\le {F}\left({X}\right)+{F}\left({Y}\right)$
22 8 21 eqbrtrd