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 ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ 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 ⁡ j L ⁡ W D ⁡ j ∈ ℝ
sge0hsphoire.h ⊢ H = x ∈ ℝ ⟼ c ∈ ℝ W ⟼ j ∈ W ⟼ if j ∈ Y c ⁡ j if c ⁡ j ≤ x c ⁡ j x
sge0hsphoire.s ⊢ φ → S ∈ ℝ
Assertion sge0hsphoire ⊢ φ → sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j ∈ ℝ

Proof

Step Hyp Ref Expression
1 sge0hsphoire.l ⊢ L = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ 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 ⁡ j L ⁡ W D ⁡ j ∈ ℝ
8 sge0hsphoire.h ⊢ H = x ∈ ℝ ⟼ c ∈ ℝ W ⟼ j ∈ W ⟼ if j ∈ Y c ⁡ j if c ⁡ j ≤ x c ⁡ j x
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 → if c ⁡ j ≤ x c ⁡ j x = if c ⁡ h ≤ x c ⁡ h x
25 21 22 24 ifbieq12d ⊢ j = h → if j ∈ Y c ⁡ j if c ⁡ j ≤ x c ⁡ j x = if h ∈ Y c ⁡ h if c ⁡ h ≤ x c ⁡ h x
26 25 cbvmptv ⊢ j ∈ W ⟼ if j ∈ Y c ⁡ j if c ⁡ j ≤ x c ⁡ j x = h ∈ W ⟼ if h ∈ Y c ⁡ h if c ⁡ h ≤ x c ⁡ h x
27 26 mpteq2i ⊢ c ∈ ℝ W ⟼ j ∈ W ⟼ if j ∈ Y c ⁡ j if c ⁡ j ≤ x c ⁡ j x = c ∈ ℝ W ⟼ h ∈ W ⟼ if h ∈ Y c ⁡ h if c ⁡ h ≤ x c ⁡ h x
28 27 mpteq2i ⊢ x ∈ ℝ ⟼ c ∈ ℝ W ⟼ j ∈ W ⟼ if j ∈ Y c ⁡ j if c ⁡ j ≤ x c ⁡ j x = x ∈ ℝ ⟼ c ∈ ℝ W ⟼ h ∈ W ⟼ if h ∈ Y c ⁡ h if c ⁡ h ≤ x c ⁡ h x
29 8 28 eqtri ⊢ H = x ∈ ℝ ⟼ c ∈ ℝ W ⟼ h ∈ W ⟼ if h ∈ Y c ⁡ h if c ⁡ h ≤ x c ⁡ h x
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 ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j ∈ 0 +∞
36 eqid ⊢ j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j = j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j
37 35 36 fmptd ⊢ φ → j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j : ℕ ⟶ 0 +∞
38 icossicc ⊢ 0 +∞ ⊆ 0 +∞
39 38 a1i ⊢ φ → 0 +∞ ⊆ 0 +∞
40 37 39 fssd ⊢ φ → j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j : ℕ ⟶ 0 +∞
41 11 40 sge0cl ⊢ φ → sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j ∈ 0 +∞
42 11 40 sge0xrcl ⊢ φ → sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j ∈ ℝ *
43 pnfxr ⊢ +∞ ∈ ℝ *
44 43 a1i ⊢ φ → +∞ ∈ ℝ *
45 7 rexrd ⊢ φ → sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W D ⁡ j ∈ ℝ *
46 nfv ⊢ Ⅎ j φ
47 38 35 sselid ⊢ φ ∧ j ∈ ℕ → C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j ∈ 0 +∞
48 1 17 20 33 hoidmvcl ⊢ φ ∧ j ∈ ℕ → C ⁡ j L ⁡ W D ⁡ j ∈ 0 +∞
49 38 48 sselid ⊢ φ ∧ j ∈ ℕ → C ⁡ j L ⁡ W D ⁡ j ∈ 0 +∞
50 3 adantr ⊢ φ ∧ j ∈ ℕ → Z ∈ W ∖ Y
51 1 17 50 4 30 29 20 33 hsphoidmvle ⊢ φ ∧ j ∈ ℕ → C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j ≤ C ⁡ j L ⁡ W D ⁡ j
52 46 11 47 49 51 sge0lempt ⊢ φ → sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W D ⁡ j
53 7 ltpnfd ⊢ φ → sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W D ⁡ j < +∞
54 42 45 44 52 53 xrlelttrd ⊢ φ → sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j < +∞
55 42 44 54 xrltned ⊢ φ → sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j ≠ +∞
56 ge0xrre ⊢ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j ∈ 0 +∞ ∧ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j ≠ +∞ → sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j ∈ ℝ
57 41 55 56 syl2anc ⊢ φ → sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ W H ⁡ S ⁡ D ⁡ j ∈ ℝ