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 ↾s ℝ )
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 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → 𝑧 ∈ ℤ )
19 18 zcnd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → 𝑧 ∈ ℂ )
20 simpr ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
21 20 recnd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
22 19 21 absmuld ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ( abs ‘ ( 𝑧 · 𝑥 ) ) = ( ( abs ‘ 𝑧 ) · ( abs ‘ 𝑥 ) ) )
23 subrgsubg ⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝ ∈ ( SubGrp ‘ ℂfld ) )
24 3 23 ax-mp ⊢ ℝ ∈ ( SubGrp ‘ ℂfld )
25 eqid ⊢ ( .g ‘ ℂfld ) = ( .g ‘ ℂfld )
26 eqid ⊢ ( .g ‘ ℝfld ) = ( .g ‘ ℝfld )
27 7 26 zlmvsca ⊢ ( .g ‘ ℝfld ) = ( ·𝑠 ‘ ( ℤMod ‘ ℝfld ) )
28 27 eqcomi ⊢ ( ·𝑠 ‘ ( ℤMod ‘ ℝfld ) ) = ( .g ‘ ℝfld )
29 25 4 28 subgmulg ⊢ ( ( ℝ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ( 𝑧 ( .g ‘ ℂfld ) 𝑥 ) = ( 𝑧 ( ·𝑠 ‘ ( ℤMod ‘ ℝfld ) ) 𝑥 ) )
30 24 29 mp3an1 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ( 𝑧 ( .g ‘ ℂfld ) 𝑥 ) = ( 𝑧 ( ·𝑠 ‘ ( ℤMod ‘ ℝfld ) ) 𝑥 ) )
31 cnfldmulg ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℂ ) → ( 𝑧 ( .g ‘ ℂfld ) 𝑥 ) = ( 𝑧 · 𝑥 ) )
32 21 31 syldan ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ( 𝑧 ( .g ‘ ℂfld ) 𝑥 ) = ( 𝑧 · 𝑥 ) )
33 30 32 eqtr3d ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ( 𝑧 ( ·𝑠 ‘ ( ℤMod ‘ ℝfld ) ) 𝑥 ) = ( 𝑧 · 𝑥 ) )
34 33 fveq2d ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ( ( abs ↾ ℝ ) ‘ ( 𝑧 ( ·𝑠 ‘ ( ℤMod ‘ ℝfld ) ) 𝑥 ) ) = ( ( abs ↾ ℝ ) ‘ ( 𝑧 · 𝑥 ) ) )
35 zre ⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℝ )
36 remulcl ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑧 · 𝑥 ) ∈ ℝ )
37 fvres ⊢ ( ( 𝑧 · 𝑥 ) ∈ ℝ → ( ( abs ↾ ℝ ) ‘ ( 𝑧 · 𝑥 ) ) = ( abs ‘ ( 𝑧 · 𝑥 ) ) )
38 36 37 syl ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( abs ↾ ℝ ) ‘ ( 𝑧 · 𝑥 ) ) = ( abs ‘ ( 𝑧 · 𝑥 ) ) )
39 35 38 sylan ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ( ( abs ↾ ℝ ) ‘ ( 𝑧 · 𝑥 ) ) = ( abs ‘ ( 𝑧 · 𝑥 ) ) )
40 34 39 eqtrd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ( ( abs ↾ ℝ ) ‘ ( 𝑧 ( ·𝑠 ‘ ( ℤMod ‘ ℝfld ) ) 𝑥 ) ) = ( abs ‘ ( 𝑧 · 𝑥 ) ) )
41 fvres ⊢ ( 𝑧 ∈ ℤ → ( ( abs ↾ ℤ ) ‘ 𝑧 ) = ( abs ‘ 𝑧 ) )
42 fvres ⊢ ( 𝑥 ∈ ℝ → ( ( abs ↾ ℝ ) ‘ 𝑥 ) = ( abs ‘ 𝑥 ) )
43 41 42 oveqan12d ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ( ( ( abs ↾ ℤ ) ‘ 𝑧 ) · ( ( abs ↾ ℝ ) ‘ 𝑥 ) ) = ( ( abs ‘ 𝑧 ) · ( abs ‘ 𝑥 ) ) )
44 22 40 43 3eqtr4d ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ( ( abs ↾ ℝ ) ‘ ( 𝑧 ( ·𝑠 ‘ ( ℤMod ‘ ℝfld ) ) 𝑥 ) ) = ( ( ( abs ↾ ℤ ) ‘ 𝑧 ) · ( ( abs ↾ ℝ ) ‘ 𝑥 ) ) )
45 44 rgen2 ⊢ ∀ 𝑧 ∈ ℤ ∀ 𝑥 ∈ ℝ ( ( abs ↾ ℝ ) ‘ ( 𝑧 ( ·𝑠 ‘ ( ℤMod ‘ ℝfld ) ) 𝑥 ) ) = ( ( ( abs ↾ ℤ ) ‘ 𝑧 ) · ( ( abs ↾ ℝ ) ‘ 𝑥 ) )
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 = ( 0g ‘ ℂ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 ) ∧ ∀ 𝑧 ∈ ℤ ∀ 𝑥 ∈ ℝ ( ( abs ↾ ℝ ) ‘ ( 𝑧 ( ·𝑠 ‘ ( ℤMod ‘ ℝfld ) ) 𝑥 ) ) = ( ( ( abs ↾ ℤ ) ‘ 𝑧 ) · ( ( abs ↾ ℝ ) ‘ 𝑥 ) ) ) )
69 17 45 68 mpbir2an ⊢ ( ℤMod ‘ ℝfld ) ∈ NrmMod