# Metamath Proof Explorer

## Theorem rezh

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

Ref Expression
Assertion rezh ${⊢}\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{NrmMod}$

### Proof

Step Hyp Ref Expression
1 cnnrg ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{NrmRing}$
2 resubdrg ${⊢}\left(ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\right)$
3 2 simpli ${⊢}ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$
4 df-refld ${⊢}{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}ℝ$
5 4 subrgnrg ${⊢}\left({ℂ}_{\mathrm{fld}}\in \mathrm{NrmRing}\wedge ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {ℝ}_{\mathrm{fld}}\in \mathrm{NrmRing}$
6 1 3 5 mp2an ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{NrmRing}$
7 eqid ${⊢}\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)$
8 7 zhmnrg ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{NrmRing}\to \mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{NrmRing}$
9 nrgngp ${⊢}\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{NrmRing}\to \mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{NrmGrp}$
10 6 8 9 mp2b ${⊢}\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{NrmGrp}$
11 nrgring ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{NrmRing}\to {ℝ}_{\mathrm{fld}}\in \mathrm{Ring}$
12 ringabl ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℝ}_{\mathrm{fld}}\in \mathrm{Abel}$
13 6 11 12 mp2b ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{Abel}$
14 7 zlmlmod ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{Abel}↔\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{LMod}$
15 13 14 mpbi ${⊢}\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{LMod}$
16 zringnrg ${⊢}{ℤ}_{\mathrm{ring}}\in \mathrm{NrmRing}$
17 10 15 16 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)$
18 simpl ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to {z}\in ℤ$
19 18 zcnd ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to {z}\in ℂ$
20 simpr ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to {x}\in ℝ$
21 20 recnd ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to {x}\in ℂ$
22 19 21 absmuld ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to \left|{z}{x}\right|=\left|{z}\right|\left|{x}\right|$
23 subrgsubg ${⊢}ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to ℝ\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$
24 3 23 ax-mp ${⊢}ℝ\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$
25 eqid ${⊢}{\cdot }_{{ℂ}_{\mathrm{fld}}}={\cdot }_{{ℂ}_{\mathrm{fld}}}$
26 eqid ${⊢}{\cdot }_{{ℝ}_{\mathrm{fld}}}={\cdot }_{{ℝ}_{\mathrm{fld}}}$
27 7 26 zlmvsca ${⊢}{\cdot }_{{ℝ}_{\mathrm{fld}}}={\cdot }_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}$
28 27 eqcomi ${⊢}{\cdot }_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}={\cdot }_{{ℝ}_{\mathrm{fld}}}$
29 25 4 28 subgmulg ${⊢}\left(ℝ\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge {z}\in ℤ\wedge {x}\in ℝ\right)\to {z}{\cdot }_{{ℂ}_{\mathrm{fld}}}{x}={z}{\cdot }_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}{x}$
30 24 29 mp3an1 ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to {z}{\cdot }_{{ℂ}_{\mathrm{fld}}}{x}={z}{\cdot }_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}{x}$
31 cnfldmulg ${⊢}\left({z}\in ℤ\wedge {x}\in ℂ\right)\to {z}{\cdot }_{{ℂ}_{\mathrm{fld}}}{x}={z}{x}$
32 21 31 syldan ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to {z}{\cdot }_{{ℂ}_{\mathrm{fld}}}{x}={z}{x}$
33 30 32 eqtr3d ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to {z}{\cdot }_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}{x}={z}{x}$
34 33 fveq2d ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to \left({\mathrm{abs}↾}_{ℝ}\right)\left({z}{\cdot }_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}{x}\right)=\left({\mathrm{abs}↾}_{ℝ}\right)\left({z}{x}\right)$
35 zre ${⊢}{z}\in ℤ\to {z}\in ℝ$
36 remulcl ${⊢}\left({z}\in ℝ\wedge {x}\in ℝ\right)\to {z}{x}\in ℝ$
37 fvres ${⊢}{z}{x}\in ℝ\to \left({\mathrm{abs}↾}_{ℝ}\right)\left({z}{x}\right)=\left|{z}{x}\right|$
38 36 37 syl ${⊢}\left({z}\in ℝ\wedge {x}\in ℝ\right)\to \left({\mathrm{abs}↾}_{ℝ}\right)\left({z}{x}\right)=\left|{z}{x}\right|$
39 35 38 sylan ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to \left({\mathrm{abs}↾}_{ℝ}\right)\left({z}{x}\right)=\left|{z}{x}\right|$
40 34 39 eqtrd ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to \left({\mathrm{abs}↾}_{ℝ}\right)\left({z}{\cdot }_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}{x}\right)=\left|{z}{x}\right|$
41 fvres ${⊢}{z}\in ℤ\to \left({\mathrm{abs}↾}_{ℤ}\right)\left({z}\right)=\left|{z}\right|$
42 fvres ${⊢}{x}\in ℝ\to \left({\mathrm{abs}↾}_{ℝ}\right)\left({x}\right)=\left|{x}\right|$
43 41 42 oveqan12d ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to \left({\mathrm{abs}↾}_{ℤ}\right)\left({z}\right)\left({\mathrm{abs}↾}_{ℝ}\right)\left({x}\right)=\left|{z}\right|\left|{x}\right|$
44 22 40 43 3eqtr4d ${⊢}\left({z}\in ℤ\wedge {x}\in ℝ\right)\to \left({\mathrm{abs}↾}_{ℝ}\right)\left({z}{\cdot }_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}{x}\right)=\left({\mathrm{abs}↾}_{ℤ}\right)\left({z}\right)\left({\mathrm{abs}↾}_{ℝ}\right)\left({x}\right)$
45 44 rgen2 ${⊢}\forall {z}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({\mathrm{abs}↾}_{ℝ}\right)\left({z}{\cdot }_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}{x}\right)=\left({\mathrm{abs}↾}_{ℤ}\right)\left({z}\right)\left({\mathrm{abs}↾}_{ℝ}\right)\left({x}\right)$
46 rebase ${⊢}ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$
47 7 46 zlmbas ${⊢}ℝ={\mathrm{Base}}_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}$
48 recusp ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{CUnifSp}$
49 48 elexi ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{V}$
50 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
51 ringmnd ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$
52 50 51 ax-mp ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$
53 0re ${⊢}0\in ℝ$
54 ax-resscn ${⊢}ℝ\subseteq ℂ$
55 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
56 cnfld0 ${⊢}0={0}_{{ℂ}_{\mathrm{fld}}}$
57 cnfldnm ${⊢}\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$
58 4 55 56 57 ressnm ${⊢}\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge 0\in ℝ\wedge ℝ\subseteq ℂ\right)\to {\mathrm{abs}↾}_{ℝ}=\mathrm{norm}\left({ℝ}_{\mathrm{fld}}\right)$
59 52 53 54 58 mp3an ${⊢}{\mathrm{abs}↾}_{ℝ}=\mathrm{norm}\left({ℝ}_{\mathrm{fld}}\right)$
60 7 59 zlmnm ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{V}\to {\mathrm{abs}↾}_{ℝ}=\mathrm{norm}\left(\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)\right)$
61 49 60 ax-mp ${⊢}{\mathrm{abs}↾}_{ℝ}=\mathrm{norm}\left(\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)\right)$
62 eqid ${⊢}{\cdot }_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}={\cdot }_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}$
63 7 zlmsca ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{V}\to {ℤ}_{\mathrm{ring}}=\mathrm{Scalar}\left(\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)\right)$
64 49 63 ax-mp ${⊢}{ℤ}_{\mathrm{ring}}=\mathrm{Scalar}\left(\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)\right)$
65 zringbas ${⊢}ℤ={\mathrm{Base}}_{{ℤ}_{\mathrm{ring}}}$
66 zringnm ${⊢}\mathrm{norm}\left({ℤ}_{\mathrm{ring}}\right)={\mathrm{abs}↾}_{ℤ}$
67 66 eqcomi ${⊢}{\mathrm{abs}↾}_{ℤ}=\mathrm{norm}\left({ℤ}_{\mathrm{ring}}\right)$
68 47 61 62 64 65 67 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({\mathrm{abs}↾}_{ℝ}\right)\left({z}{\cdot }_{\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)}{x}\right)=\left({\mathrm{abs}↾}_{ℤ}\right)\left({z}\right)\left({\mathrm{abs}↾}_{ℝ}\right)\left({x}\right)\right)$
69 17 45 68 mpbir2an ${⊢}\mathrm{ℤMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{NrmMod}$