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	⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
	sge0hsphoire.f	⊢ ( 𝜑 → 𝑌 ∈ Fin )
	sge0hsphoire.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 ∖ 𝑌 ) )
	sge0hsphoire.w	⊢ 𝑊 = ( 𝑌 ∪ { 𝑍 } )
	sge0hsphoire.c	⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
	sge0hsphoire.d	⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
	sge0hsphoire.r	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
	sge0hsphoire.h	⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) )
	sge0hsphoire.s	⊢ ( 𝜑 → 𝑆 ∈ ℝ )
Assertion	sge0hsphoire	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		sge0hsphoire.l	⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
2		sge0hsphoire.f	⊢ ( 𝜑 → 𝑌 ∈ Fin )
3		sge0hsphoire.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 ∖ 𝑌 ) )
4		sge0hsphoire.w	⊢ 𝑊 = ( 𝑌 ∪ { 𝑍 } )
5		sge0hsphoire.c	⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
6		sge0hsphoire.d	⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
7		sge0hsphoire.r	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
8		sge0hsphoire.h	⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) )
9		sge0hsphoire.s	⊢ ( 𝜑 → 𝑆 ∈ ℝ )
10		nnex	⊢ ℕ ∈ V
11	10	a1i	⊢ ( 𝜑 → ℕ ∈ V )
12		snfi	⊢ { 𝑍 } ∈ Fin
13	12	a1i	⊢ ( 𝜑 → { 𝑍 } ∈ Fin )
14		unfi	⊢ ( ( 𝑌 ∈ Fin ∧ { 𝑍 } ∈ Fin ) → ( 𝑌 ∪ { 𝑍 } ) ∈ Fin )
15	2 13 14	syl2anc	⊢ ( 𝜑 → ( 𝑌 ∪ { 𝑍 } ) ∈ Fin )
16	4 15	eqeltrid	⊢ ( 𝜑 → 𝑊 ∈ Fin )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑊 ∈ Fin )
18	5	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
19		elmapi	⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
20	18 19	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
21		eleq1w	⊢ ( 𝑗 = ℎ → ( 𝑗 ∈ 𝑌 ↔ ℎ ∈ 𝑌 ) )
22		fveq2	⊢ ( 𝑗 = ℎ → ( 𝑐 ‘ 𝑗 ) = ( 𝑐 ‘ ℎ ) )
23	22	breq1d	⊢ ( 𝑗 = ℎ → ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝑐 ‘ ℎ ) ≤ 𝑥 ) )
24	23 22	ifbieq1d	⊢ ( 𝑗 = ℎ → if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) = if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) )
25	21 22 24	ifbieq12d	⊢ ( 𝑗 = ℎ → if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) = if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) )
26	25	cbvmptv	⊢ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) = ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) )
27	26	mpteq2i	⊢ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) )
28	27	mpteq2i	⊢ ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) ) )
29	8 28	eqtri	⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) ) )
30	9	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑆 ∈ ℝ )
31	6	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
32		elmapi	⊢ ( ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
33	31 32	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
34	29 30 17 33	hsphoif	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) : 𝑊 ⟶ ℝ )
35	1 17 20 34	hoidmvcl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
36		eqid	⊢ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
37	35 36	fmptd	⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
38		icossicc	⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
39	38	a1i	⊢ ( 𝜑 → ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) )
40	37 39	fssd	⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
41	11 40	sge0cl	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
42	11 40	sge0xrcl	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ* )
43		pnfxr	⊢ +∞ ∈ ℝ*
44	43	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
45	7	rexrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
46		nfv	⊢ Ⅎ 𝑗 𝜑
47	38 35	sseldi	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
48	1 17 20 33	hoidmvcl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,) +∞ ) )
49	38 48	sseldi	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) )
50	3	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑍 ∈ ( 𝑊 ∖ 𝑌 ) )
51	1 17 50 4 30 29 20 33	hsphoidmvle	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) )
52	46 11 47 49 51	sge0lempt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
53	7	ltpnfd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) < +∞ )
54	42 45 44 52 53	xrlelttrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) < +∞ )
55	42 44 54	xrltned	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≠ +∞ )
56		ge0xrre	⊢ ( ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
57	41 55 56	syl2anc	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )