# Metamath Proof Explorer

## Theorem abvrec

Description: The absolute value distributes under reciprocal. (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses abv0.a
`|- A = ( AbsVal ` R )`
abvneg.b
`|- B = ( Base ` R )`
abvrec.z
`|- .0. = ( 0g ` R )`
abvrec.p
`|- I = ( invr ` R )`
Assertion abvrec
`|- ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` ( I ` X ) ) = ( 1 / ( F ` X ) ) )`

### Proof

Step Hyp Ref Expression
1 abv0.a
` |-  A = ( AbsVal ` R )`
2 abvneg.b
` |-  B = ( Base ` R )`
3 abvrec.z
` |-  .0. = ( 0g ` R )`
4 abvrec.p
` |-  I = ( invr ` R )`
5 simplr
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> F e. A )`
6 simprl
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> X e. B )`
7 1 2 abvcl
` |-  ( ( F e. A /\ X e. B ) -> ( F ` X ) e. RR )`
8 5 6 7 syl2anc
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` X ) e. RR )`
9 8 recnd
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` X ) e. CC )`
10 simpll
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> R e. DivRing )`
11 simprr
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> X =/= .0. )`
12 2 3 4 drnginvrcl
` |-  ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( I ` X ) e. B )`
13 10 6 11 12 syl3anc
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( I ` X ) e. B )`
14 1 2 abvcl
` |-  ( ( F e. A /\ ( I ` X ) e. B ) -> ( F ` ( I ` X ) ) e. RR )`
15 5 13 14 syl2anc
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` ( I ` X ) ) e. RR )`
16 15 recnd
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` ( I ` X ) ) e. CC )`
17 1 2 3 abvne0
` |-  ( ( F e. A /\ X e. B /\ X =/= .0. ) -> ( F ` X ) =/= 0 )`
18 5 6 11 17 syl3anc
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` X ) =/= 0 )`
19 eqid
` |-  ( .r ` R ) = ( .r ` R )`
20 eqid
` |-  ( 1r ` R ) = ( 1r ` R )`
21 2 3 19 20 4 drnginvrr
` |-  ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( X ( .r ` R ) ( I ` X ) ) = ( 1r ` R ) )`
22 10 6 11 21 syl3anc
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( X ( .r ` R ) ( I ` X ) ) = ( 1r ` R ) )`
23 22 fveq2d
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` ( X ( .r ` R ) ( I ` X ) ) ) = ( F ` ( 1r ` R ) ) )`
24 1 2 19 abvmul
` |-  ( ( F e. A /\ X e. B /\ ( I ` X ) e. B ) -> ( F ` ( X ( .r ` R ) ( I ` X ) ) ) = ( ( F ` X ) x. ( F ` ( I ` X ) ) ) )`
25 5 6 13 24 syl3anc
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` ( X ( .r ` R ) ( I ` X ) ) ) = ( ( F ` X ) x. ( F ` ( I ` X ) ) ) )`
26 1 20 abv1
` |-  ( ( R e. DivRing /\ F e. A ) -> ( F ` ( 1r ` R ) ) = 1 )`
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` ( 1r ` R ) ) = 1 )`
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( ( F ` X ) x. ( F ` ( I ` X ) ) ) = 1 )`
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` ( I ` X ) ) = ( 1 / ( F ` X ) ) )`