# Metamath Proof Explorer

## Theorem rezh

Description: The ZZ -module of RR is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018)

Ref Expression
Assertion rezh
`|- ( ZMod ` RRfld ) e. NrmMod`

### Proof

Step Hyp Ref Expression
1 cnnrg
` |-  CCfld e. NrmRing`
2 resubdrg
` |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )`
3 2 simpli
` |-  RR e. ( SubRing ` CCfld )`
4 df-refld
` |-  RRfld = ( CCfld |`s RR )`
5 4 subrgnrg
` |-  ( ( CCfld e. NrmRing /\ RR e. ( SubRing ` CCfld ) ) -> RRfld e. NrmRing )`
6 1 3 5 mp2an
` |-  RRfld e. NrmRing`
7 eqid
` |-  ( ZMod ` RRfld ) = ( ZMod ` RRfld )`
8 7 zhmnrg
` |-  ( RRfld e. NrmRing -> ( ZMod ` RRfld ) e. NrmRing )`
9 nrgngp
` |-  ( ( ZMod ` RRfld ) e. NrmRing -> ( ZMod ` RRfld ) e. NrmGrp )`
10 6 8 9 mp2b
` |-  ( ZMod ` RRfld ) e. NrmGrp`
11 nrgring
` |-  ( RRfld e. NrmRing -> RRfld e. Ring )`
12 ringabl
` |-  ( RRfld e. Ring -> RRfld e. Abel )`
13 6 11 12 mp2b
` |-  RRfld e. Abel`
14 7 zlmlmod
` |-  ( RRfld e. Abel <-> ( ZMod ` RRfld ) e. LMod )`
15 13 14 mpbi
` |-  ( ZMod ` RRfld ) e. LMod`
16 zringnrg
` |-  ZZring e. NrmRing`
17 10 15 16 3pm3.2i
` |-  ( ( ZMod ` RRfld ) e. NrmGrp /\ ( ZMod ` RRfld ) e. LMod /\ ZZring e. NrmRing )`
18 simpl
` |-  ( ( z e. ZZ /\ x e. RR ) -> z e. ZZ )`
19 18 zcnd
` |-  ( ( z e. ZZ /\ x e. RR ) -> z e. CC )`
20 simpr
` |-  ( ( z e. ZZ /\ x e. RR ) -> x e. RR )`
21 20 recnd
` |-  ( ( z e. ZZ /\ x e. RR ) -> x e. CC )`
22 19 21 absmuld
` |-  ( ( z e. ZZ /\ x e. RR ) -> ( abs ` ( z x. x ) ) = ( ( abs ` z ) x. ( abs ` x ) ) )`
23 subrgsubg
` |-  ( RR e. ( SubRing ` CCfld ) -> RR e. ( SubGrp ` CCfld ) )`
24 3 23 ax-mp
` |-  RR e. ( SubGrp ` CCfld )`
25 eqid
` |-  ( .g ` CCfld ) = ( .g ` CCfld )`
26 eqid
` |-  ( .g ` RRfld ) = ( .g ` RRfld )`
27 7 26 zlmvsca
` |-  ( .g ` RRfld ) = ( .s ` ( ZMod ` RRfld ) )`
28 27 eqcomi
` |-  ( .s ` ( ZMod ` RRfld ) ) = ( .g ` RRfld )`
29 25 4 28 subgmulg
` |-  ( ( RR e. ( SubGrp ` CCfld ) /\ z e. ZZ /\ x e. RR ) -> ( z ( .g ` CCfld ) x ) = ( z ( .s ` ( ZMod ` RRfld ) ) x ) )`
30 24 29 mp3an1
` |-  ( ( z e. ZZ /\ x e. RR ) -> ( z ( .g ` CCfld ) x ) = ( z ( .s ` ( ZMod ` RRfld ) ) x ) )`
31 cnfldmulg
` |-  ( ( z e. ZZ /\ x e. CC ) -> ( z ( .g ` CCfld ) x ) = ( z x. x ) )`
32 21 31 syldan
` |-  ( ( z e. ZZ /\ x e. RR ) -> ( z ( .g ` CCfld ) x ) = ( z x. x ) )`
33 30 32 eqtr3d
` |-  ( ( z e. ZZ /\ x e. RR ) -> ( z ( .s ` ( ZMod ` RRfld ) ) x ) = ( z x. x ) )`
34 33 fveq2d
` |-  ( ( z e. ZZ /\ x e. RR ) -> ( ( abs |` RR ) ` ( z ( .s ` ( ZMod ` RRfld ) ) x ) ) = ( ( abs |` RR ) ` ( z x. x ) ) )`
35 zre
` |-  ( z e. ZZ -> z e. RR )`
36 remulcl
` |-  ( ( z e. RR /\ x e. RR ) -> ( z x. x ) e. RR )`
37 fvres
` |-  ( ( z x. x ) e. RR -> ( ( abs |` RR ) ` ( z x. x ) ) = ( abs ` ( z x. x ) ) )`
38 36 37 syl
` |-  ( ( z e. RR /\ x e. RR ) -> ( ( abs |` RR ) ` ( z x. x ) ) = ( abs ` ( z x. x ) ) )`
39 35 38 sylan
` |-  ( ( z e. ZZ /\ x e. RR ) -> ( ( abs |` RR ) ` ( z x. x ) ) = ( abs ` ( z x. x ) ) )`
40 34 39 eqtrd
` |-  ( ( z e. ZZ /\ x e. RR ) -> ( ( abs |` RR ) ` ( z ( .s ` ( ZMod ` RRfld ) ) x ) ) = ( abs ` ( z x. x ) ) )`
41 fvres
` |-  ( z e. ZZ -> ( ( abs |` ZZ ) ` z ) = ( abs ` z ) )`
42 fvres
` |-  ( x e. RR -> ( ( abs |` RR ) ` x ) = ( abs ` x ) )`
43 41 42 oveqan12d
` |-  ( ( z e. ZZ /\ x e. RR ) -> ( ( ( abs |` ZZ ) ` z ) x. ( ( abs |` RR ) ` x ) ) = ( ( abs ` z ) x. ( abs ` x ) ) )`
44 22 40 43 3eqtr4d
` |-  ( ( z e. ZZ /\ x e. RR ) -> ( ( abs |` RR ) ` ( z ( .s ` ( ZMod ` RRfld ) ) x ) ) = ( ( ( abs |` ZZ ) ` z ) x. ( ( abs |` RR ) ` x ) ) )`
45 44 rgen2
` |-  A. z e. ZZ A. x e. RR ( ( abs |` RR ) ` ( z ( .s ` ( ZMod ` RRfld ) ) x ) ) = ( ( ( abs |` ZZ ) ` z ) x. ( ( abs |` RR ) ` x ) )`
46 rebase
` |-  RR = ( Base ` RRfld )`
47 7 46 zlmbas
` |-  RR = ( Base ` ( ZMod ` RRfld ) )`
48 recusp
` |-  RRfld e. CUnifSp`
49 48 elexi
` |-  RRfld e. _V`
50 cnring
` |-  CCfld e. Ring`
51 ringmnd
` |-  ( CCfld e. Ring -> CCfld e. Mnd )`
52 50 51 ax-mp
` |-  CCfld e. Mnd`
53 0re
` |-  0 e. RR`
54 ax-resscn
` |-  RR C_ CC`
55 cnfldbas
` |-  CC = ( Base ` CCfld )`
56 cnfld0
` |-  0 = ( 0g ` CCfld )`
57 cnfldnm
` |-  abs = ( norm ` CCfld )`
58 4 55 56 57 ressnm
` |-  ( ( CCfld e. Mnd /\ 0 e. RR /\ RR C_ CC ) -> ( abs |` RR ) = ( norm ` RRfld ) )`
59 52 53 54 58 mp3an
` |-  ( abs |` RR ) = ( norm ` RRfld )`
60 7 59 zlmnm
` |-  ( RRfld e. _V -> ( abs |` RR ) = ( norm ` ( ZMod ` RRfld ) ) )`
61 49 60 ax-mp
` |-  ( abs |` RR ) = ( norm ` ( ZMod ` RRfld ) )`
62 eqid
` |-  ( .s ` ( ZMod ` RRfld ) ) = ( .s ` ( ZMod ` RRfld ) )`
63 7 zlmsca
` |-  ( RRfld e. _V -> ZZring = ( Scalar ` ( ZMod ` RRfld ) ) )`
64 49 63 ax-mp
` |-  ZZring = ( Scalar ` ( ZMod ` RRfld ) )`
65 zringbas
` |-  ZZ = ( Base ` ZZring )`
66 zringnm
` |-  ( norm ` ZZring ) = ( abs |` ZZ )`
67 66 eqcomi
` |-  ( abs |` ZZ ) = ( norm ` ZZring )`
68 47 61 62 64 65 67 isnlm
` |-  ( ( ZMod ` RRfld ) e. NrmMod <-> ( ( ( ZMod ` RRfld ) e. NrmGrp /\ ( ZMod ` RRfld ) e. LMod /\ ZZring e. NrmRing ) /\ A. z e. ZZ A. x e. RR ( ( abs |` RR ) ` ( z ( .s ` ( ZMod ` RRfld ) ) x ) ) = ( ( ( abs |` ZZ ) ` z ) x. ( ( abs |` RR ) ` x ) ) ) )`
69 17 45 68 mpbir2an
` |-  ( ZMod ` RRfld ) e. NrmMod`