Metamath Proof Explorer

Theorem sge0hsphoire

Description: If the generalized sum of dimensional volumes of n-dimensional half-open intervals is finite, then the sum stays finite if every half-open interval is intersected with a half-space. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses sge0hsphoire.l ⊢L=x∈Fin⟼a∈ℝx,b∈ℝx⟼ifx=∅0∏k∈xvol⁡a⁡kb⁡k
sge0hsphoire.f ⊢φ→Y∈Fin
sge0hsphoire.z ⊢φ→Z∈W∖Y
sge0hsphoire.w ⊢W=Y∪Z
sge0hsphoire.c ⊢φ→C:ℕ⟶ℝW
sge0hsphoire.d ⊢φ→D:ℕ⟶ℝW
sge0hsphoire.r ⊢φ→sum^⁡j∈ℕ⟼C⁡jL⁡WD⁡j∈ℝ
sge0hsphoire.h ⊢H=x∈ℝ⟼c∈ℝW⟼j∈W⟼ifj∈Yc⁡jifc⁡j≤xc⁡jx
sge0hsphoire.s ⊢φ→S∈ℝ
Assertion sge0hsphoire ⊢φ→sum^⁡j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j∈ℝ

Proof

Step Hyp Ref Expression
1 sge0hsphoire.l ⊢L=x∈Fin⟼a∈ℝx,b∈ℝx⟼ifx=∅0∏k∈xvol⁡a⁡kb⁡k
2 sge0hsphoire.f ⊢φ→Y∈Fin
3 sge0hsphoire.z ⊢φ→Z∈W∖Y
4 sge0hsphoire.w ⊢W=Y∪Z
5 sge0hsphoire.c ⊢φ→C:ℕ⟶ℝW
6 sge0hsphoire.d ⊢φ→D:ℕ⟶ℝW
7 sge0hsphoire.r ⊢φ→sum^⁡j∈ℕ⟼C⁡jL⁡WD⁡j∈ℝ
8 sge0hsphoire.h ⊢H=x∈ℝ⟼c∈ℝW⟼j∈W⟼ifj∈Yc⁡jifc⁡j≤xc⁡jx
9 sge0hsphoire.s ⊢φ→S∈ℝ
10 nnex ⊢ℕ∈V
11 10 a1i ⊢φ→ℕ∈V
12 snfi ⊢Z∈Fin
13 12 a1i ⊢φ→Z∈Fin
14 unfi ⊢Y∈Fin∧Z∈Fin→Y∪Z∈Fin
15 2 13 14 syl2anc ⊢φ→Y∪Z∈Fin
16 4 15 eqeltrid ⊢φ→W∈Fin
17 16 adantr ⊢φ∧j∈ℕ→W∈Fin
18 5 ffvelcdmda ⊢φ∧j∈ℕ→C⁡j∈ℝW
19 elmapi ⊢C⁡j∈ℝW→C⁡j:W⟶ℝ
20 18 19 syl ⊢φ∧j∈ℕ→C⁡j:W⟶ℝ
21 eleq1w ⊢j=h→j∈Y↔h∈Y
22 fveq2 ⊢j=h→c⁡j=c⁡h
23 22 breq1d ⊢j=h→c⁡j≤x↔c⁡h≤x
24 23 22 ifbieq1d ⊢j=h→ifc⁡j≤xc⁡jx=ifc⁡h≤xc⁡hx
25 21 22 24 ifbieq12d ⊢j=h→ifj∈Yc⁡jifc⁡j≤xc⁡jx=ifh∈Yc⁡hifc⁡h≤xc⁡hx
26 25 cbvmptv ⊢j∈W⟼ifj∈Yc⁡jifc⁡j≤xc⁡jx=h∈W⟼ifh∈Yc⁡hifc⁡h≤xc⁡hx
27 26 mpteq2i ⊢c∈ℝW⟼j∈W⟼ifj∈Yc⁡jifc⁡j≤xc⁡jx=c∈ℝW⟼h∈W⟼ifh∈Yc⁡hifc⁡h≤xc⁡hx
28 27 mpteq2i ⊢x∈ℝ⟼c∈ℝW⟼j∈W⟼ifj∈Yc⁡jifc⁡j≤xc⁡jx=x∈ℝ⟼c∈ℝW⟼h∈W⟼ifh∈Yc⁡hifc⁡h≤xc⁡hx
29 8 28 eqtri ⊢H=x∈ℝ⟼c∈ℝW⟼h∈W⟼ifh∈Yc⁡hifc⁡h≤xc⁡hx
30 9 adantr ⊢φ∧j∈ℕ→S∈ℝ
31 6 ffvelcdmda ⊢φ∧j∈ℕ→D⁡j∈ℝW
32 elmapi ⊢D⁡j∈ℝW→D⁡j:W⟶ℝ
33 31 32 syl ⊢φ∧j∈ℕ→D⁡j:W⟶ℝ
34 29 30 17 33 hsphoif ⊢φ∧j∈ℕ→H⁡S⁡D⁡j:W⟶ℝ
35 1 17 20 34 hoidmvcl ⊢φ∧j∈ℕ→C⁡jL⁡WH⁡S⁡D⁡j∈0+∞
36 eqid ⊢j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j=j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j
37 35 36 fmptd ⊢φ→j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j:ℕ⟶0+∞
38 icossicc ⊢0+∞⊆0+∞
39 38 a1i ⊢φ→0+∞⊆0+∞
40 37 39 fssd ⊢φ→j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j:ℕ⟶0+∞
41 11 40 sge0cl ⊢φ→sum^⁡j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j∈0+∞
42 11 40 sge0xrcl ⊢φ→sum^⁡j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j∈ℝ*
43 pnfxr ⊢+∞∈ℝ*
44 43 a1i ⊢φ→+∞∈ℝ*
45 7 rexrd ⊢φ→sum^⁡j∈ℕ⟼C⁡jL⁡WD⁡j∈ℝ*
46 nfv ⊢Ⅎjφ
47 38 35 sselid ⊢φ∧j∈ℕ→C⁡jL⁡WH⁡S⁡D⁡j∈0+∞
48 1 17 20 33 hoidmvcl ⊢φ∧j∈ℕ→C⁡jL⁡WD⁡j∈0+∞
49 38 48 sselid ⊢φ∧j∈ℕ→C⁡jL⁡WD⁡j∈0+∞
50 3 adantr ⊢φ∧j∈ℕ→Z∈W∖Y
51 1 17 50 4 30 29 20 33 hsphoidmvle ⊢φ∧j∈ℕ→C⁡jL⁡WH⁡S⁡D⁡j≤C⁡jL⁡WD⁡j
52 46 11 47 49 51 sge0lempt ⊢φ→sum^⁡j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j≤sum^⁡j∈ℕ⟼C⁡jL⁡WD⁡j
53 7 ltpnfd ⊢φ→sum^⁡j∈ℕ⟼C⁡jL⁡WD⁡j<+∞
54 42 45 44 52 53 xrlelttrd ⊢φ→sum^⁡j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j<+∞
55 42 44 54 xrltned ⊢φ→sum^⁡j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j≠+∞
56 ge0xrre ⊢sum^⁡j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j∈0+∞∧sum^⁡j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j≠+∞→sum^⁡j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j∈ℝ
57 41 55 56 syl2anc ⊢φ→sum^⁡j∈ℕ⟼C⁡jL⁡WH⁡S⁡D⁡j∈ℝ