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 )
27 26 adantr 
 |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` ( 1r ` R ) ) = 1 )
28 23 25 27 3eqtr3d 
 |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( ( F ` X ) x. ( F ` ( I ` X ) ) ) = 1 )
29 9 16 18 28 mvllmuld 
 |-  ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` ( I ` X ) ) = ( 1 / ( F ` X ) ) )