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 ⊢ ℤMod ⁡ ℂ fld ∈ NrmMod

Proof

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 ⊢ z ∈ ℤ ∧ x ∈ ℂ → z ∈ ℤ
14 13 zcnd ⊢ z ∈ ℤ ∧ x ∈ ℂ → z ∈ ℂ
15 simpr ⊢ z ∈ ℤ ∧ x ∈ ℂ → x ∈ ℂ
16 14 15 absmuld ⊢ z ∈ ℤ ∧ x ∈ ℂ → z ⁢ x = z ⁢ x
17 cnfldmulg ⊢ z ∈ ℤ ∧ x ∈ ℂ → z ⋅ ℂ fld x = z ⁢ x
18 17 fveq2d ⊢ z ∈ ℤ ∧ x ∈ ℂ → z ⋅ ℂ fld x = z ⁢ x
19 fvres ⊢ z ∈ ℤ → abs ↾ ℤ ⁡ z = z
20 19 adantr ⊢ z ∈ ℤ ∧ x ∈ ℂ → abs ↾ ℤ ⁡ z = z
21 20 oveq1d ⊢ z ∈ ℤ ∧ x ∈ ℂ → abs ↾ ℤ ⁡ z ⁢ x = z ⁢ x
22 16 18 21 3eqtr4d ⊢ z ∈ ℤ ∧ x ∈ ℂ → z ⋅ ℂ fld x = abs ↾ ℤ ⁡ z ⁢ x
23 22 rgen2 ⊢ ∀ z ∈ ℤ ∀ x ∈ ℂ z ⋅ ℂ fld x = abs ↾ ℤ ⁡ z ⁢ x
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 ⊢ ⋅ ℂ fld = ⋅ ℂ fld
31 2 30 zlmvsca ⊢ ⋅ ℂ 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 ∧ ∀ z ∈ ℤ ∀ x ∈ ℂ z ⋅ ℂ fld x = abs ↾ ℤ ⁡ z ⁢ x
38 12 23 37 mpbir2an ⊢ ℤMod ⁡ ℂ fld ∈ NrmMod