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=ℤModG
Assertion zhmnrg GNrmRingWNrmRing

Proof

Step Hyp Ref Expression
1 zlmlem2.1 W=ℤModG
2 eqid BaseG=BaseG
3 2 a1i GNrmRingBaseG=BaseG
4 1 2 zlmbas BaseG=BaseW
5 4 a1i GNrmRingBaseG=BaseW
6 eqid +G=+G
7 1 6 zlmplusg +G=+W
8 7 a1i GNrmRing+G=+W
9 8 oveqdr GNrmRingxBaseGyBaseGx+Gy=x+Wy
10 3 5 9 grppropd GNrmRingGGrpWGrp
11 eqid distG=distG
12 1 11 zlmds GNrmRingdistG=distW
13 12 reseq1d GNrmRingdistGBaseG×BaseG=distWBaseG×BaseG
14 eqid TopSetG=TopSetG
15 1 14 zlmtset GNrmRingTopSetG=TopSetW
16 5 15 topnpropd GNrmRingTopOpenG=TopOpenW
17 3 5 13 16 mspropd GNrmRingGMetSpWMetSp
18 eqid normG=normG
19 1 18 zlmnm GNrmRingnormG=normW
20 5 8 grpsubpropd GNrmRing-G=-W
21 19 20 coeq12d GNrmRingnormG-G=normW-W
22 21 12 sseq12d GNrmRingnormG-GdistGnormW-WdistW
23 10 17 22 3anbi123d GNrmRingGGrpGMetSpnormG-GdistGWGrpWMetSpnormW-WdistW
24 eqid -G=-G
25 18 24 11 isngp GNrmGrpGGrpGMetSpnormG-GdistG
26 eqid normW=normW
27 eqid -W=-W
28 eqid distW=distW
29 26 27 28 isngp WNrmGrpWGrpWMetSpnormW-WdistW
30 23 25 29 3bitr4g GNrmRingGNrmGrpWNrmGrp
31 eqid G=G
32 1 31 zlmmulr G=W
33 32 a1i GNrmRingG=W
34 5 8 33 abvpropd2 GNrmRingAbsValG=AbsValW
35 19 34 eleq12d GNrmRingnormGAbsValGnormWAbsValW
36 30 35 anbi12d GNrmRingGNrmGrpnormGAbsValGWNrmGrpnormWAbsValW
37 eqid AbsValG=AbsValG
38 18 37 isnrg GNrmRingGNrmGrpnormGAbsValG
39 eqid AbsValW=AbsValW
40 26 39 isnrg WNrmRingWNrmGrpnormWAbsValW
41 36 38 40 3bitr4g GNrmRingGNrmRingWNrmRing
42 41 ibi GNrmRingWNrmRing