# 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 = ( ZMod ` G )`
Assertion zhmnrg
`|- ( G e. NrmRing -> W e. NrmRing )`

### Proof

Step Hyp Ref Expression
1 zlmlem2.1
` |-  W = ( ZMod ` G )`
2 eqid
` |-  ( Base ` G ) = ( Base ` G )`
3 2 a1i
` |-  ( G e. NrmRing -> ( Base ` G ) = ( Base ` G ) )`
4 1 2 zlmbas
` |-  ( Base ` G ) = ( Base ` W )`
5 4 a1i
` |-  ( G e. NrmRing -> ( Base ` G ) = ( Base ` W ) )`
6 eqid
` |-  ( +g ` G ) = ( +g ` G )`
7 1 6 zlmplusg
` |-  ( +g ` G ) = ( +g ` W )`
8 7 a1i
` |-  ( G e. NrmRing -> ( +g ` G ) = ( +g ` W ) )`
9 8 oveqdr
` |-  ( ( G e. NrmRing /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` W ) y ) )`
10 3 5 9 grppropd
` |-  ( G e. NrmRing -> ( G e. Grp <-> W e. Grp ) )`
11 eqid
` |-  ( dist ` G ) = ( dist ` G )`
12 1 11 zlmds
` |-  ( G e. NrmRing -> ( dist ` G ) = ( dist ` W ) )`
13 12 reseq1d
` |-  ( G e. NrmRing -> ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) = ( ( dist ` W ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) )`
14 eqid
` |-  ( TopSet ` G ) = ( TopSet ` G )`
15 1 14 zlmtset
` |-  ( G e. NrmRing -> ( TopSet ` G ) = ( TopSet ` W ) )`
16 5 15 topnpropd
` |-  ( G e. NrmRing -> ( TopOpen ` G ) = ( TopOpen ` W ) )`
17 3 5 13 16 mspropd
` |-  ( G e. NrmRing -> ( G e. MetSp <-> W e. MetSp ) )`
18 eqid
` |-  ( norm ` G ) = ( norm ` G )`
19 1 18 zlmnm
` |-  ( G e. NrmRing -> ( norm ` G ) = ( norm ` W ) )`
20 5 8 grpsubpropd
` |-  ( G e. NrmRing -> ( -g ` G ) = ( -g ` W ) )`
21 19 20 coeq12d
` |-  ( G e. NrmRing -> ( ( norm ` G ) o. ( -g ` G ) ) = ( ( norm ` W ) o. ( -g ` W ) ) )`
22 21 12 sseq12d
` |-  ( G e. NrmRing -> ( ( ( norm ` G ) o. ( -g ` G ) ) C_ ( dist ` G ) <-> ( ( norm ` W ) o. ( -g ` W ) ) C_ ( dist ` W ) ) )`
23 10 17 22 3anbi123d
` |-  ( G e. NrmRing -> ( ( G e. Grp /\ G e. MetSp /\ ( ( norm ` G ) o. ( -g ` G ) ) C_ ( dist ` G ) ) <-> ( W e. Grp /\ W e. MetSp /\ ( ( norm ` W ) o. ( -g ` W ) ) C_ ( dist ` W ) ) ) )`
24 eqid
` |-  ( -g ` G ) = ( -g ` G )`
25 18 24 11 isngp
` |-  ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( ( norm ` G ) o. ( -g ` G ) ) C_ ( dist ` G ) ) )`
26 eqid
` |-  ( norm ` W ) = ( norm ` W )`
27 eqid
` |-  ( -g ` W ) = ( -g ` W )`
28 eqid
` |-  ( dist ` W ) = ( dist ` W )`
29 26 27 28 isngp
` |-  ( W e. NrmGrp <-> ( W e. Grp /\ W e. MetSp /\ ( ( norm ` W ) o. ( -g ` W ) ) C_ ( dist ` W ) ) )`
30 23 25 29 3bitr4g
` |-  ( G e. NrmRing -> ( G e. NrmGrp <-> W e. NrmGrp ) )`
31 eqid
` |-  ( .r ` G ) = ( .r ` G )`
32 1 31 zlmmulr
` |-  ( .r ` G ) = ( .r ` W )`
33 32 a1i
` |-  ( G e. NrmRing -> ( .r ` G ) = ( .r ` W ) )`
34 5 8 33 abvpropd2
` |-  ( G e. NrmRing -> ( AbsVal ` G ) = ( AbsVal ` W ) )`
35 19 34 eleq12d
` |-  ( G e. NrmRing -> ( ( norm ` G ) e. ( AbsVal ` G ) <-> ( norm ` W ) e. ( AbsVal ` W ) ) )`
36 30 35 anbi12d
` |-  ( G e. NrmRing -> ( ( G e. NrmGrp /\ ( norm ` G ) e. ( AbsVal ` G ) ) <-> ( W e. NrmGrp /\ ( norm ` W ) e. ( AbsVal ` W ) ) ) )`
37 eqid
` |-  ( AbsVal ` G ) = ( AbsVal ` G )`
38 18 37 isnrg
` |-  ( G e. NrmRing <-> ( G e. NrmGrp /\ ( norm ` G ) e. ( AbsVal ` G ) ) )`
39 eqid
` |-  ( AbsVal ` W ) = ( AbsVal ` W )`
40 26 39 isnrg
` |-  ( W e. NrmRing <-> ( W e. NrmGrp /\ ( norm ` W ) e. ( AbsVal ` W ) ) )`
41 36 38 40 3bitr4g
` |-  ( G e. NrmRing -> ( G e. NrmRing <-> W e. NrmRing ) )`
42 41 ibi
` |-  ( G e. NrmRing -> W e. NrmRing )`