# Metamath Proof Explorer

## Theorem abvtriv

Description: The trivial absolute value. (This theorem is true as long as R is a domain, but it is not true for rings with zero divisors, which violate the multiplication axiom; abvdom is the converse of this remark.) (Contributed by Mario Carneiro, 8-Sep-2014) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses abvtriv.a
`|- A = ( AbsVal ` R )`
abvtriv.b
`|- B = ( Base ` R )`
abvtriv.z
`|- .0. = ( 0g ` R )`
abvtriv.f
`|- F = ( x e. B |-> if ( x = .0. , 0 , 1 ) )`
Assertion abvtriv
`|- ( R e. DivRing -> F e. A )`

### Proof

Step Hyp Ref Expression
1 abvtriv.a
` |-  A = ( AbsVal ` R )`
2 abvtriv.b
` |-  B = ( Base ` R )`
3 abvtriv.z
` |-  .0. = ( 0g ` R )`
4 abvtriv.f
` |-  F = ( x e. B |-> if ( x = .0. , 0 , 1 ) )`
5 eqid
` |-  ( .r ` R ) = ( .r ` R )`
6 drngring
` |-  ( R e. DivRing -> R e. Ring )`
7 biid
` |-  ( R e. DivRing <-> R e. DivRing )`
8 eldifsn
` |-  ( y e. ( B \ { .0. } ) <-> ( y e. B /\ y =/= .0. ) )`
9 eldifsn
` |-  ( z e. ( B \ { .0. } ) <-> ( z e. B /\ z =/= .0. ) )`
10 2 5 3 drngmcl
` |-  ( ( R e. DivRing /\ y e. ( B \ { .0. } ) /\ z e. ( B \ { .0. } ) ) -> ( y ( .r ` R ) z ) e. ( B \ { .0. } ) )`
11 7 8 9 10 syl3anbr
` |-  ( ( R e. DivRing /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y ( .r ` R ) z ) e. ( B \ { .0. } ) )`
12 eldifsn
` |-  ( ( y ( .r ` R ) z ) e. ( B \ { .0. } ) <-> ( ( y ( .r ` R ) z ) e. B /\ ( y ( .r ` R ) z ) =/= .0. ) )`
13 11 12 sylib
` |-  ( ( R e. DivRing /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( ( y ( .r ` R ) z ) e. B /\ ( y ( .r ` R ) z ) =/= .0. ) )`
14 13 simprd
` |-  ( ( R e. DivRing /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y ( .r ` R ) z ) =/= .0. )`
15 1 2 3 4 5 6 14 abvtrivd
` |-  ( R e. DivRing -> F e. A )`