Metamath Proof Explorer

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 ⊢ φ → X ∈ Fin
vonn0icc.n ⊢ φ → X ≠ ∅
vonn0icc.a ⊢ φ → A : X ⟶ ℝ
vonn0icc.b ⊢ φ → B : X ⟶ ℝ
vonn0icc.i ⊢ I = ⨉ k ∈ X A ⁡ k B ⁡ k
Assertion vonn0icc ⊢ φ → voln ⁡ X ⁡ I = ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k

Proof

Step Hyp Ref Expression
1 vonn0icc.x ⊢ φ → X ∈ Fin
2 vonn0icc.n ⊢ φ → X ≠ ∅
3 vonn0icc.a ⊢ φ → A : X ⟶ ℝ
4 vonn0icc.b ⊢ φ → B : X ⟶ ℝ
5 vonn0icc.i ⊢ I = ⨉ k ∈ X A ⁡ k B ⁡ k
6 fveq2 ⊢ j = k → a ⁡ j = a ⁡ k
7 fveq2 ⊢ j = k → b ⁡ j = b ⁡ k
8 6 7 oveq12d ⊢ j = k → a ⁡ j b ⁡ j = a ⁡ k b ⁡ k
9 8 fveq2d ⊢ j = k → vol ⁡ a ⁡ j b ⁡ j = vol ⁡ a ⁡ k b ⁡ k
10 9 cbvprodv ⊢ ∏ j ∈ x vol ⁡ a ⁡ j b ⁡ j = ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
11 ifeq2 ⊢ ∏ j ∈ x vol ⁡ a ⁡ j b ⁡ j = ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k → if x = ∅ 0 ∏ j ∈ x vol ⁡ a ⁡ j b ⁡ j = if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
12 10 11 ax-mp ⊢ if x = ∅ 0 ∏ j ∈ x vol ⁡ a ⁡ j b ⁡ j = if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
13 12 a1i ⊢ a ∈ ℝ x ∧ b ∈ ℝ x → if x = ∅ 0 ∏ j ∈ x vol ⁡ a ⁡ j b ⁡ j = if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
14 13 mpoeq3ia ⊢ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ j ∈ x vol ⁡ a ⁡ j b ⁡ j = a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
15 14 mpteq2i ⊢ x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ j ∈ x vol ⁡ a ⁡ j b ⁡ j = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
16 1 3 4 5 15 vonicc ⊢ φ → voln ⁡ X ⁡ I = A x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ j ∈ x vol ⁡ a ⁡ j b ⁡ j ⁡ X B
17 15 fveq1i ⊢ x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ j ∈ x vol ⁡ a ⁡ j b ⁡ j ⁡ X = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k ⁡ X
18 17 oveqi ⊢ A x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ j ∈ x vol ⁡ a ⁡ j b ⁡ j ⁡ X B = A x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k ⁡ X B
19 18 a1i ⊢ φ → A x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ j ∈ x vol ⁡ a ⁡ j b ⁡ j ⁡ X B = A x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k ⁡ X B
20 16 19 eqtrd ⊢ φ → voln ⁡ X ⁡ I = A x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k ⁡ X B
21 eqid ⊢ x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
22 21 1 2 3 4 hoidmvn0val ⊢ φ → A x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k ⁡ X B = ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k
23 3 ffvelcdmda ⊢ φ ∧ k ∈ X → A ⁡ k ∈ ℝ
24 4 ffvelcdmda ⊢ φ ∧ k ∈ X → B ⁡ k ∈ ℝ
25 23 24 voliccico ⊢ φ ∧ k ∈ X → vol ⁡ A ⁡ k B ⁡ k = vol ⁡ A ⁡ k B ⁡ k
26 25 eqcomd ⊢ φ ∧ k ∈ X → vol ⁡ A ⁡ k B ⁡ k = vol ⁡ A ⁡ k B ⁡ k
27 26 prodeq2dv ⊢ φ → ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k = ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k
28 20 22 27 3eqtrd ⊢ φ → voln ⁡ X ⁡ I = ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k