# Metamath Proof Explorer

## Theorem abvdiv

Description: The absolute value distributes under division. (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 )`
abvdiv.p
`|- ./ = ( /r ` R )`
Assertion abvdiv
`|- ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( 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 abvrec.z
` |-  .0. = ( 0g ` R )`
4 abvdiv.p
` |-  ./ = ( /r ` R )`
5 simplr
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> F e. A )`
6 simpr1
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> X e. B )`
7 simpll
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> R e. DivRing )`
8 simpr2
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> Y e. B )`
9 simpr3
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> Y =/= .0. )`
10 eqid
` |-  ( invr ` R ) = ( invr ` R )`
11 2 3 10 drnginvrcl
` |-  ( ( R e. DivRing /\ Y e. B /\ Y =/= .0. ) -> ( ( invr ` R ) ` Y ) e. B )`
12 7 8 9 11 syl3anc
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( ( invr ` R ) ` Y ) e. B )`
13 eqid
` |-  ( .r ` R ) = ( .r ` R )`
14 1 2 13 abvmul
` |-  ( ( F e. A /\ X e. B /\ ( ( invr ` R ) ` Y ) e. B ) -> ( F ` ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) ) = ( ( F ` X ) x. ( F ` ( ( invr ` R ) ` Y ) ) ) )`
15 5 6 12 14 syl3anc
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( F ` ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) ) = ( ( F ` X ) x. ( F ` ( ( invr ` R ) ` Y ) ) ) )`
16 1 2 3 10 abvrec
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( F ` ( ( invr ` R ) ` Y ) ) = ( 1 / ( F ` Y ) ) )`
17 16 3adantr1
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( F ` ( ( invr ` R ) ` Y ) ) = ( 1 / ( F ` Y ) ) )`
18 17 oveq2d
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( ( F ` X ) x. ( F ` ( ( invr ` R ) ` Y ) ) ) = ( ( F ` X ) x. ( 1 / ( F ` Y ) ) ) )`
19 15 18 eqtrd
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( F ` ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) ) = ( ( F ` X ) x. ( 1 / ( F ` Y ) ) ) )`
20 eqid
` |-  ( Unit ` R ) = ( Unit ` R )`
21 2 20 3 drngunit
` |-  ( R e. DivRing -> ( Y e. ( Unit ` R ) <-> ( Y e. B /\ Y =/= .0. ) ) )`
22 7 21 syl
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( Y e. ( Unit ` R ) <-> ( Y e. B /\ Y =/= .0. ) ) )`
23 8 9 22 mpbir2and
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> Y e. ( Unit ` R ) )`
24 2 13 20 10 4 dvrval
` |-  ( ( X e. B /\ Y e. ( Unit ` R ) ) -> ( X ./ Y ) = ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) )`
25 6 23 24 syl2anc
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( X ./ Y ) = ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) )`
26 25 fveq2d
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( F ` ( X ./ Y ) ) = ( F ` ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) ) )`
27 1 2 abvcl
` |-  ( ( F e. A /\ X e. B ) -> ( F ` X ) e. RR )`
28 5 6 27 syl2anc
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( F ` X ) e. RR )`
29 28 recnd
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( F ` X ) e. CC )`
30 1 2 abvcl
` |-  ( ( F e. A /\ Y e. B ) -> ( F ` Y ) e. RR )`
31 5 8 30 syl2anc
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( F ` Y ) e. RR )`
32 31 recnd
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( F ` Y ) e. CC )`
33 1 2 3 abvne0
` |-  ( ( F e. A /\ Y e. B /\ Y =/= .0. ) -> ( F ` Y ) =/= 0 )`
34 5 8 9 33 syl3anc
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( F ` Y ) =/= 0 )`
35 29 32 34 divrecd
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( ( F ` X ) / ( F ` Y ) ) = ( ( F ` X ) x. ( 1 / ( F ` Y ) ) ) )`
36 19 26 35 3eqtr4d
` |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( F ` ( X ./ Y ) ) = ( ( F ` X ) / ( F ` Y ) ) )`