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 ) ) → ( 𝐹 ‘ ( 𝑋 / 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) / ( 𝐹 ‘ 𝑌 ) ) )