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