Metamath Proof Explorer

Theorem cnzh

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

Ref Expression
Assertion cnzh
`|- ( ZMod ` CCfld ) e. NrmMod`

Proof

Step Hyp Ref Expression
1 cnnrg
` |-  CCfld e. NrmRing`
2 eqid
` |-  ( ZMod ` CCfld ) = ( ZMod ` CCfld )`
3 2 zhmnrg
` |-  ( CCfld e. NrmRing -> ( ZMod ` CCfld ) e. NrmRing )`
4 nrgngp
` |-  ( ( ZMod ` CCfld ) e. NrmRing -> ( ZMod ` CCfld ) e. NrmGrp )`
5 1 3 4 mp2b
` |-  ( ZMod ` CCfld ) e. NrmGrp`
6 nrgring
` |-  ( CCfld e. NrmRing -> CCfld e. Ring )`
7 ringabl
` |-  ( CCfld e. Ring -> CCfld e. Abel )`
8 1 6 7 mp2b
` |-  CCfld e. Abel`
9 2 zlmlmod
` |-  ( CCfld e. Abel <-> ( ZMod ` CCfld ) e. LMod )`
10 8 9 mpbi
` |-  ( ZMod ` CCfld ) e. LMod`
11 zringnrg
` |-  ZZring e. NrmRing`
12 5 10 11 3pm3.2i
` |-  ( ( ZMod ` CCfld ) e. NrmGrp /\ ( ZMod ` CCfld ) e. LMod /\ ZZring e. NrmRing )`
13 simpl
` |-  ( ( z e. ZZ /\ x e. CC ) -> z e. ZZ )`
14 13 zcnd
` |-  ( ( z e. ZZ /\ x e. CC ) -> z e. CC )`
15 simpr
` |-  ( ( z e. ZZ /\ x e. CC ) -> x e. CC )`
16 14 15 absmuld
` |-  ( ( z e. ZZ /\ x e. CC ) -> ( abs ` ( z x. x ) ) = ( ( abs ` z ) x. ( abs ` x ) ) )`
17 cnfldmulg
` |-  ( ( z e. ZZ /\ x e. CC ) -> ( z ( .g ` CCfld ) x ) = ( z x. x ) )`
18 17 fveq2d
` |-  ( ( z e. ZZ /\ x e. CC ) -> ( abs ` ( z ( .g ` CCfld ) x ) ) = ( abs ` ( z x. x ) ) )`
19 fvres
` |-  ( z e. ZZ -> ( ( abs |` ZZ ) ` z ) = ( abs ` z ) )`
` |-  ( ( z e. ZZ /\ x e. CC ) -> ( ( abs |` ZZ ) ` z ) = ( abs ` z ) )`
21 20 oveq1d
` |-  ( ( z e. ZZ /\ x e. CC ) -> ( ( ( abs |` ZZ ) ` z ) x. ( abs ` x ) ) = ( ( abs ` z ) x. ( abs ` x ) ) )`
22 16 18 21 3eqtr4d
` |-  ( ( z e. ZZ /\ x e. CC ) -> ( abs ` ( z ( .g ` CCfld ) x ) ) = ( ( ( abs |` ZZ ) ` z ) x. ( abs ` x ) ) )`
23 22 rgen2
` |-  A. z e. ZZ A. x e. CC ( abs ` ( z ( .g ` CCfld ) x ) ) = ( ( ( abs |` ZZ ) ` z ) x. ( abs ` x ) )`
24 cnfldbas
` |-  CC = ( Base ` CCfld )`
25 2 24 zlmbas
` |-  CC = ( Base ` ( ZMod ` CCfld ) )`
26 cnfldex
` |-  CCfld e. _V`
27 cnfldnm
` |-  abs = ( norm ` CCfld )`
28 2 27 zlmnm
` |-  ( CCfld e. _V -> abs = ( norm ` ( ZMod ` CCfld ) ) )`
29 26 28 ax-mp
` |-  abs = ( norm ` ( ZMod ` CCfld ) )`
30 eqid
` |-  ( .g ` CCfld ) = ( .g ` CCfld )`
31 2 30 zlmvsca
` |-  ( .g ` CCfld ) = ( .s ` ( ZMod ` CCfld ) )`
32 2 zlmsca
` |-  ( CCfld e. _V -> ZZring = ( Scalar ` ( ZMod ` CCfld ) ) )`
33 26 32 ax-mp
` |-  ZZring = ( Scalar ` ( ZMod ` CCfld ) )`
34 zringbas
` |-  ZZ = ( Base ` ZZring )`
35 zringnm
` |-  ( norm ` ZZring ) = ( abs |` ZZ )`
36 35 eqcomi
` |-  ( abs |` ZZ ) = ( norm ` ZZring )`
37 25 29 31 33 34 36 isnlm
` |-  ( ( ZMod ` CCfld ) e. NrmMod <-> ( ( ( ZMod ` CCfld ) e. NrmGrp /\ ( ZMod ` CCfld ) e. LMod /\ ZZring e. NrmRing ) /\ A. z e. ZZ A. x e. CC ( abs ` ( z ( .g ` CCfld ) x ) ) = ( ( ( abs |` ZZ ) ` z ) x. ( abs ` x ) ) ) )`
38 12 23 37 mpbir2an
` |-  ( ZMod ` CCfld ) e. NrmMod`