Theorem hoidmv0val

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

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

Proof

Step	Hyp	Ref	Expression
1		hoidmv0val.l	⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
2		hoidmv0val.a	⊢ ( 𝜑 → 𝐴 : ∅ ⟶ ℝ )
3		hoidmv0val.b	⊢ ( 𝜑 → 𝐵 : ∅ ⟶ ℝ )
4		0fin	⊢ ∅ ∈ Fin
5	4	a1i	⊢ ( 𝜑 → ∅ ∈ Fin )
6	1 2 3 5	hoidmvval	⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ ∅ ) 𝐵 ) = if ( ∅ = ∅ , 0 , ∏ 𝑘 ∈ ∅ ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
7		eqid	⊢ ∅ = ∅
8		iftrue	⊢ ( ∅ = ∅ → if ( ∅ = ∅ , 0 , ∏ 𝑘 ∈ ∅ ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) = 0 )
9	7 8	ax-mp	⊢ if ( ∅ = ∅ , 0 , ∏ 𝑘 ∈ ∅ ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) = 0
10	9	a1i	⊢ ( 𝜑 → if ( ∅ = ∅ , 0 , ∏ 𝑘 ∈ ∅ ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) = 0 )
11	6 10	eqtrd	⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ ∅ ) 𝐵 ) = 0 )