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