# 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}=\mathrm{AbsVal}\left({R}\right)$
abvneg.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
abvrec.z
abvrec.p ${⊢}{I}={inv}_{r}\left({R}\right)$
Assertion abvrec

### Proof

Step Hyp Ref Expression
1 abv0.a ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
2 abvneg.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 abvrec.z
4 abvrec.p ${⊢}{I}={inv}_{r}\left({R}\right)$
5 simplr
6 simprl
7 1 2 abvcl ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {F}\left({X}\right)\in ℝ$
8 5 6 7 syl2anc
9 8 recnd
10 simpll
11 simprr
12 2 3 4 drnginvrcl
13 10 6 11 12 syl3anc
14 1 2 abvcl ${⊢}\left({F}\in {A}\wedge {I}\left({X}\right)\in {B}\right)\to {F}\left({I}\left({X}\right)\right)\in ℝ$
15 5 13 14 syl2anc
16 15 recnd
17 1 2 3 abvne0
18 5 6 11 17 syl3anc
19 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
20 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
21 2 3 19 20 4 drnginvrr
22 10 6 11 21 syl3anc
23 22 fveq2d
24 1 2 19 abvmul ${⊢}\left({F}\in {A}\wedge {X}\in {B}\wedge {I}\left({X}\right)\in {B}\right)\to {F}\left({X}{\cdot }_{{R}}{I}\left({X}\right)\right)={F}\left({X}\right){F}\left({I}\left({X}\right)\right)$
25 5 6 13 24 syl3anc
26 1 20 abv1 ${⊢}\left({R}\in \mathrm{DivRing}\wedge {F}\in {A}\right)\to {F}\left({1}_{{R}}\right)=1$