# Metamath Proof Explorer

## Theorem zhmnrg

Description: The ZZ -module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017)

Ref Expression
Hypothesis zlmlem2.1 ${⊢}{W}=\mathrm{ℤMod}\left({G}\right)$
Assertion zhmnrg ${⊢}{G}\in \mathrm{NrmRing}\to {W}\in \mathrm{NrmRing}$

### Proof

Step Hyp Ref Expression
1 zlmlem2.1 ${⊢}{W}=\mathrm{ℤMod}\left({G}\right)$
2 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
3 2 a1i ${⊢}{G}\in \mathrm{NrmRing}\to {\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
4 1 2 zlmbas ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{W}}$
5 4 a1i ${⊢}{G}\in \mathrm{NrmRing}\to {\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{W}}$
6 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
7 1 6 zlmplusg ${⊢}{+}_{{G}}={+}_{{W}}$
8 7 a1i ${⊢}{G}\in \mathrm{NrmRing}\to {+}_{{G}}={+}_{{W}}$
9 8 oveqdr ${⊢}\left({G}\in \mathrm{NrmRing}\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\right)\to {x}{+}_{{G}}{y}={x}{+}_{{W}}{y}$
10 3 5 9 grppropd ${⊢}{G}\in \mathrm{NrmRing}\to \left({G}\in \mathrm{Grp}↔{W}\in \mathrm{Grp}\right)$
11 eqid ${⊢}\mathrm{dist}\left({G}\right)=\mathrm{dist}\left({G}\right)$
12 1 11 zlmds ${⊢}{G}\in \mathrm{NrmRing}\to \mathrm{dist}\left({G}\right)=\mathrm{dist}\left({W}\right)$
13 12 reseq1d ${⊢}{G}\in \mathrm{NrmRing}\to {\mathrm{dist}\left({G}\right)↾}_{\left({\mathrm{Base}}_{{G}}×{\mathrm{Base}}_{{G}}\right)}={\mathrm{dist}\left({W}\right)↾}_{\left({\mathrm{Base}}_{{G}}×{\mathrm{Base}}_{{G}}\right)}$
14 eqid ${⊢}\mathrm{TopSet}\left({G}\right)=\mathrm{TopSet}\left({G}\right)$
15 1 14 zlmtset ${⊢}{G}\in \mathrm{NrmRing}\to \mathrm{TopSet}\left({G}\right)=\mathrm{TopSet}\left({W}\right)$
16 5 15 topnpropd ${⊢}{G}\in \mathrm{NrmRing}\to \mathrm{TopOpen}\left({G}\right)=\mathrm{TopOpen}\left({W}\right)$
17 3 5 13 16 mspropd ${⊢}{G}\in \mathrm{NrmRing}\to \left({G}\in \mathrm{MetSp}↔{W}\in \mathrm{MetSp}\right)$
18 eqid ${⊢}\mathrm{norm}\left({G}\right)=\mathrm{norm}\left({G}\right)$
19 1 18 zlmnm ${⊢}{G}\in \mathrm{NrmRing}\to \mathrm{norm}\left({G}\right)=\mathrm{norm}\left({W}\right)$
20 5 8 grpsubpropd ${⊢}{G}\in \mathrm{NrmRing}\to {-}_{{G}}={-}_{{W}}$
21 19 20 coeq12d ${⊢}{G}\in \mathrm{NrmRing}\to \mathrm{norm}\left({G}\right)\circ {-}_{{G}}=\mathrm{norm}\left({W}\right)\circ {-}_{{W}}$
22 21 12 sseq12d ${⊢}{G}\in \mathrm{NrmRing}\to \left(\mathrm{norm}\left({G}\right)\circ {-}_{{G}}\subseteq \mathrm{dist}\left({G}\right)↔\mathrm{norm}\left({W}\right)\circ {-}_{{W}}\subseteq \mathrm{dist}\left({W}\right)\right)$
23 10 17 22 3anbi123d ${⊢}{G}\in \mathrm{NrmRing}\to \left(\left({G}\in \mathrm{Grp}\wedge {G}\in \mathrm{MetSp}\wedge \mathrm{norm}\left({G}\right)\circ {-}_{{G}}\subseteq \mathrm{dist}\left({G}\right)\right)↔\left({W}\in \mathrm{Grp}\wedge {W}\in \mathrm{MetSp}\wedge \mathrm{norm}\left({W}\right)\circ {-}_{{W}}\subseteq \mathrm{dist}\left({W}\right)\right)\right)$
24 eqid ${⊢}{-}_{{G}}={-}_{{G}}$
25 18 24 11 isngp ${⊢}{G}\in \mathrm{NrmGrp}↔\left({G}\in \mathrm{Grp}\wedge {G}\in \mathrm{MetSp}\wedge \mathrm{norm}\left({G}\right)\circ {-}_{{G}}\subseteq \mathrm{dist}\left({G}\right)\right)$
26 eqid ${⊢}\mathrm{norm}\left({W}\right)=\mathrm{norm}\left({W}\right)$
27 eqid ${⊢}{-}_{{W}}={-}_{{W}}$
28 eqid ${⊢}\mathrm{dist}\left({W}\right)=\mathrm{dist}\left({W}\right)$
29 26 27 28 isngp ${⊢}{W}\in \mathrm{NrmGrp}↔\left({W}\in \mathrm{Grp}\wedge {W}\in \mathrm{MetSp}\wedge \mathrm{norm}\left({W}\right)\circ {-}_{{W}}\subseteq \mathrm{dist}\left({W}\right)\right)$
30 23 25 29 3bitr4g ${⊢}{G}\in \mathrm{NrmRing}\to \left({G}\in \mathrm{NrmGrp}↔{W}\in \mathrm{NrmGrp}\right)$
31 eqid ${⊢}{\cdot }_{{G}}={\cdot }_{{G}}$
32 1 31 zlmmulr ${⊢}{\cdot }_{{G}}={\cdot }_{{W}}$
33 32 a1i ${⊢}{G}\in \mathrm{NrmRing}\to {\cdot }_{{G}}={\cdot }_{{W}}$
34 5 8 33 abvpropd2 ${⊢}{G}\in \mathrm{NrmRing}\to \mathrm{AbsVal}\left({G}\right)=\mathrm{AbsVal}\left({W}\right)$
35 19 34 eleq12d ${⊢}{G}\in \mathrm{NrmRing}\to \left(\mathrm{norm}\left({G}\right)\in \mathrm{AbsVal}\left({G}\right)↔\mathrm{norm}\left({W}\right)\in \mathrm{AbsVal}\left({W}\right)\right)$
36 30 35 anbi12d ${⊢}{G}\in \mathrm{NrmRing}\to \left(\left({G}\in \mathrm{NrmGrp}\wedge \mathrm{norm}\left({G}\right)\in \mathrm{AbsVal}\left({G}\right)\right)↔\left({W}\in \mathrm{NrmGrp}\wedge \mathrm{norm}\left({W}\right)\in \mathrm{AbsVal}\left({W}\right)\right)\right)$
37 eqid ${⊢}\mathrm{AbsVal}\left({G}\right)=\mathrm{AbsVal}\left({G}\right)$
38 18 37 isnrg ${⊢}{G}\in \mathrm{NrmRing}↔\left({G}\in \mathrm{NrmGrp}\wedge \mathrm{norm}\left({G}\right)\in \mathrm{AbsVal}\left({G}\right)\right)$
39 eqid ${⊢}\mathrm{AbsVal}\left({W}\right)=\mathrm{AbsVal}\left({W}\right)$
40 26 39 isnrg ${⊢}{W}\in \mathrm{NrmRing}↔\left({W}\in \mathrm{NrmGrp}\wedge \mathrm{norm}\left({W}\right)\in \mathrm{AbsVal}\left({W}\right)\right)$
41 36 38 40 3bitr4g ${⊢}{G}\in \mathrm{NrmRing}\to \left({G}\in \mathrm{NrmRing}↔{W}\in \mathrm{NrmRing}\right)$
42 41 ibi ${⊢}{G}\in \mathrm{NrmRing}\to {W}\in \mathrm{NrmRing}$