Theorem hoiprodcl2

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

	Ref	Expression
Hypotheses	hoiprodcl2.kph	⊢ Ⅎ 𝑘 𝜑
	hoiprodcl2.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	hoiprodcl2.l	⊢ 𝐿 = ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) )
	hoiprodcl2.i	⊢ ( 𝜑 → 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
Assertion	hoiprodcl2	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐼 ) ∈ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		hoiprodcl2.kph	⊢ Ⅎ 𝑘 𝜑
2		hoiprodcl2.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		hoiprodcl2.l	⊢ 𝐿 = ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) )
4		hoiprodcl2.i	⊢ ( 𝜑 → 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
5		coeq2	⊢ ( 𝑖 = 𝐼 → ( [,) ∘ 𝑖 ) = ( [,) ∘ 𝐼 ) )
6	5	fveq1d	⊢ ( 𝑖 = 𝐼 → ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) = ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) )
7	6	fveq2d	⊢ ( 𝑖 = 𝐼 → ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) )
8	7	ralrimivw	⊢ ( 𝑖 = 𝐼 → ∀ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) )
9	8	prodeq2d	⊢ ( 𝑖 = 𝐼 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) )
10		reex	⊢ ℝ ∈ V
11	10 10	xpex	⊢ ( ℝ × ℝ ) ∈ V
12	11	a1i	⊢ ( 𝜑 → ( ℝ × ℝ ) ∈ V )
13	12 2	jca	⊢ ( 𝜑 → ( ( ℝ × ℝ ) ∈ V ∧ 𝑋 ∈ Fin ) )
14		elmapg	⊢ ( ( ( ℝ × ℝ ) ∈ V ∧ 𝑋 ∈ Fin ) → ( 𝐼 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↔ 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) ) )
15	13 14	syl	⊢ ( 𝜑 → ( 𝐼 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↔ 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) ) )
16	4 15	mpbird	⊢ ( 𝜑 → 𝐼 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
17	1 2 4	hoiprodcl	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )
18	3 9 16 17	fvmptd3	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐼 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) )
19	18 17	eqeltrd	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐼 ) ∈ ( 0 [,) +∞ ) )