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 )