Metamath Proof Explorer


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 0fin ∅ ∈ 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 ffvelrnda ( ( 𝜑𝑘𝑋 ) → ( 𝐴𝑘 ) ∈ ℝ )
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 )