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 = ℤMod ⁡ G
Assertion zhmnrg ⊢ G ∈ NrmRing → W ∈ NrmRing

Proof

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