Theorem hoidmvcl

Description: The dimensional volume of a multidimensional half-open interval is a nonnegative real. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hoidmvcl.l	⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
	hoidmvcl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	hoidmvcl.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
	hoidmvcl.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
Assertion	hoidmvcl	⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ∈ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		hoidmvcl.l	⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
2		hoidmvcl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		hoidmvcl.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
4		hoidmvcl.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
5	1 3 4 2	hoidmvval	⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
6		0e0icopnf	⊢ 0 ∈ ( 0 [,) +∞ )
7	6	a1i	⊢ ( 𝜑 → 0 ∈ ( 0 [,) +∞ ) )
8		0xr	⊢ 0 ∈ ℝ*
9	8	a1i	⊢ ( 𝜑 → 0 ∈ ℝ* )
10		pnfxr	⊢ +∞ ∈ ℝ*
11	10	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
12	3	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
13	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
14		volico	⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) )
15	12 13 14	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) )
16	13 12	resubcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
17		0red	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 0 ∈ ℝ )
18	16 17	ifcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) ∈ ℝ )
19	15 18	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
20	2 19	fprodrecl	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
21	20	rexrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ* )
22		nfv	⊢ Ⅎ 𝑘 𝜑
23	13	rexrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* )
24		icombl	⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ* ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ∈ dom vol )
25	12 23 24	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ∈ dom vol )
26		volge0	⊢ ( ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ∈ dom vol → 0 ≤ ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
27	25 26	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 0 ≤ ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
28	22 2 19 27	fprodge0	⊢ ( 𝜑 → 0 ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
29	20	ltpnfd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) < +∞ )
30	9 11 21 28 29	elicod	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ( 0 [,) +∞ ) )
31	7 30	ifcld	⊢ ( 𝜑 → if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) ∈ ( 0 [,) +∞ ) )
32	5 31	eqeltrd	⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ∈ ( 0 [,) +∞ ) )