Metamath Proof Explorer

Theorem rezh

Description: The ZZ -module of RR is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018)

Ref Expression
Assertion rezh ⊢ ℤMod ⁡ ℝ fld ∈ NrmMod

Proof

Step Hyp Ref Expression
1 cnnrg ⊢ ℂ fld ∈ NrmRing
2 resubdrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing
3 2 simpli ⊢ ℝ ∈ SubRing ⁡ ℂ fld
4 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
5 4 subrgnrg ⊢ ℂ fld ∈ NrmRing ∧ ℝ ∈ SubRing ⁡ ℂ fld → ℝ fld ∈ NrmRing
6 1 3 5 mp2an ⊢ ℝ fld ∈ NrmRing
7 eqid ⊢ ℤMod ⁡ ℝ fld = ℤMod ⁡ ℝ fld
8 7 zhmnrg ⊢ ℝ fld ∈ NrmRing → ℤMod ⁡ ℝ fld ∈ NrmRing
9 nrgngp ⊢ ℤMod ⁡ ℝ fld ∈ NrmRing → ℤMod ⁡ ℝ fld ∈ NrmGrp
10 6 8 9 mp2b ⊢ ℤMod ⁡ ℝ fld ∈ NrmGrp
11 nrgring ⊢ ℝ fld ∈ NrmRing → ℝ fld ∈ Ring
12 ringabl ⊢ ℝ fld ∈ Ring → ℝ fld ∈ Abel
13 6 11 12 mp2b ⊢ ℝ fld ∈ Abel
14 7 zlmlmod ⊢ ℝ fld ∈ Abel ↔ ℤMod ⁡ ℝ fld ∈ LMod
15 13 14 mpbi ⊢ ℤMod ⁡ ℝ fld ∈ LMod
16 zringnrg ⊢ ℤ ring ∈ NrmRing
17 10 15 16 3pm3.2i ⊢ ℤMod ⁡ ℝ fld ∈ NrmGrp ∧ ℤMod ⁡ ℝ fld ∈ LMod ∧ ℤ ring ∈ NrmRing
18 simpl ⊢ z ∈ ℤ ∧ x ∈ ℝ → z ∈ ℤ
19 18 zcnd ⊢ z ∈ ℤ ∧ x ∈ ℝ → z ∈ ℂ
20 simpr ⊢ z ∈ ℤ ∧ x ∈ ℝ → x ∈ ℝ
21 20 recnd ⊢ z ∈ ℤ ∧ x ∈ ℝ → x ∈ ℂ
22 19 21 absmuld ⊢ z ∈ ℤ ∧ x ∈ ℝ → z ⁢ x = z ⁢ x
23 subrgsubg ⊢ ℝ ∈ SubRing ⁡ ℂ fld → ℝ ∈ SubGrp ⁡ ℂ fld
24 3 23 ax-mp ⊢ ℝ ∈ SubGrp ⁡ ℂ fld
25 eqid ⊢ ⋅ ℂ fld = ⋅ ℂ fld
26 eqid ⊢ ⋅ ℝ fld = ⋅ ℝ fld
27 7 26 zlmvsca ⊢ ⋅ ℝ fld = ⋅ ℤMod ⁡ ℝ fld
28 27 eqcomi ⊢ ⋅ ℤMod ⁡ ℝ fld = ⋅ ℝ fld
29 25 4 28 subgmulg ⊢ ℝ ∈ SubGrp ⁡ ℂ fld ∧ z ∈ ℤ ∧ x ∈ ℝ → z ⋅ ℂ fld x = z ⋅ ℤMod ⁡ ℝ fld x
30 24 29 mp3an1 ⊢ z ∈ ℤ ∧ x ∈ ℝ → z ⋅ ℂ fld x = z ⋅ ℤMod ⁡ ℝ fld x
31 cnfldmulg ⊢ z ∈ ℤ ∧ x ∈ ℂ → z ⋅ ℂ fld x = z ⁢ x
32 21 31 syldan ⊢ z ∈ ℤ ∧ x ∈ ℝ → z ⋅ ℂ fld x = z ⁢ x
33 30 32 eqtr3d ⊢ z ∈ ℤ ∧ x ∈ ℝ → z ⋅ ℤMod ⁡ ℝ fld x = z ⁢ x
34 33 fveq2d ⊢ z ∈ ℤ ∧ x ∈ ℝ → abs ↾ ℝ ⁡ z ⋅ ℤMod ⁡ ℝ fld x = abs ↾ ℝ ⁡ z ⁢ x
35 zre ⊢ z ∈ ℤ → z ∈ ℝ
36 remulcl ⊢ z ∈ ℝ ∧ x ∈ ℝ → z ⁢ x ∈ ℝ
37 fvres ⊢ z ⁢ x ∈ ℝ → abs ↾ ℝ ⁡ z ⁢ x = z ⁢ x
38 36 37 syl ⊢ z ∈ ℝ ∧ x ∈ ℝ → abs ↾ ℝ ⁡ z ⁢ x = z ⁢ x
39 35 38 sylan ⊢ z ∈ ℤ ∧ x ∈ ℝ → abs ↾ ℝ ⁡ z ⁢ x = z ⁢ x
40 34 39 eqtrd ⊢ z ∈ ℤ ∧ x ∈ ℝ → abs ↾ ℝ ⁡ z ⋅ ℤMod ⁡ ℝ fld x = z ⁢ x
41 fvres ⊢ z ∈ ℤ → abs ↾ ℤ ⁡ z = z
42 fvres ⊢ x ∈ ℝ → abs ↾ ℝ ⁡ x = x
43 41 42 oveqan12d ⊢ z ∈ ℤ ∧ x ∈ ℝ → abs ↾ ℤ ⁡ z ⁢ abs ↾ ℝ ⁡ x = z ⁢ x
44 22 40 43 3eqtr4d ⊢ z ∈ ℤ ∧ x ∈ ℝ → abs ↾ ℝ ⁡ z ⋅ ℤMod ⁡ ℝ fld x = abs ↾ ℤ ⁡ z ⁢ abs ↾ ℝ ⁡ x
45 44 rgen2 ⊢ ∀ z ∈ ℤ ∀ x ∈ ℝ abs ↾ ℝ ⁡ z ⋅ ℤMod ⁡ ℝ fld x = abs ↾ ℤ ⁡ z ⁢ abs ↾ ℝ ⁡ x
46 rebase ⊢ ℝ = Base ℝ fld
47 7 46 zlmbas ⊢ ℝ = Base ℤMod ⁡ ℝ fld
48 recusp ⊢ ℝ fld ∈ CUnifSp
49 48 elexi ⊢ ℝ fld ∈ V
50 cnring ⊢ ℂ fld ∈ Ring
51 ringmnd ⊢ ℂ fld ∈ Ring → ℂ fld ∈ Mnd
52 50 51 ax-mp ⊢ ℂ fld ∈ Mnd
53 0re ⊢ 0 ∈ ℝ
54 ax-resscn ⊢ ℝ ⊆ ℂ
55 cnfldbas ⊢ ℂ = Base ℂ fld
56 cnfld0 ⊢ 0 = 0 ℂ fld
57 cnfldnm ⊢ abs = norm ⁡ ℂ fld
58 4 55 56 57 ressnm ⊢ ℂ fld ∈ Mnd ∧ 0 ∈ ℝ ∧ ℝ ⊆ ℂ → abs ↾ ℝ = norm ⁡ ℝ fld
59 52 53 54 58 mp3an ⊢ abs ↾ ℝ = norm ⁡ ℝ fld
60 7 59 zlmnm ⊢ ℝ fld ∈ V → abs ↾ ℝ = norm ⁡ ℤMod ⁡ ℝ fld
61 49 60 ax-mp ⊢ abs ↾ ℝ = norm ⁡ ℤMod ⁡ ℝ fld
62 eqid ⊢ ⋅ ℤMod ⁡ ℝ fld = ⋅ ℤMod ⁡ ℝ fld
63 7 zlmsca ⊢ ℝ fld ∈ V → ℤ ring = Scalar ⁡ ℤMod ⁡ ℝ fld
64 49 63 ax-mp ⊢ ℤ ring = Scalar ⁡ ℤMod ⁡ ℝ fld
65 zringbas ⊢ ℤ = Base ℤ ring
66 zringnm ⊢ norm ⁡ ℤ ring = abs ↾ ℤ
67 66 eqcomi ⊢ abs ↾ ℤ = norm ⁡ ℤ ring
68 47 61 62 64 65 67 isnlm ⊢ ℤMod ⁡ ℝ fld ∈ NrmMod ↔ ℤMod ⁡ ℝ fld ∈ NrmGrp ∧ ℤMod ⁡ ℝ fld ∈ LMod ∧ ℤ ring ∈ NrmRing ∧ ∀ z ∈ ℤ ∀ x ∈ ℝ abs ↾ ℝ ⁡ z ⋅ ℤMod ⁡ ℝ fld x = abs ↾ ℤ ⁡ z ⁢ abs ↾ ℝ ⁡ x
69 17 45 68 mpbir2an ⊢ ℤMod ⁡ ℝ fld ∈ NrmMod