Metamath Proof Explorer

Theorem hoidmvval

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

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

Proof

Step Hyp Ref Expression
1 hoidmvval.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
2 hoidmvval.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
3 hoidmvval.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
4 hoidmvval.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
5 oveq2 ⊢ ( 𝑥 = 𝑋 → ( ℝ ↑m 𝑥 ) = ( ℝ ↑m 𝑋 ) )
6 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ∅ ↔ 𝑋 = ∅ ) )
7 prodeq1 ⊢ ( 𝑥 = 𝑋 → ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) )
8 6 7 ifbieq2d ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) = if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) )
9 5 5 8 mpoeq123dv ⊢ ( 𝑥 = 𝑋 → ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) = ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) , 𝑏 ∈ ( ℝ ↑m 𝑋 ) ↦ if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
10 ovex ⊢ ( ℝ ↑m 𝑋 ) ∈ V
11 10 10 mpoex ⊢ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) , 𝑏 ∈ ( ℝ ↑m 𝑋 ) ↦ if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ∈ V
12 11 a1i ⊢ ( 𝜑 → ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) , 𝑏 ∈ ( ℝ ↑m 𝑋 ) ↦ if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ∈ V )
13 1 9 4 12 fvmptd3 ⊢ ( 𝜑 → ( 𝐿 ‘ 𝑋 ) = ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) , 𝑏 ∈ ( ℝ ↑m 𝑋 ) ↦ if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
14 fveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
15 14 adantr ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
16 fveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
17 16 adantl ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑏 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
18 15 17 oveq12d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
19 18 fveq2d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
20 19 prodeq2ad ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
21 20 ifeq2d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) = if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
22 21 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) = if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
23 reex ⊢ ℝ ∈ V
24 23 a1i ⊢ ( 𝜑 → ℝ ∈ V )
25 elmapg ⊢ ( ( ℝ ∈ V ∧ 𝑋 ∈ Fin ) → ( 𝐴 ∈ ( ℝ ↑m 𝑋 ) ↔ 𝐴 : 𝑋 ⟶ ℝ ) )
26 24 4 25 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∈ ( ℝ ↑m 𝑋 ) ↔ 𝐴 : 𝑋 ⟶ ℝ ) )
27 2 26 mpbird ⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m 𝑋 ) )
28 elmapg ⊢ ( ( ℝ ∈ V ∧ 𝑋 ∈ Fin ) → ( 𝐵 ∈ ( ℝ ↑m 𝑋 ) ↔ 𝐵 : 𝑋 ⟶ ℝ ) )
29 24 4 28 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( ℝ ↑m 𝑋 ) ↔ 𝐵 : 𝑋 ⟶ ℝ ) )
30 3 29 mpbird ⊢ ( 𝜑 → 𝐵 ∈ ( ℝ ↑m 𝑋 ) )
31 c0ex ⊢ 0 ∈ V
32 prodex ⊢ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ V
33 31 32 ifex ⊢ if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) ∈ V
34 33 a1i ⊢ ( 𝜑 → if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) ∈ V )
35 13 22 27 30 34 ovmpod ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )