# Metamath Proof Explorer

## Theorem abvmul

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

Ref Expression
Hypotheses abvf.a 𝐴 = ( AbsVal ‘ 𝑅 )
abvf.b 𝐵 = ( Base ‘ 𝑅 )
abvmul.t · = ( .r𝑅 )
Assertion abvmul ( ( 𝐹𝐴𝑋𝐵𝑌𝐵 ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹𝑋 ) · ( 𝐹𝑌 ) ) )

### Proof

Step Hyp Ref Expression
1 abvf.a 𝐴 = ( AbsVal ‘ 𝑅 )
2 abvf.b 𝐵 = ( Base ‘ 𝑅 )
3 abvmul.t · = ( .r𝑅 )
4 1 abvrcl ( 𝐹𝐴𝑅 ∈ Ring )
5 eqid ( +g𝑅 ) = ( +g𝑅 )
6 eqid ( 0g𝑅 ) = ( 0g𝑅 )
7 1 2 5 3 6 isabv ( 𝑅 ∈ Ring → ( 𝐹𝐴 ↔ ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥𝐵 ( ( ( 𝐹𝑥 ) = 0 ↔ 𝑥 = ( 0g𝑅 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹𝑥 ) + ( 𝐹𝑦 ) ) ) ) ) ) )
8 4 7 syl ( 𝐹𝐴 → ( 𝐹𝐴 ↔ ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥𝐵 ( ( ( 𝐹𝑥 ) = 0 ↔ 𝑥 = ( 0g𝑅 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹𝑥 ) + ( 𝐹𝑦 ) ) ) ) ) ) )
9 8 ibi ( 𝐹𝐴 → ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥𝐵 ( ( ( 𝐹𝑥 ) = 0 ↔ 𝑥 = ( 0g𝑅 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹𝑥 ) + ( 𝐹𝑦 ) ) ) ) ) )
10 simpl ( ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹𝑥 ) + ( 𝐹𝑦 ) ) ) → ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) )
11 10 ralimi ( ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹𝑥 ) + ( 𝐹𝑦 ) ) ) → ∀ 𝑦𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) )
12 11 adantl ( ( ( ( 𝐹𝑥 ) = 0 ↔ 𝑥 = ( 0g𝑅 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹𝑥 ) + ( 𝐹𝑦 ) ) ) ) → ∀ 𝑦𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) )
13 12 ralimi ( ∀ 𝑥𝐵 ( ( ( 𝐹𝑥 ) = 0 ↔ 𝑥 = ( 0g𝑅 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹𝑥 ) + ( 𝐹𝑦 ) ) ) ) → ∀ 𝑥𝐵𝑦𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) )
14 9 13 simpl2im ( 𝐹𝐴 → ∀ 𝑥𝐵𝑦𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) )
15 fvoveq1 ( 𝑥 = 𝑋 → ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑦 ) ) )
16 fveq2 ( 𝑥 = 𝑋 → ( 𝐹𝑥 ) = ( 𝐹𝑋 ) )
17 16 oveq1d ( 𝑥 = 𝑋 → ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) = ( ( 𝐹𝑋 ) · ( 𝐹𝑦 ) ) )
18 15 17 eqeq12d ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑋 · 𝑦 ) ) = ( ( 𝐹𝑋 ) · ( 𝐹𝑦 ) ) ) )
19 oveq2 ( 𝑦 = 𝑌 → ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) )
20 19 fveq2d ( 𝑦 = 𝑌 → ( 𝐹 ‘ ( 𝑋 · 𝑦 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
21 fveq2 ( 𝑦 = 𝑌 → ( 𝐹𝑦 ) = ( 𝐹𝑌 ) )
22 21 oveq2d ( 𝑦 = 𝑌 → ( ( 𝐹𝑋 ) · ( 𝐹𝑦 ) ) = ( ( 𝐹𝑋 ) · ( 𝐹𝑌 ) ) )
23 20 22 eqeq12d ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ ( 𝑋 · 𝑦 ) ) = ( ( 𝐹𝑋 ) · ( 𝐹𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹𝑋 ) · ( 𝐹𝑌 ) ) ) )
24 18 23 rspc2v ( ( 𝑋𝐵𝑌𝐵 ) → ( ∀ 𝑥𝐵𝑦𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹𝑋 ) · ( 𝐹𝑌 ) ) ) )
25 14 24 syl5com ( 𝐹𝐴 → ( ( 𝑋𝐵𝑌𝐵 ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹𝑋 ) · ( 𝐹𝑌 ) ) ) )
26 25 3impib ( ( 𝐹𝐴𝑋𝐵𝑌𝐵 ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹𝑋 ) · ( 𝐹𝑌 ) ) )