qqhnm

Description: The norm of the image by QQHom of a rational number in a topological division ring. (Contributed by Thierry Arnoux, 8-Nov-2017)

	Ref	Expression
Hypotheses	qqhnm.n	$⊢ N = norm (R)$
	qqhnm.z	$⊢ Z = ℤMod (R)$
Assertion	qqhnm	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to N (ℚHom (R) (Q)) = \|Q\|$

Proof

Step	Hyp	Ref	Expression
1		qqhnm.n	$⊢ N = norm (R)$
2		qqhnm.z	$⊢ Z = ℤMod (R)$
3		simpr	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to Q \in ℚ$
4		qeqnumdivden	$⊢ Q \in ℚ \to Q = \frac{numer (Q)}{denom (Q)}$
5	4	fveq2d	$⊢ Q \in ℚ \to \|Q\| = \|\frac{numer (Q)}{denom (Q)}\|$
6	3 5	syl	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to \|Q\| = \|\frac{numer (Q)}{denom (Q)}\|$
7		qnumcl	$⊢ Q \in ℚ \to numer (Q) \in ℤ$
8	3 7	syl	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to numer (Q) \in ℤ$
9	8	zcnd	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to numer (Q) \in ℂ$
10		qdencl	$⊢ Q \in ℚ \to denom (Q) \in ℕ$
11	3 10	syl	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to denom (Q) \in ℕ$
12	11	nncnd	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to denom (Q) \in ℂ$
13		nnne0	$⊢ denom (Q) \in ℕ \to denom (Q) \neq 0$
14	3 10 13	3syl	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to denom (Q) \neq 0$
15	9 12 14	absdivd	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to \|\frac{numer (Q)}{denom (Q)}\| = \frac{\|numer (Q)\|}{\|denom (Q)\|}$
16		inss2	$⊢ NrmRing \cap DivRing \subseteq DivRing$
17		simpl1	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to R \in (NrmRing \cap DivRing)$
18	16 17	sselid	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to R \in DivRing$
19		simpl3	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to chr (R) = 0$
20		eqid	$⊢ {Base}_{R} = {Base}_{R}$
21		eqid	$⊢ /_{r} (R) = /_{r} (R)$
22		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
23	20 21 22	qqhvval	$⊢ ((R \in DivRing \land chr (R) = 0) \land Q \in ℚ) \to ℚHom (R) (Q) = ℤRHom (R) (numer (Q)) /_{r} (R) ℤRHom (R) (denom (Q))$
24	23	fveq2d	$⊢ ((R \in DivRing \land chr (R) = 0) \land Q \in ℚ) \to N (ℚHom (R) (Q)) = N (ℤRHom (R) (numer (Q)) /_{r} (R) ℤRHom (R) (denom (Q)))$
25	18 19 3 24	syl21anc	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to N (ℚHom (R) (Q)) = N (ℤRHom (R) (numer (Q)) /_{r} (R) ℤRHom (R) (denom (Q)))$
26		inss1	$⊢ NrmRing \cap DivRing \subseteq NrmRing$
27	26 17	sselid	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to R \in NrmRing$
28		drngnzr	$⊢ R \in DivRing \to R \in NzRing$
29	18 28	syl	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to R \in NzRing$
30		drngring	$⊢ R \in DivRing \to R \in Ring$
31	22	zrhrhm	$⊢ R \in Ring \to ℤRHom (R) \in (ℤ_{ring} RingHom R)$
32		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
33	32 20	rhmf	$⊢ ℤRHom (R) \in (ℤ_{ring} RingHom R) \to ℤRHom (R) : ℤ ⟶ {Base}_{R}$
34	18 30 31 33	4syl	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to ℤRHom (R) : ℤ ⟶ {Base}_{R}$
35	34 8	ffvelrnd	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to ℤRHom (R) (numer (Q)) \in {Base}_{R}$
36	11	nnzd	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to denom (Q) \in ℤ$
37		eqid	$⊢ 0_{R} = 0_{R}$
38	20 22 37	elzrhunit	$⊢ ((R \in DivRing \land chr (R) = 0) \land (denom (Q) \in ℤ \land denom (Q) \neq 0)) \to ℤRHom (R) (denom (Q)) \in Unit (R)$
39	18 19 36 14 38	syl22anc	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to ℤRHom (R) (denom (Q)) \in Unit (R)$
40		eqid	$⊢ Unit (R) = Unit (R)$
41	20 1 40 21	nmdvr	$⊢ ((R \in NrmRing \land R \in NzRing) \land (ℤRHom (R) (numer (Q)) \in {Base}_{R} \land ℤRHom (R) (denom (Q)) \in Unit (R))) \to N (ℤRHom (R) (numer (Q)) /_{r} (R) ℤRHom (R) (denom (Q))) = \frac{N (ℤRHom (R) (numer (Q)))}{N (ℤRHom (R) (denom (Q)))}$
42	27 29 35 39 41	syl22anc	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to N (ℤRHom (R) (numer (Q)) /_{r} (R) ℤRHom (R) (denom (Q))) = \frac{N (ℤRHom (R) (numer (Q)))}{N (ℤRHom (R) (denom (Q)))}$
43		simpl2	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to Z \in NrmMod$
44	2	zhmnrg	$⊢ R \in NrmRing \to Z \in NrmRing$
45	27 44	syl	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to Z \in NrmRing$
46	20 1 2 22	zrhnm	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land numer (Q) \in ℤ) \to N (ℤRHom (R) (numer (Q))) = \|numer (Q)\|$
47	43 45 29 8 46	syl31anc	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to N (ℤRHom (R) (numer (Q))) = \|numer (Q)\|$
48	20 1 2 22	zrhnm	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land denom (Q) \in ℤ) \to N (ℤRHom (R) (denom (Q))) = \|denom (Q)\|$
49	43 45 29 36 48	syl31anc	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to N (ℤRHom (R) (denom (Q))) = \|denom (Q)\|$
50	47 49	oveq12d	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to \frac{N (ℤRHom (R) (numer (Q)))}{N (ℤRHom (R) (denom (Q)))} = \frac{\|numer (Q)\|}{\|denom (Q)\|}$
51	25 42 50	3eqtrrd	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to \frac{\|numer (Q)\|}{\|denom (Q)\|} = N (ℚHom (R) (Q))$
52	6 15 51	3eqtrrd	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land Q \in ℚ) \to N (ℚHom (R) (Q)) = \|Q\|$

Metamath Proof Explorer

Theorem qqhnm

Proof