| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cnnrg |
⊢ ℂfld ∈ NrmRing |
| 2 |
|
eqid |
⊢ ( ℤMod ‘ ℂfld ) = ( ℤMod ‘ ℂfld ) |
| 3 |
2
|
zhmnrg |
⊢ ( ℂfld ∈ NrmRing → ( ℤMod ‘ ℂfld ) ∈ NrmRing ) |
| 4 |
|
nrgngp |
⊢ ( ( ℤMod ‘ ℂfld ) ∈ NrmRing → ( ℤMod ‘ ℂfld ) ∈ NrmGrp ) |
| 5 |
1 3 4
|
mp2b |
⊢ ( ℤMod ‘ ℂfld ) ∈ NrmGrp |
| 6 |
|
nrgring |
⊢ ( ℂfld ∈ NrmRing → ℂfld ∈ Ring ) |
| 7 |
|
ringabl |
⊢ ( ℂfld ∈ Ring → ℂfld ∈ Abel ) |
| 8 |
1 6 7
|
mp2b |
⊢ ℂfld ∈ Abel |
| 9 |
2
|
zlmlmod |
⊢ ( ℂfld ∈ Abel ↔ ( ℤMod ‘ ℂfld ) ∈ LMod ) |
| 10 |
8 9
|
mpbi |
⊢ ( ℤMod ‘ ℂfld ) ∈ LMod |
| 11 |
|
zringnrg |
⊢ ℤring ∈ NrmRing |
| 12 |
5 10 11
|
3pm3.2i |
⊢ ( ( ℤMod ‘ ℂfld ) ∈ NrmGrp ∧ ( ℤMod ‘ ℂfld ) ∈ LMod ∧ ℤring ∈ NrmRing ) |
| 13 |
|
simpl |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℂ ) → 𝑧 ∈ ℤ ) |
| 14 |
13
|
zcnd |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℂ ) → 𝑧 ∈ ℂ ) |
| 15 |
|
simpr |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ ) |
| 16 |
14 15
|
absmuld |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℂ ) → ( abs ‘ ( 𝑧 · 𝑥 ) ) = ( ( abs ‘ 𝑧 ) · ( abs ‘ 𝑥 ) ) ) |
| 17 |
|
cnfldmulg |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℂ ) → ( 𝑧 ( .g ‘ ℂfld ) 𝑥 ) = ( 𝑧 · 𝑥 ) ) |
| 18 |
17
|
fveq2d |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℂ ) → ( abs ‘ ( 𝑧 ( .g ‘ ℂfld ) 𝑥 ) ) = ( abs ‘ ( 𝑧 · 𝑥 ) ) ) |
| 19 |
|
fvres |
⊢ ( 𝑧 ∈ ℤ → ( ( abs ↾ ℤ ) ‘ 𝑧 ) = ( abs ‘ 𝑧 ) ) |
| 20 |
19
|
adantr |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℂ ) → ( ( abs ↾ ℤ ) ‘ 𝑧 ) = ( abs ‘ 𝑧 ) ) |
| 21 |
20
|
oveq1d |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℂ ) → ( ( ( abs ↾ ℤ ) ‘ 𝑧 ) · ( abs ‘ 𝑥 ) ) = ( ( abs ‘ 𝑧 ) · ( abs ‘ 𝑥 ) ) ) |
| 22 |
16 18 21
|
3eqtr4d |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℂ ) → ( abs ‘ ( 𝑧 ( .g ‘ ℂfld ) 𝑥 ) ) = ( ( ( abs ↾ ℤ ) ‘ 𝑧 ) · ( abs ‘ 𝑥 ) ) ) |
| 23 |
22
|
rgen2 |
⊢ ∀ 𝑧 ∈ ℤ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝑧 ( .g ‘ ℂfld ) 𝑥 ) ) = ( ( ( abs ↾ ℤ ) ‘ 𝑧 ) · ( abs ‘ 𝑥 ) ) |
| 24 |
|
cnfldbas |
⊢ ℂ = ( Base ‘ ℂfld ) |
| 25 |
2 24
|
zlmbas |
⊢ ℂ = ( Base ‘ ( ℤMod ‘ ℂfld ) ) |
| 26 |
|
cnfldex |
⊢ ℂfld ∈ V |
| 27 |
|
cnfldnm |
⊢ abs = ( norm ‘ ℂfld ) |
| 28 |
2 27
|
zlmnm |
⊢ ( ℂfld ∈ V → abs = ( norm ‘ ( ℤMod ‘ ℂfld ) ) ) |
| 29 |
26 28
|
ax-mp |
⊢ abs = ( norm ‘ ( ℤMod ‘ ℂfld ) ) |
| 30 |
|
eqid |
⊢ ( .g ‘ ℂfld ) = ( .g ‘ ℂfld ) |
| 31 |
2 30
|
zlmvsca |
⊢ ( .g ‘ ℂfld ) = ( ·𝑠 ‘ ( ℤMod ‘ ℂfld ) ) |
| 32 |
2
|
zlmsca |
⊢ ( ℂfld ∈ V → ℤring = ( Scalar ‘ ( ℤMod ‘ ℂfld ) ) ) |
| 33 |
26 32
|
ax-mp |
⊢ ℤring = ( Scalar ‘ ( ℤMod ‘ ℂfld ) ) |
| 34 |
|
zringbas |
⊢ ℤ = ( Base ‘ ℤring ) |
| 35 |
|
zringnm |
⊢ ( norm ‘ ℤring ) = ( abs ↾ ℤ ) |
| 36 |
35
|
eqcomi |
⊢ ( abs ↾ ℤ ) = ( norm ‘ ℤring ) |
| 37 |
25 29 31 33 34 36
|
isnlm |
⊢ ( ( ℤMod ‘ ℂfld ) ∈ NrmMod ↔ ( ( ( ℤMod ‘ ℂfld ) ∈ NrmGrp ∧ ( ℤMod ‘ ℂfld ) ∈ LMod ∧ ℤring ∈ NrmRing ) ∧ ∀ 𝑧 ∈ ℤ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝑧 ( .g ‘ ℂfld ) 𝑥 ) ) = ( ( ( abs ↾ ℤ ) ‘ 𝑧 ) · ( abs ‘ 𝑥 ) ) ) ) |
| 38 |
12 23 37
|
mpbir2an |
⊢ ( ℤMod ‘ ℂfld ) ∈ NrmMod |