zrhnm

Description: The norm of the image by ZRHom of an integer in a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017)

	Ref	Expression
Hypotheses	nmmulg.x	$⊢ B = {Base}_{R}$
	nmmulg.n	$⊢ N = norm (R)$
	nmmulg.z	$⊢ Z = ℤMod (R)$
	zrhnm.1	$⊢ L = ℤRHom (R)$
Assertion	zrhnm	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to N (L (M)) = \|M\|$

Proof

Step	Hyp	Ref	Expression
1		nmmulg.x	$⊢ B = {Base}_{R}$
2		nmmulg.n	$⊢ N = norm (R)$
3		nmmulg.z	$⊢ Z = ℤMod (R)$
4		zrhnm.1	$⊢ L = ℤRHom (R)$
5		simpl3	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to R \in NzRing$
6		nzrring	$⊢ R \in NzRing \to R \in Ring$
7	5 6	syl	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to R \in Ring$
8		simpr	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to M \in ℤ$
9		eqid	$⊢ \cdot_{R} = \cdot_{R}$
10		eqid	$⊢ 1_{R} = 1_{R}$
11	4 9 10	zrhmulg	$⊢ (R \in Ring \land M \in ℤ) \to L (M) = M \cdot_{R} 1_{R}$
12	11	fveq2d	$⊢ (R \in Ring \land M \in ℤ) \to N (L (M)) = N (M \cdot_{R} 1_{R})$
13	7 8 12	syl2anc	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to N (L (M)) = N (M \cdot_{R} 1_{R})$
14		simpl1	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to Z \in NrmMod$
15	1 10	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
16	7 15	syl	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to 1_{R} \in B$
17	1 2 3 9	nmmulg	$⊢ (Z \in NrmMod \land M \in ℤ \land 1_{R} \in B) \to N (M \cdot_{R} 1_{R}) = \|M\| N (1_{R})$
18	14 8 16 17	syl3anc	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to N (M \cdot_{R} 1_{R}) = \|M\| N (1_{R})$
19	3 2	zlmnm	$⊢ R \in NzRing \to N = norm (Z)$
20	5 19	syl	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to N = norm (Z)$
21	20	fveq1d	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to N (1_{R}) = norm (Z) (1_{R})$
22		simpl2	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to Z \in NrmRing$
23		nrgring	$⊢ Z \in NrmRing \to Z \in Ring$
24	22 23	syl	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to Z \in Ring$
25		eqid	$⊢ 0_{R} = 0_{R}$
26	10 25	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
27	5 26	syl	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to 1_{R} \neq 0_{R}$
28	3 10	zlm1	$⊢ 1_{R} = 1_{Z}$
29	3 25	zlm0	$⊢ 0_{R} = 0_{Z}$
30	28 29	isnzr	$⊢ Z \in NzRing \leftrightarrow (Z \in Ring \land 1_{R} \neq 0_{R})$
31	24 27 30	sylanbrc	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to Z \in NzRing$
32		eqid	$⊢ norm (Z) = norm (Z)$
33	32 28	nm1	$⊢ (Z \in NrmRing \land Z \in NzRing) \to norm (Z) (1_{R}) = 1$
34	22 31 33	syl2anc	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to norm (Z) (1_{R}) = 1$
35	21 34	eqtrd	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to N (1_{R}) = 1$
36	35	oveq2d	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to \|M\| N (1_{R}) = \|M\| \cdot 1$
37	13 18 36	3eqtrd	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to N (L (M)) = \|M\| \cdot 1$
38	8	zcnd	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to M \in ℂ$
39		abscl	$⊢ M \in ℂ \to \|M\| \in ℝ$
40	39	recnd	$⊢ M \in ℂ \to \|M\| \in ℂ$
41		mulrid	$⊢ \|M\| \in ℂ \to \|M\| \cdot 1 = \|M\|$
42	38 40 41	3syl	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to \|M\| \cdot 1 = \|M\|$
43	37 42	eqtrd	$⊢ ((Z \in NrmMod \land Z \in NrmRing \land R \in NzRing) \land M \in ℤ) \to N (L (M)) = \|M\|$

Metamath Proof Explorer

Theorem zrhnm

Proof