vonsn - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > vonsn		Structured version Visualization version GIF version

Theorem vonsn 47795

Description: The n-dimensional Lebesgue measure of a singleton is zero. This is the first statement in Proposition 115G (e) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.)

**Hypotheses**
Ref	Expression
vonsn.1	⊢ (𝜑 → 𝑋 ∈ Fin)
vonsn.2	⊢ (𝜑 → 𝐴 ∈ (ℝ ↑_m 𝑋))

**Assertion**
Ref	Expression
vonsn	⊢ (𝜑 → ((voln‘𝑋)‘{𝐴}) = 0)

Proof of Theorem vonsn Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6886	. . . . 5 ⊢ (𝑋 = ∅ → (voln‘𝑋) = (voln‘∅))
2	1	fveq1d 6888	. . . 4 ⊢ (𝑋 = ∅ → ((voln‘𝑋)‘{𝐴}) = ((voln‘∅)‘{𝐴}))
3	2	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘{𝐴}) = ((voln‘∅)‘{𝐴}))
4		0fi 9074	. . . . . 6 ⊢ ∅ ∈ Fin
5	4	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈ Fin)
6		vonsn.2	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ (ℝ ↑_m 𝑋))
7	6	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴 ∈ (ℝ ↑_m 𝑋))
8		oveq2 7429	. . . . . . 7 ⊢ (𝑋 = ∅ → (ℝ ↑_m 𝑋) = (ℝ ↑_m ∅))
9	8	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (ℝ ↑_m 𝑋) = (ℝ ↑_m ∅))
10	7, 9	eleqtrd 2862	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴 ∈ (ℝ ↑_m ∅))
11	5, 10	snvonmbl 47790	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → {𝐴} ∈ dom (voln‘∅))
12	11	von0val 47775	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘∅)‘{𝐴}) = 0)
13	3, 12	eqtrd 2795	. 2 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘{𝐴}) = 0)
14		neqne 2963	. . . 4 ⊢ (¬ 𝑋 = ∅ → 𝑋 ≠ ∅)
15	14	adantl 487	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅)
16	6	rrxsnicc 47404	. . . . . . 7 ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) = {𝐴})
17	16	eqcomd 2766	. . . . . 6 ⊢ (𝜑 → {𝐴} = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)))
18	17	fveq2d 6890	. . . . 5 ⊢ (𝜑 → ((voln‘𝑋)‘{𝐴}) = ((voln‘𝑋)‘X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))))
19	18	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln‘𝑋)‘{𝐴}) = ((voln‘𝑋)‘X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))))
20		vonsn.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ Fin)
21	20	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ∈ Fin)
22		simpr 490	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ≠ ∅)
23		elmapi 8873	. . . . . . 7 ⊢ (𝐴 ∈ (ℝ ↑_m 𝑋) → 𝐴:𝑋⟶ℝ)
24	6, 23	syl 18	. . . . . 6 ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
25	24	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐴:𝑋⟶ℝ)
26		eqid 2760	. . . . 5 ⊢ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))
27	21, 22, 25, 25, 26	vonn0icc 47792	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln‘𝑋)‘X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘))) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,](𝐴‘𝑘))))
28	24	ffvelcdmda 7085	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ)
29	28	rexrd 11363	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ^*)
30		iccid 13525	. . . . . . . . . 10 ⊢ ((𝐴‘𝑘) ∈ ℝ^* → ((𝐴‘𝑘)[,](𝐴‘𝑘)) = {(𝐴‘𝑘)})
31	29, 30	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,](𝐴‘𝑘)) = {(𝐴‘𝑘)})
32	31	fveq2d 6890	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,](𝐴‘𝑘))) = (vol‘{(𝐴‘𝑘)}))
33		volsn 47071	. . . . . . . . 9 ⊢ ((𝐴‘𝑘) ∈ ℝ → (vol‘{(𝐴‘𝑘)}) = 0)
34	28, 33	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘{(𝐴‘𝑘)}) = 0)
35	32, 34	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,](𝐴‘𝑘))) = 0)
36	35	prodeq2dv 16096	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,](𝐴‘𝑘))) = ∏𝑘 ∈ 𝑋 0)
37	36	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,](𝐴‘𝑘))) = ∏𝑘 ∈ 𝑋 0)
38		0cnd 11303	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℂ)
39		fprodconst 16151	. . . . . . 7 ⊢ ((𝑋 ∈ Fin ∧ 0 ∈ ℂ) → ∏𝑘 ∈ 𝑋 0 = (0↑(♯‘𝑋)))
40	20, 38, 39	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 0 = (0↑(♯‘𝑋)))
41	40	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∏𝑘 ∈ 𝑋 0 = (0↑(♯‘𝑋)))
42		hashnncl 14514	. . . . . . . . 9 ⊢ (𝑋 ∈ Fin → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
43	20, 42	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
44	43	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
45	22, 44	mpbird 260	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (♯‘𝑋) ∈ ℕ)
46		0exp 14244	. . . . . 6 ⊢ ((♯‘𝑋) ∈ ℕ → (0↑(♯‘𝑋)) = 0)
47	45, 46	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (0↑(♯‘𝑋)) = 0)
48	37, 41, 47	3eqtrd 2799	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,](𝐴‘𝑘))) = 0)
49	19, 27, 48	3eqtrd 2799	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln‘𝑋)‘{𝐴}) = 0)
50	15, 49	syldan 603	. 2 ⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln‘𝑋)‘{𝐴}) = 0)
51	13, 50	pm2.61dan 825	1 ⊢ (𝜑 → ((voln‘𝑋)‘{𝐴}) = 0)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∅c0 4278 {csn 4584 ⟶wf 6535 ‘cfv 6539 (class class class)co 7421 ↑_m cmap 8851 Xcixp 8929 Fincfn 8977 ℂcc 11202 ℝcr 11203 0cc0 11204 ℝ^*cxr 11346 ℕcn 12339 [,]cicc 13483 ↑cexp 14208 ♯chash 14478 ∏cprod 16078 volcvol 25790 volncvoln 47642

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-inf2 9646 ax-cc 10517 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-pre-sup 11282 ax-addf 11283 ax-mulf 11284

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-disj 5070 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-of 7694 df-om 7879 df-1st 8002 df-2nd 8003 df-supp 8181 df-tpos 8247 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-2o 8481 df-oadd 8484 df-omul 8485 df-er 8721 df-map 8853 df-pm 8854 df-ixp 8930 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-fsupp 9358 df-fi 9407 df-sup 9438 df-inf 9439 df-oi 9508 df-dju 9986 df-card 10024 df-acn 10027 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-div 11978 df-nn 12340 df-2 12409 df-3 12410 df-4 12411 df-5 12412 df-6 12413 df-7 12414 df-8 12415 df-9 12416 df-n0 12611 df-z 12698 df-dec 12819 df-uz 12970 df-q 13080 df-rp 13125 df-xneg 13245 df-xadd 13246 df-xmul 13247 df-ioo 13484 df-ico 13486 df-icc 13487 df-fz 13644 df-fzo 13793 df-fl 13936 df-seq 14149 df-exp 14209 df-hash 14479 df-cj 15272 df-re 15273 df-im 15274 df-sqrt 15408 df-abs 15409 df-clim 15661 df-rlim 15662 df-sum 15860 df-prod 16079 df-struct 17331 df-sets 17348 df-slot 17366 df-ndx 17378 df-base 17394 df-ress 17415 df-plusg 17447 df-mulr 17448 df-starv 17449 df-sca 17450 df-vsca 17451 df-ip 17452 df-tset 17453 df-ple 17454 df-ds 17456 df-unif 17457 df-hom 17458 df-cco 17459 df-rest 17599 df-topn 17600 df-0g 17618 df-gsum 17619 df-topgen 17620 df-pt 17621 df-prds 17624 df-pws 17626 df-xrs 17680 df-qtop 17685 df-imas 17686 df-xps 17688 df-mre 17762 df-mrc 17763 df-acs 17765 df-mgm 18822 df-sgrp 18914 df-mnd 18930 df-mhm 18984 df-submnd 18985 df-grp 19153 df-minusg 19154 df-sbg 19155 df-mulg 19284 df-subg 19339 df-ghm 19434 df-cntz 19537 df-cmn 20002 df-abl 20003 df-mgp 20367 df-rng 20381 df-ur 20414 df-ring 20467 df-cring 20468 df-oppr 20573 df-dvdsr 20593 df-unit 20594 df-invr 20624 df-dvr 20637 df-rhm 20708 df-subrng 20804 df-subrg 20828 df-drng 20988 df-field 20989 df-abv 21072 df-staf 21102 df-srng 21103 df-lmod 21143 df-lss 21213 df-lmhm 21303 df-lvec 21384 df-sra 21454 df-rgmod 21455 df-psmet 21676 df-xmet 21677 df-met 21678 df-bl 21679 df-mopn 21680 df-cnfld 21685 df-refld 21917 df-phl 21938 df-dsmm 22044 df-frlm 22059 df-top 23218 df-topon 23235 df-topsp 23257 df-bases 23270 df-cn 23551 df-cnp 23552 df-cmp 23711 df-tx 23887 df-hmeo 24080 df-xms 24645 df-ms 24646 df-tms 24647 df-nm 24907 df-ngp 24908 df-tng 24909 df-nrg 24910 df-nlm 24911 df-cncf 25205 df-clm 25390 df-cph 25495 df-tcph 25496 df-rrx 25712 df-ovol 25791 df-vol 25792 df-salg 47413 df-sumge0 47467 df-mea 47554 df-ome 47594 df-caragen 47596 df-ovoln 47641 df-voln 47643

This theorem is used by: vonct 47797

W3C validator