Theorem vonsn

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)

	Ref	Expression
Hypotheses	vonsn.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	vonsn.2	⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m 𝑋 ) )
Assertion	vonsn	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ { 𝐴 } ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		vonsn.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		vonsn.2	⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m 𝑋 ) )
3		fveq2	⊢ ( 𝑋 = ∅ → ( voln ‘ 𝑋 ) = ( voln ‘ ∅ ) )
4	3	fveq1d	⊢ ( 𝑋 = ∅ → ( ( voln ‘ 𝑋 ) ‘ { 𝐴 } ) = ( ( voln ‘ ∅ ) ‘ { 𝐴 } ) )
5	4	adantl	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln ‘ 𝑋 ) ‘ { 𝐴 } ) = ( ( voln ‘ ∅ ) ‘ { 𝐴 } ) )
6		0fi	⊢ ∅ ∈ Fin
7	6	a1i	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∅ ∈ Fin )
8	2	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 ∈ ( ℝ ↑m 𝑋 ) )
9		oveq2	⊢ ( 𝑋 = ∅ → ( ℝ ↑m 𝑋 ) = ( ℝ ↑m ∅ ) )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ℝ ↑m 𝑋 ) = ( ℝ ↑m ∅ ) )
11	8 10	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 ∈ ( ℝ ↑m ∅ ) )
12	7 11	snvonmbl	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → { 𝐴 } ∈ dom ( voln ‘ ∅ ) )
13	12	von0val	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln ‘ ∅ ) ‘ { 𝐴 } ) = 0 )
14	5 13	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln ‘ 𝑋 ) ‘ { 𝐴 } ) = 0 )
15		neqne	⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
16	15	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
17	2	rrxsnicc	⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) = { 𝐴 } )
18	17	eqcomd	⊢ ( 𝜑 → { 𝐴 } = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) )
19	18	fveq2d	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ { 𝐴 } ) = ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) ) )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ( voln ‘ 𝑋 ) ‘ { 𝐴 } ) = ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) ) )
21	1	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ∈ Fin )
22		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ≠ ∅ )
23		elmapi	⊢ ( 𝐴 ∈ ( ℝ ↑m 𝑋 ) → 𝐴 : 𝑋 ⟶ ℝ )
24	2 23	syl	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝐴 : 𝑋 ⟶ ℝ )
26		eqid	⊢ X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) )
27	21 22 25 25 26	vonn0icc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) ) )
28	24	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
29	28	rexrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ* )
30		iccid	⊢ ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ* → ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) = { ( 𝐴 ‘ 𝑘 ) } )
31	29 30	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) = { ( 𝐴 ‘ 𝑘 ) } )
32	31	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) ) = ( vol ‘ { ( 𝐴 ‘ 𝑘 ) } ) )
33		volsn	⊢ ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ → ( vol ‘ { ( 𝐴 ‘ 𝑘 ) } ) = 0 )
34	28 33	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ { ( 𝐴 ‘ 𝑘 ) } ) = 0 )
35	32 34	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) ) = 0 )
36	35	prodeq2dv	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 0 )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 0 )
38		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
39		fprodconst	⊢ ( ( 𝑋 ∈ Fin ∧ 0 ∈ ℂ ) → ∏ 𝑘 ∈ 𝑋 0 = ( 0 ↑ ( ♯ ‘ 𝑋 ) ) )
40	1 38 39	syl2anc	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 0 = ( 0 ↑ ( ♯ ‘ 𝑋 ) ) )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∏ 𝑘 ∈ 𝑋 0 = ( 0 ↑ ( ♯ ‘ 𝑋 ) ) )
42		hashnncl	⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
43	1 42	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
44	43	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
45	22 44	mpbird	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ♯ ‘ 𝑋 ) ∈ ℕ )
46		0exp	⊢ ( ( ♯ ‘ 𝑋 ) ∈ ℕ → ( 0 ↑ ( ♯ ‘ 𝑋 ) ) = 0 )
47	45 46	syl	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 0 ↑ ( ♯ ‘ 𝑋 ) ) = 0 )
48	37 41 47	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) ) = 0 )
49	20 27 48	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ( voln ‘ 𝑋 ) ‘ { 𝐴 } ) = 0 )
50	16 49	syldan	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ( voln ‘ 𝑋 ) ‘ { 𝐴 } ) = 0 )
51	14 50	pm2.61dan	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ { 𝐴 } ) = 0 )