# Metamath Proof Explorer

## Theorem abvdiv

Description: The absolute value distributes under division. (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses abv0.a 𝐴 = ( AbsVal ‘ 𝑅 )
abvneg.b 𝐵 = ( Base ‘ 𝑅 )
abvrec.z 0 = ( 0g𝑅 )
abvdiv.p / = ( /r𝑅 )
Assertion abvdiv ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝐹 ‘ ( 𝑋 / 𝑌 ) ) = ( ( 𝐹𝑋 ) / ( 𝐹𝑌 ) ) )

### Proof

Step Hyp Ref Expression
1 abv0.a 𝐴 = ( AbsVal ‘ 𝑅 )
2 abvneg.b 𝐵 = ( Base ‘ 𝑅 )
3 abvrec.z 0 = ( 0g𝑅 )
4 abvdiv.p / = ( /r𝑅 )
5 simplr ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → 𝐹𝐴 )
6 simpr1 ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → 𝑋𝐵 )
7 simpll ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → 𝑅 ∈ DivRing )
8 simpr2 ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → 𝑌𝐵 )
9 simpr3 ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → 𝑌0 )
10 eqid ( invr𝑅 ) = ( invr𝑅 )
11 2 3 10 drnginvrcl ( ( 𝑅 ∈ DivRing ∧ 𝑌𝐵𝑌0 ) → ( ( invr𝑅 ) ‘ 𝑌 ) ∈ 𝐵 )
12 7 8 9 11 syl3anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( ( invr𝑅 ) ‘ 𝑌 ) ∈ 𝐵 )
13 eqid ( .r𝑅 ) = ( .r𝑅 )
14 1 2 13 abvmul ( ( 𝐹𝐴𝑋𝐵 ∧ ( ( invr𝑅 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 ( .r𝑅 ) ( ( invr𝑅 ) ‘ 𝑌 ) ) ) = ( ( 𝐹𝑋 ) · ( 𝐹 ‘ ( ( invr𝑅 ) ‘ 𝑌 ) ) ) )
15 5 6 12 14 syl3anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝐹 ‘ ( 𝑋 ( .r𝑅 ) ( ( invr𝑅 ) ‘ 𝑌 ) ) ) = ( ( 𝐹𝑋 ) · ( 𝐹 ‘ ( ( invr𝑅 ) ‘ 𝑌 ) ) ) )
16 1 2 3 10 abvrec ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( 𝐹 ‘ ( ( invr𝑅 ) ‘ 𝑌 ) ) = ( 1 / ( 𝐹𝑌 ) ) )
17 16 3adantr1 ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝐹 ‘ ( ( invr𝑅 ) ‘ 𝑌 ) ) = ( 1 / ( 𝐹𝑌 ) ) )
18 17 oveq2d ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( ( 𝐹𝑋 ) · ( 𝐹 ‘ ( ( invr𝑅 ) ‘ 𝑌 ) ) ) = ( ( 𝐹𝑋 ) · ( 1 / ( 𝐹𝑌 ) ) ) )
19 15 18 eqtrd ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝐹 ‘ ( 𝑋 ( .r𝑅 ) ( ( invr𝑅 ) ‘ 𝑌 ) ) ) = ( ( 𝐹𝑋 ) · ( 1 / ( 𝐹𝑌 ) ) ) )
20 eqid ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
21 2 20 3 drngunit ( 𝑅 ∈ DivRing → ( 𝑌 ∈ ( Unit ‘ 𝑅 ) ↔ ( 𝑌𝐵𝑌0 ) ) )
22 7 21 syl ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝑌 ∈ ( Unit ‘ 𝑅 ) ↔ ( 𝑌𝐵𝑌0 ) ) )
23 8 9 22 mpbir2and ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → 𝑌 ∈ ( Unit ‘ 𝑅 ) )
24 2 13 20 10 4 dvrval ( ( 𝑋𝐵𝑌 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 / 𝑌 ) = ( 𝑋 ( .r𝑅 ) ( ( invr𝑅 ) ‘ 𝑌 ) ) )
25 6 23 24 syl2anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝑋 / 𝑌 ) = ( 𝑋 ( .r𝑅 ) ( ( invr𝑅 ) ‘ 𝑌 ) ) )
26 25 fveq2d ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝐹 ‘ ( 𝑋 / 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 ( .r𝑅 ) ( ( invr𝑅 ) ‘ 𝑌 ) ) ) )
27 1 2 abvcl ( ( 𝐹𝐴𝑋𝐵 ) → ( 𝐹𝑋 ) ∈ ℝ )
28 5 6 27 syl2anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝐹𝑋 ) ∈ ℝ )
29 28 recnd ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝐹𝑋 ) ∈ ℂ )
30 1 2 abvcl ( ( 𝐹𝐴𝑌𝐵 ) → ( 𝐹𝑌 ) ∈ ℝ )
31 5 8 30 syl2anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝐹𝑌 ) ∈ ℝ )
32 31 recnd ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝐹𝑌 ) ∈ ℂ )
33 1 2 3 abvne0 ( ( 𝐹𝐴𝑌𝐵𝑌0 ) → ( 𝐹𝑌 ) ≠ 0 )
34 5 8 9 33 syl3anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝐹𝑌 ) ≠ 0 )
35 29 32 34 divrecd ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( ( 𝐹𝑋 ) / ( 𝐹𝑌 ) ) = ( ( 𝐹𝑋 ) · ( 1 / ( 𝐹𝑌 ) ) ) )
36 19 26 35 3eqtr4d ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑌𝐵𝑌0 ) ) → ( 𝐹 ‘ ( 𝑋 / 𝑌 ) ) = ( ( 𝐹𝑋 ) / ( 𝐹𝑌 ) ) )