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 = ( AbsVal ` R )`
abvneg.b
`|- B = ( Base ` R )`
abvsubtri.p
`|- .- = ( -g ` R )`
Assertion abvsubtri
`|- ( ( F e. A /\ X e. B /\ Y e. B ) -> ( F ` ( X .- Y ) ) <_ ( ( F ` X ) + ( F ` Y ) ) )`

Proof

Step Hyp Ref Expression
1 abv0.a
` |-  A = ( AbsVal ` R )`
2 abvneg.b
` |-  B = ( Base ` R )`
3 abvsubtri.p
` |-  .- = ( -g ` R )`
4 eqid
` |-  ( +g ` R ) = ( +g ` R )`
5 eqid
` |-  ( invg ` R ) = ( invg ` R )`
6 2 4 5 3 grpsubval
` |-  ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X ( +g ` R ) ( ( invg ` R ) ` Y ) ) )`
` |-  ( ( F e. A /\ X e. B /\ Y e. B ) -> ( X .- Y ) = ( X ( +g ` R ) ( ( invg ` R ) ` Y ) ) )`
8 7 fveq2d
` |-  ( ( F e. A /\ X e. B /\ Y e. B ) -> ( F ` ( X .- Y ) ) = ( F ` ( X ( +g ` R ) ( ( invg ` R ) ` Y ) ) ) )`
9 1 abvrcl
` |-  ( F e. A -> R e. Ring )`
` |-  ( ( F e. A /\ X e. B /\ Y e. B ) -> R e. Ring )`
11 ringgrp
` |-  ( R e. Ring -> R e. Grp )`
12 10 11 syl
` |-  ( ( F e. A /\ X e. B /\ Y e. B ) -> R e. Grp )`
13 simp3
` |-  ( ( F e. A /\ X e. B /\ Y e. B ) -> Y e. B )`
14 2 5 grpinvcl
` |-  ( ( R e. Grp /\ Y e. B ) -> ( ( invg ` R ) ` Y ) e. B )`
15 12 13 14 syl2anc
` |-  ( ( F e. A /\ X e. B /\ Y e. B ) -> ( ( invg ` R ) ` Y ) e. B )`
16 1 2 4 abvtri
` |-  ( ( F e. A /\ X e. B /\ ( ( invg ` R ) ` Y ) e. B ) -> ( F ` ( X ( +g ` R ) ( ( invg ` R ) ` Y ) ) ) <_ ( ( F ` X ) + ( F ` ( ( invg ` R ) ` Y ) ) ) )`
17 15 16 syld3an3
` |-  ( ( F e. A /\ X e. B /\ Y e. B ) -> ( F ` ( X ( +g ` R ) ( ( invg ` R ) ` Y ) ) ) <_ ( ( F ` X ) + ( F ` ( ( invg ` R ) ` Y ) ) ) )`
18 1 2 5 abvneg
` |-  ( ( F e. A /\ Y e. B ) -> ( F ` ( ( invg ` R ) ` Y ) ) = ( F ` Y ) )`
` |-  ( ( F e. A /\ X e. B /\ Y e. B ) -> ( F ` ( ( invg ` R ) ` Y ) ) = ( F ` Y ) )`
` |-  ( ( F e. A /\ X e. B /\ Y e. B ) -> ( ( F ` X ) + ( F ` ( ( invg ` R ) ` Y ) ) ) = ( ( F ` X ) + ( F ` Y ) ) )`
` |-  ( ( F e. A /\ X e. B /\ Y e. B ) -> ( F ` ( X ( +g ` R ) ( ( invg ` R ) ` Y ) ) ) <_ ( ( F ` X ) + ( F ` Y ) ) )`
` |-  ( ( F e. A /\ X e. B /\ Y e. B ) -> ( F ` ( X .- Y ) ) <_ ( ( F ` X ) + ( F ` Y ) ) )`