Metamath Proof Explorer

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 mulid1 ⊢ ( ( abs ‘ 𝑀 ) ∈ ℂ → ( ( abs ‘ 𝑀 ) · 1 ) = ( abs ‘ 𝑀 ) )
42 38 40 41 3syl ⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) · 1 ) = ( abs ‘ 𝑀 ) )
43 37 42 eqtrd ⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ‘ ( 𝐿 ‘ 𝑀 ) ) = ( abs ‘ 𝑀 ) )