nmdvr

Description: The norm of a division in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	nmdvr.x	$⊢ X = {Base}_{R}$
	nmdvr.n	$⊢ N = norm (R)$
	nmdvr.u	$⊢ U = Unit (R)$
	nmdvr.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
Assertion	nmdvr	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to N (A \underset{˙}{\times} B) = \frac{N (A)}{N (B)}$

Proof

Step	Hyp	Ref	Expression
1		nmdvr.x	$⊢ X = {Base}_{R}$
2		nmdvr.n	$⊢ N = norm (R)$
3		nmdvr.u	$⊢ U = Unit (R)$
4		nmdvr.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
5		simpll	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to R \in NrmRing$
6		simprl	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to A \in X$
7		nrgring	$⊢ R \in NrmRing \to R \in Ring$
8	7	ad2antrr	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to R \in Ring$
9		simprr	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to B \in U$
10		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
11	3 10 1	ringinvcl	$⊢ (R \in Ring \land B \in U) \to {inv}_{r} (R) (B) \in X$
12	8 9 11	syl2anc	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to {inv}_{r} (R) (B) \in X$
13		eqid	$⊢ \cdot_{R} = \cdot_{R}$
14	1 2 13	nmmul	$⊢ (R \in NrmRing \land A \in X \land {inv}_{r} (R) (B) \in X) \to N (A \cdot_{R} {inv}_{r} (R) (B)) = N (A) N ({inv}_{r} (R) (B))$
15	5 6 12 14	syl3anc	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to N (A \cdot_{R} {inv}_{r} (R) (B)) = N (A) N ({inv}_{r} (R) (B))$
16		simplr	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to R \in NzRing$
17	2 3 10	nminvr	$⊢ (R \in NrmRing \land R \in NzRing \land B \in U) \to N ({inv}_{r} (R) (B)) = \frac{1}{N (B)}$
18	5 16 9 17	syl3anc	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to N ({inv}_{r} (R) (B)) = \frac{1}{N (B)}$
19	18	oveq2d	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to N (A) N ({inv}_{r} (R) (B)) = N (A) (\frac{1}{N (B)})$
20	15 19	eqtrd	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to N (A \cdot_{R} {inv}_{r} (R) (B)) = N (A) (\frac{1}{N (B)})$
21	1 13 3 10 4	dvrval	$⊢ (A \in X \land B \in U) \to A \underset{˙}{\times} B = A \cdot_{R} {inv}_{r} (R) (B)$
22	21	adantl	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to A \underset{˙}{\times} B = A \cdot_{R} {inv}_{r} (R) (B)$
23	22	fveq2d	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to N (A \underset{˙}{\times} B) = N (A \cdot_{R} {inv}_{r} (R) (B))$
24		nrgngp	$⊢ R \in NrmRing \to R \in NrmGrp$
25	24	ad2antrr	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to R \in NrmGrp$
26	1 2	nmcl	$⊢ (R \in NrmGrp \land A \in X) \to N (A) \in ℝ$
27	25 6 26	syl2anc	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to N (A) \in ℝ$
28	27	recnd	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to N (A) \in ℂ$
29	1 3	unitss	$⊢ U \subseteq X$
30	29 9	sseldi	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to B \in X$
31	1 2	nmcl	$⊢ (R \in NrmGrp \land B \in X) \to N (B) \in ℝ$
32	25 30 31	syl2anc	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to N (B) \in ℝ$
33	32	recnd	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to N (B) \in ℂ$
34	2 3	unitnmn0	$⊢ (R \in NrmRing \land R \in NzRing \land B \in U) \to N (B) \neq 0$
35	34	3expa	$⊢ ((R \in NrmRing \land R \in NzRing) \land B \in U) \to N (B) \neq 0$
36	35	adantrl	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to N (B) \neq 0$
37	28 33 36	divrecd	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to \frac{N (A)}{N (B)} = N (A) (\frac{1}{N (B)})$
38	20 23 37	3eqtr4d	$⊢ ((R \in NrmRing \land R \in NzRing) \land (A \in X \land B \in U)) \to N (A \underset{˙}{\times} B) = \frac{N (A)}{N (B)}$

Metamath Proof Explorer

Theorem nmdvr

Proof