Theorem 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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	nmmulg.n	⊢ 𝑁 = ( norm ‘ 𝑅 )
	nmmulg.z	⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
	zrhnm.1	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
Assertion	zrhnm	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ‘ ( 𝐿 ‘ 𝑀 ) ) = ( abs ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		nmmulg.x	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		nmmulg.n	⊢ 𝑁 = ( norm ‘ 𝑅 )
3		nmmulg.z	⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
4		zrhnm.1	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
5		simpl3	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → 𝑅 ∈ NzRing )
6		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
7	5 6	syl	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → 𝑅 ∈ Ring )
8		simpr	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
9		eqid	⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
10		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
11	4 9 10	zrhmulg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ) → ( 𝐿 ‘ 𝑀 ) = ( 𝑀 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
12	11	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ‘ ( 𝐿 ‘ 𝑀 ) ) = ( 𝑁 ‘ ( 𝑀 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
13	7 8 12	syl2anc	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ‘ ( 𝐿 ‘ 𝑀 ) ) = ( 𝑁 ‘ ( 𝑀 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
14		simpl1	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → 𝑍 ∈ NrmMod )
15	1 10	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
16	7 15	syl	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
17	1 2 3 9	nmmulg	⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑀 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( ( abs ‘ 𝑀 ) · ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) )
18	14 8 16 17	syl3anc	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ‘ ( 𝑀 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( ( abs ‘ 𝑀 ) · ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) )
19	3 2	zlmnm	⊢ ( 𝑅 ∈ NzRing → 𝑁 = ( norm ‘ 𝑍 ) )
20	5 19	syl	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → 𝑁 = ( norm ‘ 𝑍 ) )
21	20	fveq1d	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) = ( ( norm ‘ 𝑍 ) ‘ ( 1r ‘ 𝑅 ) ) )
22		simpl2	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → 𝑍 ∈ NrmRing )
23		nrgring	⊢ ( 𝑍 ∈ NrmRing → 𝑍 ∈ Ring )
24	22 23	syl	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → 𝑍 ∈ Ring )
25		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
26	10 25	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
27	5 26	syl	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
28	3 10	zlm1	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑍 )
29	3 25	zlm0	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑍 )
30	28 29	isnzr	⊢ ( 𝑍 ∈ NzRing ↔ ( 𝑍 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
31	24 27 30	sylanbrc	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → 𝑍 ∈ NzRing )
32		eqid	⊢ ( norm ‘ 𝑍 ) = ( norm ‘ 𝑍 )
33	32 28	nm1	⊢ ( ( 𝑍 ∈ NrmRing ∧ 𝑍 ∈ NzRing ) → ( ( norm ‘ 𝑍 ) ‘ ( 1r ‘ 𝑅 ) ) = 1 )
34	22 31 33	syl2anc	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( ( norm ‘ 𝑍 ) ‘ ( 1r ‘ 𝑅 ) ) = 1 )
35	21 34	eqtrd	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) = 1 )
36	35	oveq2d	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) · ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = ( ( abs ‘ 𝑀 ) · 1 ) )
37	13 18 36	3eqtrd	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ‘ ( 𝐿 ‘ 𝑀 ) ) = ( ( abs ‘ 𝑀 ) · 1 ) )
38	8	zcnd	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℂ )
39		abscl	⊢ ( 𝑀 ∈ ℂ → ( abs ‘ 𝑀 ) ∈ ℝ )
40	39	recnd	⊢ ( 𝑀 ∈ ℂ → ( abs ‘ 𝑀 ) ∈ ℂ )
41		mulrid	⊢ ( ( abs ‘ 𝑀 ) ∈ ℂ → ( ( abs ‘ 𝑀 ) · 1 ) = ( abs ‘ 𝑀 ) )
42	38 40 41	3syl	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) · 1 ) = ( abs ‘ 𝑀 ) )
43	37 42	eqtrd	⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ‘ ( 𝐿 ‘ 𝑀 ) ) = ( abs ‘ 𝑀 ) )