rezh - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > rezh		Structured version Visualization version GIF version

Theorem rezh 34054

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

**Assertion**
Ref	Expression
rezh	⊢ (ℤMod‘ℝ_fld) ∈ NrmMod

Proof of Theorem rezh Dummy variables 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnnrg 24715	. . . . 5 ⊢ ℂ_fld ∈ NrmRing
2		resubdrg 21554	. . . . . 6 ⊢ (ℝ ∈ (SubRing‘ℂ_fld) ∧ ℝ_fld ∈ DivRing)
3	2	simpli 483	. . . . 5 ⊢ ℝ ∈ (SubRing‘ℂ_fld)
4		df-refld 21551	. . . . . 6 ⊢ ℝ_fld = (ℂ_fld ↾_s ℝ)
5	4	subrgnrg 24608	. . . . 5 ⊢ ((ℂ_fld ∈ NrmRing ∧ ℝ ∈ (SubRing‘ℂ_fld)) → ℝ_fld ∈ NrmRing)
6	1, 3, 5	mp2an 692	. . . 4 ⊢ ℝ_fld ∈ NrmRing
7		eqid 2733	. . . . 5 ⊢ (ℤMod‘ℝ_fld) = (ℤMod‘ℝ_fld)
8	7	zhmnrg 34050	. . . 4 ⊢ (ℝ_fld ∈ NrmRing → (ℤMod‘ℝ_fld) ∈ NrmRing)
9		nrgngp 24597	. . . 4 ⊢ ((ℤMod‘ℝ_fld) ∈ NrmRing → (ℤMod‘ℝ_fld) ∈ NrmGrp)
10	6, 8, 9	mp2b 10	. . 3 ⊢ (ℤMod‘ℝ_fld) ∈ NrmGrp
11		nrgring 24598	. . . . 5 ⊢ (ℝ_fld ∈ NrmRing → ℝ_fld ∈ Ring)
12		ringabl 20207	. . . . 5 ⊢ (ℝ_fld ∈ Ring → ℝ_fld ∈ Abel)
13	6, 11, 12	mp2b 10	. . . 4 ⊢ ℝ_fld ∈ Abel
14	7	zlmlmod 21468	. . . 4 ⊢ (ℝ_fld ∈ Abel ↔ (ℤMod‘ℝ_fld) ∈ LMod)
15	13, 14	mpbi 230	. . 3 ⊢ (ℤMod‘ℝ_fld) ∈ LMod
16		zringnrg 24723	. . 3 ⊢ ℤ_ring ∈ NrmRing
17	10, 15, 16	3pm3.2i 1340	. 2 ⊢ ((ℤMod‘ℝ_fld) ∈ NrmGrp ∧ (ℤMod‘ℝ_fld) ∈ LMod ∧ ℤ_ring ∈ NrmRing)
18		simpl 482	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → 𝑧 ∈ ℤ)
19	18	zcnd 12588	. . . . 5 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → 𝑧 ∈ ℂ)
20		simpr 484	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
21	20	recnd 11151	. . . . 5 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
22	19, 21	absmuld 15371	. . . 4 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → (abs‘(𝑧 · 𝑥)) = ((abs‘𝑧) · (abs‘𝑥)))
23		subrgsubg 20501	. . . . . . . . 9 ⊢ (ℝ ∈ (SubRing‘ℂ_fld) → ℝ ∈ (SubGrp‘ℂ_fld))
24	3, 23	ax-mp 5	. . . . . . . 8 ⊢ ℝ ∈ (SubGrp‘ℂ_fld)
25		eqid 2733	. . . . . . . . 9 ⊢ (._g‘ℂ_fld) = (._g‘ℂ_fld)
26		eqid 2733	. . . . . . . . . . 11 ⊢ (._g‘ℝ_fld) = (._g‘ℝ_fld)
27	7, 26	zlmvsca 21467	. . . . . . . . . 10 ⊢ (._g‘ℝ_fld) = ( ·_𝑠 ‘(ℤMod‘ℝ_fld))
28	27	eqcomi 2742	. . . . . . . . 9 ⊢ ( ·_𝑠 ‘(ℤMod‘ℝ_fld)) = (._g‘ℝ_fld)
29	25, 4, 28	subgmulg 19061	. . . . . . . 8 ⊢ ((ℝ ∈ (SubGrp‘ℂ_fld) ∧ 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → (𝑧(._g‘ℂ_fld)𝑥) = (𝑧( ·_𝑠 ‘(ℤMod‘ℝ_fld))𝑥))
30	24, 29	mp3an1 1450	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → (𝑧(._g‘ℂ_fld)𝑥) = (𝑧( ·_𝑠 ‘(ℤMod‘ℝ_fld))𝑥))
31		cnfldmulg 21349	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℂ) → (𝑧(._g‘ℂ_fld)𝑥) = (𝑧 · 𝑥))
32	21, 31	syldan 591	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → (𝑧(._g‘ℂ_fld)𝑥) = (𝑧 · 𝑥))
33	30, 32	eqtr3d 2770	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → (𝑧( ·_𝑠 ‘(ℤMod‘ℝ_fld))𝑥) = (𝑧 · 𝑥))
34	33	fveq2d 6835	. . . . 5 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → ((abs ↾ ℝ)‘(𝑧( ·_𝑠 ‘(ℤMod‘ℝ_fld))𝑥)) = ((abs ↾ ℝ)‘(𝑧 · 𝑥)))
35		zre 12483	. . . . . 6 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℝ)
36		remulcl 11102	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
37		fvres 6850	. . . . . . 7 ⊢ ((𝑧 · 𝑥) ∈ ℝ → ((abs ↾ ℝ)‘(𝑧 · 𝑥)) = (abs‘(𝑧 · 𝑥)))
38	36, 37	syl 17	. . . . . 6 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((abs ↾ ℝ)‘(𝑧 · 𝑥)) = (abs‘(𝑧 · 𝑥)))
39	35, 38	sylan 580	. . . . 5 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → ((abs ↾ ℝ)‘(𝑧 · 𝑥)) = (abs‘(𝑧 · 𝑥)))
40	34, 39	eqtrd 2768	. . . 4 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → ((abs ↾ ℝ)‘(𝑧( ·_𝑠 ‘(ℤMod‘ℝ_fld))𝑥)) = (abs‘(𝑧 · 𝑥)))
41		fvres 6850	. . . . 5 ⊢ (𝑧 ∈ ℤ → ((abs ↾ ℤ)‘𝑧) = (abs‘𝑧))
42		fvres 6850	. . . . 5 ⊢ (𝑥 ∈ ℝ → ((abs ↾ ℝ)‘𝑥) = (abs‘𝑥))
43	41, 42	oveqan12d 7374	. . . 4 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → (((abs ↾ ℤ)‘𝑧) · ((abs ↾ ℝ)‘𝑥)) = ((abs‘𝑧) · (abs‘𝑥)))
44	22, 40, 43	3eqtr4d 2778	. . 3 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → ((abs ↾ ℝ)‘(𝑧( ·_𝑠 ‘(ℤMod‘ℝ_fld))𝑥)) = (((abs ↾ ℤ)‘𝑧) · ((abs ↾ ℝ)‘𝑥)))
45	44	rgen2 3173	. 2 ⊢ ∀𝑧 ∈ ℤ ∀𝑥 ∈ ℝ ((abs ↾ ℝ)‘(𝑧( ·_𝑠 ‘(ℤMod‘ℝ_fld))𝑥)) = (((abs ↾ ℤ)‘𝑧) · ((abs ↾ ℝ)‘𝑥))
46		rebase 21552	. . . 4 ⊢ ℝ = (Base‘ℝ_fld)
47	7, 46	zlmbas 21463	. . 3 ⊢ ℝ = (Base‘(ℤMod‘ℝ_fld))
48		recusp 25329	. . . . 5 ⊢ ℝ_fld ∈ CUnifSp
49	48	elexi 3460	. . . 4 ⊢ ℝ_fld ∈ V
50		cnring 21336	. . . . . . 7 ⊢ ℂ_fld ∈ Ring
51		ringmnd 20169	. . . . . . 7 ⊢ (ℂ_fld ∈ Ring → ℂ_fld ∈ Mnd)
52	50, 51	ax-mp 5	. . . . . 6 ⊢ ℂ_fld ∈ Mnd
53		0re 11125	. . . . . 6 ⊢ 0 ∈ ℝ
54		ax-resscn 11074	. . . . . 6 ⊢ ℝ ⊆ ℂ
55		cnfldbas 21304	. . . . . . 7 ⊢ ℂ = (Base‘ℂ_fld)
56		cnfld0 21338	. . . . . . 7 ⊢ 0 = (0_g‘ℂ_fld)
57		cnfldnm 24713	. . . . . . 7 ⊢ abs = (norm‘ℂ_fld)
58	4, 55, 56, 57	ressnm 32974	. . . . . 6 ⊢ ((ℂ_fld ∈ Mnd ∧ 0 ∈ ℝ ∧ ℝ ⊆ ℂ) → (abs ↾ ℝ) = (norm‘ℝ_fld))
59	52, 53, 54, 58	mp3an 1463	. . . . 5 ⊢ (abs ↾ ℝ) = (norm‘ℝ_fld)
60	7, 59	zlmnm 34049	. . . 4 ⊢ (ℝ_fld ∈ V → (abs ↾ ℝ) = (norm‘(ℤMod‘ℝ_fld)))
61	49, 60	ax-mp 5	. . 3 ⊢ (abs ↾ ℝ) = (norm‘(ℤMod‘ℝ_fld))
62		eqid 2733	. . 3 ⊢ ( ·_𝑠 ‘(ℤMod‘ℝ_fld)) = ( ·_𝑠 ‘(ℤMod‘ℝ_fld))
63	7	zlmsca 21466	. . . 4 ⊢ (ℝ_fld ∈ V → ℤ_ring = (Scalar‘(ℤMod‘ℝ_fld)))
64	49, 63	ax-mp 5	. . 3 ⊢ ℤ_ring = (Scalar‘(ℤMod‘ℝ_fld))
65		zringbas 21399	. . 3 ⊢ ℤ = (Base‘ℤ_ring)
66		zringnm 34043	. . . 4 ⊢ (norm‘ℤ_ring) = (abs ↾ ℤ)
67	66	eqcomi 2742	. . 3 ⊢ (abs ↾ ℤ) = (norm‘ℤ_ring)
68	47, 61, 62, 64, 65, 67	isnlm 24610	. 2 ⊢ ((ℤMod‘ℝ_fld) ∈ NrmMod ↔ (((ℤMod‘ℝ_fld) ∈ NrmGrp ∧ (ℤMod‘ℝ_fld) ∈ LMod ∧ ℤ_ring ∈ NrmRing) ∧ ∀𝑧 ∈ ℤ ∀𝑥 ∈ ℝ ((abs ↾ ℝ)‘(𝑧( ·_𝑠 ‘(ℤMod‘ℝ_fld))𝑥)) = (((abs ↾ ℤ)‘𝑧) · ((abs ↾ ℝ)‘𝑥))))
69	17, 45, 68	mpbir2an 711	1 ⊢ (ℤMod‘ℝ_fld) ∈ NrmMod

