Metamath Proof Explorer

Theorem cnzh

Description: The ZZ -module of CC is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018)

Ref Expression
Assertion cnzh ⊢ℤMod⁡ℂfld∈NrmMod

Proof

Step Hyp Ref Expression
1 cnnrg ⊢ℂfld∈NrmRing
2 eqid ⊢ℤMod⁡ℂfld=ℤMod⁡ℂfld
3 2 zhmnrg ⊢ℂfld∈NrmRing→ℤMod⁡ℂfld∈NrmRing
4 nrgngp ⊢ℤMod⁡ℂfld∈NrmRing→ℤMod⁡ℂfld∈NrmGrp
5 1 3 4 mp2b ⊢ℤMod⁡ℂfld∈NrmGrp
6 nrgring ⊢ℂfld∈NrmRing→ℂfld∈Ring
7 ringabl ⊢ℂfld∈Ring→ℂfld∈Abel
8 1 6 7 mp2b ⊢ℂfld∈Abel
9 2 zlmlmod ⊢ℂfld∈Abel↔ℤMod⁡ℂfld∈LMod
10 8 9 mpbi ⊢ℤMod⁡ℂfld∈LMod
11 zringnrg ⊢ℤring∈NrmRing
12 5 10 11 3pm3.2i ⊢ℤMod⁡ℂfld∈NrmGrp∧ℤMod⁡ℂfld∈LMod∧ℤring∈NrmRing
13 simpl ⊢z∈ℤ∧x∈ℂ→z∈ℤ
14 13 zcnd ⊢z∈ℤ∧x∈ℂ→z∈ℂ
15 simpr ⊢z∈ℤ∧x∈ℂ→x∈ℂ
16 14 15 absmuld ⊢z∈ℤ∧x∈ℂ→z⁢x=z⁢x
17 cnfldmulg ⊢z∈ℤ∧x∈ℂ→z⋅ℂfldx=z⁢x
18 17 fveq2d ⊢z∈ℤ∧x∈ℂ→z⋅ℂfldx=z⁢x
19 fvres ⊢z∈ℤ→abs↾ℤ⁡z=z
20 19 adantr ⊢z∈ℤ∧x∈ℂ→abs↾ℤ⁡z=z
21 20 oveq1d ⊢z∈ℤ∧x∈ℂ→abs↾ℤ⁡z⁢x=z⁢x
22 16 18 21 3eqtr4d ⊢z∈ℤ∧x∈ℂ→z⋅ℂfldx=abs↾ℤ⁡z⁢x
23 22 rgen2 ⊢∀z∈ℤ∀x∈ℂz⋅ℂfldx=abs↾ℤ⁡z⁢x
24 cnfldbas ⊢ℂ=Baseℂfld
25 2 24 zlmbas ⊢ℂ=BaseℤMod⁡ℂfld
26 cnfldex ⊢ℂfld∈V
27 cnfldnm ⊢abs=norm⁡ℂfld
28 2 27 zlmnm ⊢ℂfld∈V→abs=norm⁡ℤMod⁡ℂfld
29 26 28 ax-mp ⊢abs=norm⁡ℤMod⁡ℂfld
30 eqid ⊢⋅ℂfld=⋅ℂfld
31 2 30 zlmvsca ⊢⋅ℂfld=⋅ℤMod⁡ℂfld
32 2 zlmsca ⊢ℂfld∈V→ℤring=Scalar⁡ℤMod⁡ℂfld
33 26 32 ax-mp ⊢ℤring=Scalar⁡ℤMod⁡ℂfld
34 zringbas ⊢ℤ=Baseℤring
35 zringnm ⊢norm⁡ℤring=abs↾ℤ
36 35 eqcomi ⊢abs↾ℤ=norm⁡ℤring
37 25 29 31 33 34 36 isnlm ⊢ℤMod⁡ℂfld∈NrmMod↔ℤMod⁡ℂfld∈NrmGrp∧ℤMod⁡ℂfld∈LMod∧ℤring∈NrmRing∧∀z∈ℤ∀x∈ℂz⋅ℂfldx=abs↾ℤ⁡z⁢x
38 12 23 37 mpbir2an ⊢ℤMod⁡ℂfld∈NrmMod