Metamath Proof Explorer

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 ⊢ L = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
hoidmv0val.a ⊢ φ → A : ∅ ⟶ ℝ
hoidmv0val.b ⊢ φ → B : ∅ ⟶ ℝ
Assertion hoidmv0val ⊢ φ → A L ⁡ ∅ B = 0

Proof

Step Hyp Ref Expression
1 hoidmv0val.l ⊢ L = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
2 hoidmv0val.a ⊢ φ → A : ∅ ⟶ ℝ
3 hoidmv0val.b ⊢ φ → B : ∅ ⟶ ℝ
4 0fin ⊢ ∅ ∈ Fin
5 4 a1i ⊢ φ → ∅ ∈ Fin
6 1 2 3 5 hoidmvval ⊢ φ → A L ⁡ ∅ B = if ∅ = ∅ 0 ∏ k ∈ ∅ vol ⁡ A ⁡ k B ⁡ k
7 eqid ⊢ ∅ = ∅
8 iftrue ⊢ ∅ = ∅ → if ∅ = ∅ 0 ∏ k ∈ ∅ vol ⁡ A ⁡ k B ⁡ k = 0
9 7 8 ax-mp ⊢ if ∅ = ∅ 0 ∏ k ∈ ∅ vol ⁡ A ⁡ k B ⁡ k = 0
10 9 a1i ⊢ φ → if ∅ = ∅ 0 ∏ k ∈ ∅ vol ⁡ A ⁡ k B ⁡ k = 0
11 6 10 eqtrd ⊢ φ → A L ⁡ ∅ B = 0