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 ) ) )