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 ) )
20 19 adantr
 |-  ( ( 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