hoiprodcl

Description: The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	hoiprodcl.1	⊢ Ⅎ 𝑘 𝜑
	hoiprodcl.2	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	hoiprodcl.3	⊢ ( 𝜑 → 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
Assertion	hoiprodcl	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		hoiprodcl.1	⊢ Ⅎ 𝑘 𝜑
2		hoiprodcl.2	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		hoiprodcl.3	⊢ ( 𝜑 → 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
4		0xr	⊢ 0 ∈ ℝ^*
5	4	a1i	⊢ ( 𝜑 → 0 ∈ ℝ^* )
6		pnfxr	⊢ +∞ ∈ ℝ^*
7	6	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ^* )
8	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
9		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
10	8 9	fvovco	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = ( ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) ) )
11	10	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) = ( vol ‘ ( ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) ) ) )
12	3	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐼 ‘ 𝑘 ) ∈ ( ℝ × ℝ ) )
13		xp1st	⊢ ( ( 𝐼 ‘ 𝑘 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ )
14	12 13	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ )
15		xp2nd	⊢ ( ( 𝐼 ‘ 𝑘 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ )
16	12 15	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ )
17		volico	⊢ ( ( ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ‘ ( ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) ) ) = if ( ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) , ( ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) ) , 0 ) )
18	14 16 17	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) ) ) = if ( ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) , ( ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) ) , 0 ) )
19	11 18	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) = if ( ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) , ( ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) ) , 0 ) )
20	16 14	resubcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) ) ∈ ℝ )
21		0red	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 0 ∈ ℝ )
22	20 21	ifcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → if ( ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) , ( ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) ) , 0 ) ∈ ℝ )
23	19 22	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) ∈ ℝ )
24	1 2 23	fprodreclf	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) ∈ ℝ )
25	24	rexrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) ∈ ℝ^* )
26	16	rexrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ^* )
27		icombl	⊢ ( ( ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ^* ) → ( ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) ) ∈ dom vol )
28	14 26 27	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 1^st ‘ ( 𝐼 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐼 ‘ 𝑘 ) ) ) ∈ dom vol )
29	10 28	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ∈ dom vol )
30		volge0	⊢ ( ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ∈ dom vol → 0 ≤ ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) )
31	29 30	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 0 ≤ ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) )
32	1 2 23 31	fprodge0	⊢ ( 𝜑 → 0 ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) )
33	24	ltpnfd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) < +∞ )
34	5 7 25 32 33	elicod	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )

Metamath Proof Explorer

Theorem hoiprodcl

Proof