Theorem hoidmvn0val

Description: The dimensional volume of a non-0-dimensional half-open interval. Definition 115A (c) of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

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

Proof

Step	Hyp	Ref	Expression
1		hoidmvn0val.l	⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
2		hoidmvn0val.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		hoidmvn0val.n	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
4		hoidmvn0val.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
5		hoidmvn0val.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
6	1 4 5 2	hoidmvval	⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
7	3	neneqd	⊢ ( 𝜑 → ¬ 𝑋 = ∅ )
8	7	iffalsed	⊢ ( 𝜑 → if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
9	6 8	eqtrd	⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )