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⋅ℂfldx=z⋅ℤMod⁡ℝfldx
30 24 29 mp3an1 ⊢z∈ℤ∧x∈ℝ→z⋅ℂfldx=z⋅ℤMod⁡ℝfldx
31 cnfldmulg ⊢z∈ℤ∧x∈ℂ→z⋅ℂfldx=z⁢x
32 21 31 syldan ⊢z∈ℤ∧x∈ℝ→z⋅ℂfldx=z⁢x
33 30 32 eqtr3d ⊢z∈ℤ∧x∈ℝ→z⋅ℤMod⁡ℝfldx=z⁢x
34 33 fveq2d ⊢z∈ℤ∧x∈ℝ→abs↾ℝ⁡z⋅ℤMod⁡ℝfldx=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⁡ℝfldx=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⁡ℝfldx=abs↾ℤ⁡z⁢abs↾ℝ⁡x
45 44 rgen2 ⊢∀z∈ℤ∀x∈ℝabs↾ℝ⁡z⋅ℤMod⁡ℝfldx=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⁡ℝfldx=abs↾ℤ⁡z⁢abs↾ℝ⁡x
69 17 45 68 mpbir2an ⊢ℤMod⁡ℝfld∈NrmMod