Metamath Proof Explorer

Theorem vonhoire

Description: The Lebesgue measure of a n-dimensional half-open interval is a real number. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses vonhoire.n ⊢ Ⅎ 𝑘 𝜑
vonhoire.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
vonhoire.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
vonhoire.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
Assertion vonhoire ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 vonhoire.n ⊢ Ⅎ 𝑘 𝜑
2 vonhoire.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 vonhoire.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
4 vonhoire.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
5 fveq2 ⊢ ( 𝑋 = ∅ → ( voln ‘ 𝑋 ) = ( voln ‘ ∅ ) )
6 5 fveq1d ⊢ ( 𝑋 = ∅ → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) = ( ( voln ‘ ∅ ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) = ( ( voln ‘ ∅ ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) )
8 ixpeq1 ⊢ ( 𝑋 = ∅ → X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) = X 𝑘 ∈ ∅ ( 𝐴 [,) 𝐵 ) )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) = X 𝑘 ∈ ∅ ( 𝐴 [,) 𝐵 ) )
10 0fin ⊢ ∅ ∈ Fin
11 10 a1i ⊢ ( 𝜑 → ∅ ∈ Fin )
12 eqid ⊢ dom ( voln ‘ ∅ ) = dom ( voln ‘ ∅ )
13 noel ⊢ ¬ 𝑘 ∈ ∅
14 13 pm2.21i ⊢ ( 𝑘 ∈ ∅ → 𝐴 ∈ ℝ )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∅ ) → 𝐴 ∈ ℝ )
16 13 pm2.21i ⊢ ( 𝑘 ∈ ∅ → 𝐵 ∈ ℝ )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∅ ) → 𝐵 ∈ ℝ )
18 1 11 12 15 17 hoimbl2 ⊢ ( 𝜑 → X 𝑘 ∈ ∅ ( 𝐴 [,) 𝐵 ) ∈ dom ( voln ‘ ∅ ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → X 𝑘 ∈ ∅ ( 𝐴 [,) 𝐵 ) ∈ dom ( voln ‘ ∅ ) )
20 9 19 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ∈ dom ( voln ‘ ∅ ) )
21 20 von0val ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln ‘ ∅ ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) = 0 )
22 7 21 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) = 0 )
23 0red ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 0 ∈ ℝ )
24 22 23 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )
25 neqne ⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
26 25 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
27 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → 𝑗 ∈ 𝑋 )
28 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑋
29 1 28 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑋 )
30 nfcv ⊢ Ⅎ 𝑘 𝑗
31 30 nfcsb1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴
32 31 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ
33 29 32 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ )
34 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑋 ↔ 𝑗 ∈ 𝑋 ) )
35 34 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) ) )
36 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐴 = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
37 36 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ ) )
38 35 37 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ ) ) )
39 33 38 3 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ )
40 eqid ⊢ ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑘 ∈ 𝑋 ↦ 𝐴 )
41 30 31 36 40 fvmptf ⊢ ( ( 𝑗 ∈ 𝑋 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
42 27 39 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
43 30 nfcsb1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
44 nfcv ⊢ Ⅎ 𝑘 ℝ
45 43 44 nfel ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ
46 29 45 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ )
47 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
48 47 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℝ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) )
49 35 48 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) ) )
50 46 49 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ )
51 eqid ⊢ ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑘 ∈ 𝑋 ↦ 𝐵 )
52 30 43 47 51 fvmptf ⊢ ( ( 𝑗 ∈ 𝑋 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
53 27 50 52 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
54 42 53 oveq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
55 54 ixpeq2dva ⊢ ( 𝜑 → X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) = X 𝑗 ∈ 𝑋 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
56 nfcv ⊢ Ⅎ 𝑗 ( 𝐴 [,) 𝐵 )
57 nfcv ⊢ Ⅎ 𝑘 [,)
58 31 57 43 nfov ⊢ Ⅎ 𝑘 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
59 36 47 oveq12d ⊢ ( 𝑘 = 𝑗 → ( 𝐴 [,) 𝐵 ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
60 56 58 59 cbvixp ⊢ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) = X 𝑗 ∈ 𝑋 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
61 60 eqcomi ⊢ X 𝑗 ∈ 𝑋 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) = X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 )
62 61 a1i ⊢ ( 𝜑 → X 𝑗 ∈ 𝑋 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) = X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) )
63 55 62 eqtr2d ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) = X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) )
64 63 fveq2d ⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) = ( ( voln ‘ 𝑋 ) ‘ X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) = ( ( voln ‘ 𝑋 ) ‘ X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) )
66 2 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ∈ Fin )
67 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ≠ ∅ )
68 1 3 40 fmptdf ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℝ )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℝ )
70 1 4 51 fmptdf ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℝ )
71 70 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℝ )
72 eqid ⊢ X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) = X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) )
73 66 67 69 71 72 vonn0hoi ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ( voln ‘ 𝑋 ) ‘ X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) = ∏ 𝑗 ∈ 𝑋 ( vol ‘ ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) )
74 65 73 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) = ∏ 𝑗 ∈ 𝑋 ( vol ‘ ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) )
75 42 39 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) ∈ ℝ )
76 53 50 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ∈ ℝ )
77 volicore ⊢ ( ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) ∈ ℝ ∧ ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ∈ ℝ ) → ( vol ‘ ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) ∈ ℝ )
78 75 76 77 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( vol ‘ ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) ∈ ℝ )
79 2 78 fprodrecl ⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝑋 ( vol ‘ ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) ∈ ℝ )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∏ 𝑗 ∈ 𝑋 ( vol ‘ ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) ∈ ℝ )
81 74 80 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )
82 26 81 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )
83 24 82 pm2.61dan ⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )