# 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 ${⊢}\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{NrmMod}$

### Proof

Step Hyp Ref Expression
1 cnnrg ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{NrmRing}$
2 eqid ${⊢}\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)$
3 2 zhmnrg ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{NrmRing}\to \mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{NrmRing}$
4 nrgngp ${⊢}\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{NrmRing}\to \mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{NrmGrp}$
5 1 3 4 mp2b ${⊢}\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{NrmGrp}$
6 nrgring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{NrmRing}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
7 ringabl ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Abel}$
8 1 6 7 mp2b ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Abel}$
9 2 zlmlmod ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Abel}↔\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{LMod}$
10 8 9 mpbi ${⊢}\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{LMod}$
11 zringnrg ${⊢}{ℤ}_{\mathrm{ring}}\in \mathrm{NrmRing}$
12 5 10 11 3pm3.2i ${⊢}\left(\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{NrmGrp}\wedge \mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{LMod}\wedge {ℤ}_{\mathrm{ring}}\in \mathrm{NrmRing}\right)$
13 simpl ${⊢}\left({z}\in ℤ\wedge {x}\in ℂ\right)\to {z}\in ℤ$
14 13 zcnd ${⊢}\left({z}\in ℤ\wedge {x}\in ℂ\right)\to {z}\in ℂ$
15 simpr ${⊢}\left({z}\in ℤ\wedge {x}\in ℂ\right)\to {x}\in ℂ$
16 14 15 absmuld ${⊢}\left({z}\in ℤ\wedge {x}\in ℂ\right)\to \left|{z}{x}\right|=\left|{z}\right|\left|{x}\right|$
17 cnfldmulg ${⊢}\left({z}\in ℤ\wedge {x}\in ℂ\right)\to {z}{\cdot }_{{ℂ}_{\mathrm{fld}}}{x}={z}{x}$
18 17 fveq2d ${⊢}\left({z}\in ℤ\wedge {x}\in ℂ\right)\to \left|{z}{\cdot }_{{ℂ}_{\mathrm{fld}}}{x}\right|=\left|{z}{x}\right|$
19 fvres ${⊢}{z}\in ℤ\to \left({\mathrm{abs}↾}_{ℤ}\right)\left({z}\right)=\left|{z}\right|$
20 19 adantr ${⊢}\left({z}\in ℤ\wedge {x}\in ℂ\right)\to \left({\mathrm{abs}↾}_{ℤ}\right)\left({z}\right)=\left|{z}\right|$
21 20 oveq1d ${⊢}\left({z}\in ℤ\wedge {x}\in ℂ\right)\to \left({\mathrm{abs}↾}_{ℤ}\right)\left({z}\right)\left|{x}\right|=\left|{z}\right|\left|{x}\right|$
22 16 18 21 3eqtr4d ${⊢}\left({z}\in ℤ\wedge {x}\in ℂ\right)\to \left|{z}{\cdot }_{{ℂ}_{\mathrm{fld}}}{x}\right|=\left({\mathrm{abs}↾}_{ℤ}\right)\left({z}\right)\left|{x}\right|$
23 22 rgen2 ${⊢}\forall {z}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left|{z}{\cdot }_{{ℂ}_{\mathrm{fld}}}{x}\right|=\left({\mathrm{abs}↾}_{ℤ}\right)\left({z}\right)\left|{x}\right|$
24 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
25 2 24 zlmbas ${⊢}ℂ={\mathrm{Base}}_{\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)}$
26 cnfldex ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{V}$
27 cnfldnm ${⊢}\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$
28 2 27 zlmnm ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{V}\to \mathrm{abs}=\mathrm{norm}\left(\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\right)$
29 26 28 ax-mp ${⊢}\mathrm{abs}=\mathrm{norm}\left(\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\right)$
30 eqid ${⊢}{\cdot }_{{ℂ}_{\mathrm{fld}}}={\cdot }_{{ℂ}_{\mathrm{fld}}}$
31 2 30 zlmvsca ${⊢}{\cdot }_{{ℂ}_{\mathrm{fld}}}={\cdot }_{\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)}$
32 2 zlmsca ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{V}\to {ℤ}_{\mathrm{ring}}=\mathrm{Scalar}\left(\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\right)$
33 26 32 ax-mp ${⊢}{ℤ}_{\mathrm{ring}}=\mathrm{Scalar}\left(\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\right)$
34 zringbas ${⊢}ℤ={\mathrm{Base}}_{{ℤ}_{\mathrm{ring}}}$
35 zringnm ${⊢}\mathrm{norm}\left({ℤ}_{\mathrm{ring}}\right)={\mathrm{abs}↾}_{ℤ}$
36 35 eqcomi ${⊢}{\mathrm{abs}↾}_{ℤ}=\mathrm{norm}\left({ℤ}_{\mathrm{ring}}\right)$
37 25 29 31 33 34 36 isnlm ${⊢}\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{NrmMod}↔\left(\left(\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{NrmGrp}\wedge \mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{LMod}\wedge {ℤ}_{\mathrm{ring}}\in \mathrm{NrmRing}\right)\wedge \forall {z}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left|{z}{\cdot }_{{ℂ}_{\mathrm{fld}}}{x}\right|=\left({\mathrm{abs}↾}_{ℤ}\right)\left({z}\right)\left|{x}\right|\right)$
38 12 23 37 mpbir2an ${⊢}\mathrm{ℤMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{NrmMod}$