Theorem vonn0icc

Description: The n-dimensional Lebesgue measure of a closed interval, when the dimension of the space is nonzero. This is the second statement in Proposition 115G (d) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonn0icc.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	vonn0icc.n	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
	vonn0icc.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
	vonn0icc.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
	vonn0icc.i	⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐵 ‘ 𝑘 ) )
Assertion	vonn0icc	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐵 ‘ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		vonn0icc.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		vonn0icc.n	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3		vonn0icc.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
4		vonn0icc.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
5		vonn0icc.i	⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐵 ‘ 𝑘 ) )
6		fveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑎 ‘ 𝑗 ) = ( 𝑎 ‘ 𝑘 ) )
7		fveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑏 ‘ 𝑗 ) = ( 𝑏 ‘ 𝑘 ) )
8	6 7	oveq12d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) = ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) )
9	8	fveq2d	⊢ ( 𝑗 = 𝑘 → ( vol ‘ ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) ) = ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) )
10	9	cbvprodv	⊢ ∏ 𝑗 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) ) = ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) )
11		ifeq2	⊢ ( ∏ 𝑗 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) ) = ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) → if ( 𝑥 = ∅ , 0 , ∏ 𝑗 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) ) ) = if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) )
12	10 11	ax-mp	⊢ if ( 𝑥 = ∅ , 0 , ∏ 𝑗 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) ) ) = if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) )
13	12	a1i	⊢ ( ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) ∧ 𝑏 ∈ ( ℝ ↑m 𝑥 ) ) → if ( 𝑥 = ∅ , 0 , ∏ 𝑗 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) ) ) = if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) )
14	13	mpoeq3ia	⊢ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑗 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) ) ) ) = ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) )
15	14	mpteq2i	⊢ ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑗 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) ) ) ) ) = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
16	1 3 4 5 15	vonicc	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑗 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) ) ) ) ) ‘ 𝑋 ) 𝐵 ) )
17	15	fveq1i	⊢ ( ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑗 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) ) ) ) ) ‘ 𝑋 ) = ( ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑋 )
18	17	oveqi	⊢ ( 𝐴 ( ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑗 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) ) ) ) ) ‘ 𝑋 ) 𝐵 ) = ( 𝐴 ( ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑋 ) 𝐵 )
19	18	a1i	⊢ ( 𝜑 → ( 𝐴 ( ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑗 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑗 ) [,) ( 𝑏 ‘ 𝑗 ) ) ) ) ) ) ‘ 𝑋 ) 𝐵 ) = ( 𝐴 ( ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑋 ) 𝐵 ) )
20	16 19	eqtrd	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑋 ) 𝐵 ) )
21		eqid	⊢ ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
22	21 1 2 3 4	hoidmvn0val	⊢ ( 𝜑 → ( 𝐴 ( ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
23	3	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
24	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
25	23 24	voliccico	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
26	25	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐵 ‘ 𝑘 ) ) ) )
27	26	prodeq2dv	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐵 ‘ 𝑘 ) ) ) )
28	20 22 27	3eqtrd	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐵 ‘ 𝑘 ) ) ) )