Colors of variables: wff setvar class

Syntax hints: ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ∀wral 3048 Vcvv 3437 ⊆ wss 3898 ↾ cres 5623 ‘cfv 6489 (class class class)co 7355 ℂcc 11015 ℝcr 11016 0cc0 11017 · cmul 11022 ℤcz 12479 abscabs 15148 Scalarcsca 17171 ·_𝑠 cvsca 17172 Mndcmnd 18650 ._gcmg 18988 SubGrpcsubg 19041 Abelcabl 19701 Ringcrg 20159 SubRingcsubrg 20493 DivRingcdr 20653 LModclmod 20802 ℂ_fldccnfld 21300 ℤ_ringczring 21392 ℤModczlm 21446 ℝ_fldcrefld 21550 CUnifSpccusp 24231 normcnm 24511 NrmGrpcngp 24512 NrmRingcnrg 24514 NrmModcnlm 24515

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 ax-cnex 11073 ax-resscn 11074 ax-1cn 11075 ax-icn 11076 ax-addcl 11077 ax-addrcl 11078 ax-mulcl 11079 ax-mulrcl 11080 ax-mulcom 11081 ax-addass 11082 ax-mulass 11083 ax-distr 11084 ax-i2m1 11085 ax-1ne0 11086 ax-1rid 11087 ax-rnegex 11088 ax-rrecex 11089 ax-cnre 11090 ax-pre-lttri 11091 ax-pre-lttrn 11092 ax-pre-ltadd 11093 ax-pre-mulgt0 11094 ax-pre-sup 11095 ax-addf 11096 ax-mulf 11097

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-iin 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-se 5575 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-isom 6498 df-riota 7312 df-ov 7358 df-oprab 7359 df-mpo 7360 df-of 7619 df-om 7806 df-1st 7930 df-2nd 7931 df-supp 8100 df-tpos 8165 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-2o 8395 df-er 8631 df-map 8761 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9257 df-fi 9306 df-sup 9337 df-inf 9338 df-oi 9407 df-card 9843 df-pnf 11159 df-mnf 11160 df-xr 11161 df-ltxr 11162 df-le 11163 df-sub 11357 df-neg 11358 df-div 11786 df-nn 12137 df-2 12199 df-3 12200 df-4 12201 df-5 12202 df-6 12203 df-7 12204 df-8 12205 df-9 12206 df-n0 12393 df-z 12480 df-dec 12599 df-uz 12743 df-q 12853 df-rp 12897 df-xneg 13017 df-xadd 13018 df-xmul 13019 df-ioo 13256 df-ico 13258 df-icc 13259 df-fz 13415 df-fzo 13562 df-seq 13916 df-exp 13976 df-hash 14245 df-cj 15013 df-re 15014 df-im 15015 df-sqrt 15149 df-abs 15150 df-struct 17065 df-sets 17082 df-slot 17100 df-ndx 17112 df-base 17128 df-ress 17149 df-plusg 17181 df-mulr 17182 df-starv 17183 df-sca 17184 df-vsca 17185 df-ip 17186 df-tset 17187 df-ple 17188 df-ds 17190 df-unif 17191 df-hom 17192 df-cco 17193 df-rest 17333 df-topn 17334 df-0g 17352 df-gsum 17353 df-topgen 17354 df-pt 17355 df-prds 17358 df-xrs 17414 df-qtop 17419 df-imas 17420 df-xps 17422 df-mre 17496 df-mrc 17497 df-acs 17499 df-mgm 18556 df-sgrp 18635 df-mnd 18651 df-submnd 18700 df-grp 18857 df-minusg 18858 df-sbg 18859 df-mulg 18989 df-subg 19044 df-cntz 19237 df-cmn 19702 df-abl 19703 df-mgp 20067 df-rng 20079 df-ur 20108 df-ring 20161 df-cring 20162 df-oppr 20264 df-dvdsr 20284 df-unit 20285 df-invr 20315 df-dvr 20328 df-subrng 20470 df-subrg 20494 df-drng 20655 df-abv 20733 df-lmod 20804 df-psmet 21292 df-xmet 21293 df-met 21294 df-bl 21295 df-mopn 21296 df-fbas 21297 df-fg 21298 df-metu 21299 df-cnfld 21301 df-zring 21393 df-zlm 21450 df-refld 21551 df-top 22829 df-topon 22846 df-topsp 22868 df-bases 22881 df-cld 22954 df-ntr 22955 df-cls 22956 df-nei 23033 df-cn 23162 df-cnp 23163 df-haus 23250 df-cmp 23322 df-tx 23497 df-hmeo 23690 df-fil 23781 df-flim 23874 df-fcls 23876 df-ust 24136 df-utop 24166 df-uss 24191 df-usp 24192 df-cfilu 24221 df-cusp 24232 df-xms 24255 df-ms 24256 df-tms 24257 df-nm 24517 df-ngp 24518 df-nrg 24520 df-nlm 24521 df-cncf 24818 df-cfil 25202 df-cmet 25204 df-cms 25282

This theorem is referenced by: rerrext 34094

W3C validator