# Metamath Proof Explorer

## Theorem abv1z

Description: The absolute value of one is one in a non-trivial ring. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abv0.a
`|- A = ( AbsVal ` R )`
abv1.p
`|- .1. = ( 1r ` R )`
abv1z.z
`|- .0. = ( 0g ` R )`
Assertion abv1z
`|- ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) = 1 )`

### Proof

Step Hyp Ref Expression
1 abv0.a
` |-  A = ( AbsVal ` R )`
2 abv1.p
` |-  .1. = ( 1r ` R )`
3 abv1z.z
` |-  .0. = ( 0g ` R )`
4 1 abvrcl
` |-  ( F e. A -> R e. Ring )`
5 eqid
` |-  ( Base ` R ) = ( Base ` R )`
6 5 2 ringidcl
` |-  ( R e. Ring -> .1. e. ( Base ` R ) )`
7 4 6 syl
` |-  ( F e. A -> .1. e. ( Base ` R ) )`
8 1 5 abvcl
` |-  ( ( F e. A /\ .1. e. ( Base ` R ) ) -> ( F ` .1. ) e. RR )`
9 7 8 mpdan
` |-  ( F e. A -> ( F ` .1. ) e. RR )`
` |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) e. RR )`
11 10 recnd
` |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) e. CC )`
12 simpl
` |-  ( ( F e. A /\ .1. =/= .0. ) -> F e. A )`
` |-  ( ( F e. A /\ .1. =/= .0. ) -> .1. e. ( Base ` R ) )`
14 simpr
` |-  ( ( F e. A /\ .1. =/= .0. ) -> .1. =/= .0. )`
15 1 5 3 abvne0
` |-  ( ( F e. A /\ .1. e. ( Base ` R ) /\ .1. =/= .0. ) -> ( F ` .1. ) =/= 0 )`
16 12 13 14 15 syl3anc
` |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) =/= 0 )`
17 11 11 16 divcan3d
` |-  ( ( F e. A /\ .1. =/= .0. ) -> ( ( ( F ` .1. ) x. ( F ` .1. ) ) / ( F ` .1. ) ) = ( F ` .1. ) )`
18 eqid
` |-  ( .r ` R ) = ( .r ` R )`
19 5 18 2 ringlidm
` |-  ( ( R e. Ring /\ .1. e. ( Base ` R ) ) -> ( .1. ( .r ` R ) .1. ) = .1. )`
20 4 13 19 syl2an2r
` |-  ( ( F e. A /\ .1. =/= .0. ) -> ( .1. ( .r ` R ) .1. ) = .1. )`
21 20 fveq2d
` |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` ( .1. ( .r ` R ) .1. ) ) = ( F ` .1. ) )`
22 1 5 18 abvmul
` |-  ( ( F e. A /\ .1. e. ( Base ` R ) /\ .1. e. ( Base ` R ) ) -> ( F ` ( .1. ( .r ` R ) .1. ) ) = ( ( F ` .1. ) x. ( F ` .1. ) ) )`
23 12 13 13 22 syl3anc
` |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` ( .1. ( .r ` R ) .1. ) ) = ( ( F ` .1. ) x. ( F ` .1. ) ) )`
24 21 23 eqtr3d
` |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) = ( ( F ` .1. ) x. ( F ` .1. ) ) )`
25 24 oveq1d
` |-  ( ( F e. A /\ .1. =/= .0. ) -> ( ( F ` .1. ) / ( F ` .1. ) ) = ( ( ( F ` .1. ) x. ( F ` .1. ) ) / ( F ` .1. ) ) )`
26 11 16 dividd
` |-  ( ( F e. A /\ .1. =/= .0. ) -> ( ( F ` .1. ) / ( F ` .1. ) ) = 1 )`
27 25 26 eqtr3d
` |-  ( ( F e. A /\ .1. =/= .0. ) -> ( ( ( F ` .1. ) x. ( F ` .1. ) ) / ( F ` .1. ) ) = 1 )`
28 17 27 eqtr3d
` |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) = 1 )`