Metamath Proof Explorer

Theorem hoiprodp1

Description: The dimensional volume of a half-open interval with dimension n + 1 . Used in the first equality of step (e) of Lemma 115B of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoiprodp1.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
hoiprodp1.y ⊢ ( 𝜑 → 𝑌 ∈ Fin )
hoiprodp1.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
hoiprodp1.z ⊢ ( 𝜑 → ¬ 𝑍 ∈ 𝑌 )
hoiprodp1.x ⊢ 𝑋 = ( 𝑌 ∪ { 𝑍 } )
hoiprodp1.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
hoiprodp1.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
hoiprodp1.g ⊢ 𝐺 = ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
Assertion hoiprodp1 ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( 𝐺 · ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoiprodp1.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
2 hoiprodp1.y ⊢ ( 𝜑 → 𝑌 ∈ Fin )
3 hoiprodp1.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
4 hoiprodp1.z ⊢ ( 𝜑 → ¬ 𝑍 ∈ 𝑌 )
5 hoiprodp1.x ⊢ 𝑋 = ( 𝑌 ∪ { 𝑍 } )
6 hoiprodp1.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
7 hoiprodp1.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
8 hoiprodp1.g ⊢ 𝐺 = ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
9 snfi ⊢ { 𝑍 } ∈ Fin
10 9 a1i ⊢ ( 𝜑 → { 𝑍 } ∈ Fin )
11 unfi ⊢ ( ( 𝑌 ∈ Fin ∧ { 𝑍 } ∈ Fin ) → ( 𝑌 ∪ { 𝑍 } ) ∈ Fin )
12 2 10 11 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∪ { 𝑍 } ) ∈ Fin )
13 5 12 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ Fin )
14 snidg ⊢ ( 𝑍 ∈ 𝑉 → 𝑍 ∈ { 𝑍 } )
15 3 14 syl ⊢ ( 𝜑 → 𝑍 ∈ { 𝑍 } )
16 elun2 ⊢ ( 𝑍 ∈ { 𝑍 } → 𝑍 ∈ ( 𝑌 ∪ { 𝑍 } ) )
17 15 16 syl ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑌 ∪ { 𝑍 } ) )
18 17 5 eleqtrrdi ⊢ ( 𝜑 → 𝑍 ∈ 𝑋 )
19 18 ne0d ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
20 1 13 19 6 7 hoidmvn0val ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
21 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
22 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
23 volicore ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
24 21 22 23 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
25 24 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℂ )
26 fveq2 ⊢ ( 𝑘 = 𝑍 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑍 ) )
27 fveq2 ⊢ ( 𝑘 = 𝑍 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑍 ) )
28 26 27 oveq12d ⊢ ( 𝑘 = 𝑍 → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) )
29 28 fveq2d ⊢ ( 𝑘 = 𝑍 → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑍 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) )
31 13 25 18 30 fprodsplit1 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
32 5 difeq1i ⊢ ( 𝑋 ∖ { 𝑍 } ) = ( ( 𝑌 ∪ { 𝑍 } ) ∖ { 𝑍 } )
33 32 a1i ⊢ ( 𝜑 → ( 𝑋 ∖ { 𝑍 } ) = ( ( 𝑌 ∪ { 𝑍 } ) ∖ { 𝑍 } ) )
34 difun2 ⊢ ( ( 𝑌 ∪ { 𝑍 } ) ∖ { 𝑍 } ) = ( 𝑌 ∖ { 𝑍 } )
35 34 a1i ⊢ ( 𝜑 → ( ( 𝑌 ∪ { 𝑍 } ) ∖ { 𝑍 } ) = ( 𝑌 ∖ { 𝑍 } ) )
36 difsn ⊢ ( ¬ 𝑍 ∈ 𝑌 → ( 𝑌 ∖ { 𝑍 } ) = 𝑌 )
37 4 36 syl ⊢ ( 𝜑 → ( 𝑌 ∖ { 𝑍 } ) = 𝑌 )
38 33 35 37 3eqtrd ⊢ ( 𝜑 → ( 𝑋 ∖ { 𝑍 } ) = 𝑌 )
39 38 prodeq1d ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
40 8 eqcomi ⊢ ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 𝐺
41 40 a1i ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 𝐺 )
42 39 41 eqtrd ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 𝐺 )
43 42 oveq2d ⊢ ( 𝜑 → ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) · 𝐺 ) )
44 6 18 ffvelcdmd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ )
45 7 18 ffvelcdmd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
46 volicore ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ∈ ℝ )
47 44 45 46 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ∈ ℝ )
48 47 recnd ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ∈ ℂ )
49 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝐴 : 𝑋 ⟶ ℝ )
50 ssun1 ⊢ 𝑌 ⊆ ( 𝑌 ∪ { 𝑍 } )
51 50 5 sseqtrri ⊢ 𝑌 ⊆ 𝑋
52 id ⊢ ( 𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑌 )
53 51 52 sselid ⊢ ( 𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑋 )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝑘 ∈ 𝑋 )
55 49 54 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
56 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝐵 : 𝑋 ⟶ ℝ )
57 56 54 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
58 55 57 23 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
59 2 58 fprodrecl ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
60 8 59 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ ℝ )
61 60 recnd ⊢ ( 𝜑 → 𝐺 ∈ ℂ )
62 48 61 mulcomd ⊢ ( 𝜑 → ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) · 𝐺 ) = ( 𝐺 · ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ) )
63 43 62 eqtrd ⊢ ( 𝜑 → ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) = ( 𝐺 · ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ) )
64 20 31 63 3eqtrd ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( 𝐺 · ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ) )