abvdiv

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

	Ref	Expression
Hypotheses	abv0.a	$⊢ A = AbsVal (R)$
	abvneg.b	$⊢ B = {Base}_{R}$
	abvrec.z	$⊢ \underset{˙}{0} = 0_{R}$
	abvdiv.p	$⊢ \underset{˙}{\times} = /_{r} (R)$
Assertion	abvdiv	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F (X \underset{˙}{\times} Y) = \frac{F (X)}{F (Y)}$

Proof

Step	Hyp	Ref	Expression
1		abv0.a	$⊢ A = AbsVal (R)$
2		abvneg.b	$⊢ B = {Base}_{R}$
3		abvrec.z	$⊢ \underset{˙}{0} = 0_{R}$
4		abvdiv.p	$⊢ \underset{˙}{\times} = /_{r} (R)$
5		simplr	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F \in A$
6		simpr1	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to X \in B$
7		simpll	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to R \in DivRing$
8		simpr2	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to Y \in B$
9		simpr3	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to Y \neq \underset{˙}{0}$
10		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
11	2 3 10	drnginvrcl	$⊢ (R \in DivRing \land Y \in B \land Y \neq \underset{˙}{0}) \to {inv}_{r} (R) (Y) \in B$
12	7 8 9 11	syl3anc	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to {inv}_{r} (R) (Y) \in B$
13		eqid	$⊢ \cdot_{R} = \cdot_{R}$
14	1 2 13	abvmul	$⊢ (F \in A \land X \in B \land {inv}_{r} (R) (Y) \in B) \to F (X \cdot_{R} {inv}_{r} (R) (Y)) = F (X) F ({inv}_{r} (R) (Y))$
15	5 6 12 14	syl3anc	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F (X \cdot_{R} {inv}_{r} (R) (Y)) = F (X) F ({inv}_{r} (R) (Y))$
16	1 2 3 10	abvrec	$⊢ ((R \in DivRing \land F \in A) \land (Y \in B \land Y \neq \underset{˙}{0})) \to F ({inv}_{r} (R) (Y)) = \frac{1}{F (Y)}$
17	16	3adantr1	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F ({inv}_{r} (R) (Y)) = \frac{1}{F (Y)}$
18	17	oveq2d	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F (X) F ({inv}_{r} (R) (Y)) = F (X) (\frac{1}{F (Y)})$
19	15 18	eqtrd	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F (X \cdot_{R} {inv}_{r} (R) (Y)) = F (X) (\frac{1}{F (Y)})$
20		eqid	$⊢ Unit (R) = Unit (R)$
21	2 20 3	drngunit	$⊢ R \in DivRing \to (Y \in Unit (R) \leftrightarrow (Y \in B \land Y \neq \underset{˙}{0}))$
22	7 21	syl	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to (Y \in Unit (R) \leftrightarrow (Y \in B \land Y \neq \underset{˙}{0}))$
23	8 9 22	mpbir2and	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to Y \in Unit (R)$
24	2 13 20 10 4	dvrval	$⊢ (X \in B \land Y \in Unit (R)) \to X \underset{˙}{\times} Y = X \cdot_{R} {inv}_{r} (R) (Y)$
25	6 23 24	syl2anc	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to X \underset{˙}{\times} Y = X \cdot_{R} {inv}_{r} (R) (Y)$
26	25	fveq2d	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F (X \underset{˙}{\times} Y) = F (X \cdot_{R} {inv}_{r} (R) (Y))$
27	1 2	abvcl	$⊢ (F \in A \land X \in B) \to F (X) \in ℝ$
28	5 6 27	syl2anc	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F (X) \in ℝ$
29	28	recnd	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F (X) \in ℂ$
30	1 2	abvcl	$⊢ (F \in A \land Y \in B) \to F (Y) \in ℝ$
31	5 8 30	syl2anc	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F (Y) \in ℝ$
32	31	recnd	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F (Y) \in ℂ$
33	1 2 3	abvne0	$⊢ (F \in A \land Y \in B \land Y \neq \underset{˙}{0}) \to F (Y) \neq 0$
34	5 8 9 33	syl3anc	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F (Y) \neq 0$
35	29 32 34	divrecd	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to \frac{F (X)}{F (Y)} = F (X) (\frac{1}{F (Y)})$
36	19 26 35	3eqtr4d	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land Y \in B \land Y \neq \underset{˙}{0})) \to F (X \underset{˙}{\times} Y) = \frac{F (X)}{F (Y)}$

Metamath Proof Explorer

Theorem abvdiv

Proof