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