# Metamath Proof Explorer

## Theorem abvmul

Description: An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abvf.a ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
abvf.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
abvmul.t
Assertion abvmul

### Proof

Step Hyp Ref Expression
1 abvf.a ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
2 abvf.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 abvmul.t
4 1 abvrcl ${⊢}{F}\in {A}\to {R}\in \mathrm{Ring}$
5 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
6 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
7 1 2 5 3 6 isabv
8 4 7 syl
9 8 ibi
10 simpl
11 10 ralimi
13 12 ralimi
14 9 13 simpl2im
15 fvoveq1
16 fveq2 ${⊢}{x}={X}\to {F}\left({x}\right)={F}\left({X}\right)$
17 16 oveq1d ${⊢}{x}={X}\to {F}\left({x}\right){F}\left({y}\right)={F}\left({X}\right){F}\left({y}\right)$
18 15 17 eqeq12d
19 oveq2
20 19 fveq2d
21 fveq2 ${⊢}{y}={Y}\to {F}\left({y}\right)={F}\left({Y}\right)$
22 21 oveq2d ${⊢}{y}={Y}\to {F}\left({X}\right){F}\left({y}\right)={F}\left({X}\right){F}\left({Y}\right)$
23 20 22 eqeq12d
24 18 23 rspc2v
25 14 24 syl5com
26 25 3impib