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 |