abvrec

Description: The absolute value distributes under reciprocal. (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}$
	abvrec.p	$⊢ I = {inv}_{r} (R)$
Assertion	abvrec	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to F (I (X)) = \frac{1}{F (X)}$

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		abvrec.p	$⊢ I = {inv}_{r} (R)$
5		simplr	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to F \in A$
6		simprl	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to X \in B$
7	1 2	abvcl	$⊢ (F \in A \land X \in B) \to F (X) \in ℝ$
8	5 6 7	syl2anc	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to F (X) \in ℝ$
9	8	recnd	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to F (X) \in ℂ$
10		simpll	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to R \in DivRing$
11		simprr	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to X \neq \underset{˙}{0}$
12	2 3 4	drnginvrcl	$⊢ (R \in DivRing \land X \in B \land X \neq \underset{˙}{0}) \to I (X) \in B$
13	10 6 11 12	syl3anc	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to I (X) \in B$
14	1 2	abvcl	$⊢ (F \in A \land I (X) \in B) \to F (I (X)) \in ℝ$
15	5 13 14	syl2anc	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to F (I (X)) \in ℝ$
16	15	recnd	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to F (I (X)) \in ℂ$
17	1 2 3	abvne0	$⊢ (F \in A \land X \in B \land X \neq \underset{˙}{0}) \to F (X) \neq 0$
18	5 6 11 17	syl3anc	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to F (X) \neq 0$
19		eqid	$⊢ \cdot_{R} = \cdot_{R}$
20		eqid	$⊢ 1_{R} = 1_{R}$
21	2 3 19 20 4	drnginvrr	$⊢ (R \in DivRing \land X \in B \land X \neq \underset{˙}{0}) \to X \cdot_{R} I (X) = 1_{R}$
22	10 6 11 21	syl3anc	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to X \cdot_{R} I (X) = 1_{R}$
23	22	fveq2d	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to F (X \cdot_{R} I (X)) = F (1_{R})$
24	1 2 19	abvmul	$⊢ (F \in A \land X \in B \land I (X) \in B) \to F (X \cdot_{R} I (X)) = F (X) F (I (X))$
25	5 6 13 24	syl3anc	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to F (X \cdot_{R} I (X)) = F (X) F (I (X))$
26	1 20	abv1	$⊢ (R \in DivRing \land F \in A) \to F (1_{R}) = 1$
27	26	adantr	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to F (1_{R}) = 1$
28	23 25 27	3eqtr3d	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to F (X) F (I (X)) = 1$
29	9 16 18 28	mvllmuld	$⊢ ((R \in DivRing \land F \in A) \land (X \in B \land X \neq \underset{˙}{0})) \to F (I (X)) = \frac{1}{F (X)}$

Metamath Proof Explorer

Theorem abvrec

Proof