Metamath Proof Explorer

Theorem hsphoidmvle

Description: The dimensional volume of a half-open interval intersected with a half-space, is less than or equal to the dimensional volume of the original half-open interval. Used in the last inequality of step (e) of Lemma 115B of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hsphoidmvle.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
hsphoidmvle.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hsphoidmvle.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) )
hsphoidmvle.y ⊢ 𝑋 = ( 𝑌 ∪ { 𝑍 } )
hsphoidmvle.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
hsphoidmvle.h ⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑗 ∈ 𝑋 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) )
hsphoidmvle.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
hsphoidmvle.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
Assertion hsphoidmvle ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ) ≤ ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 hsphoidmvle.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
2 hsphoidmvle.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 hsphoidmvle.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) )
4 hsphoidmvle.y ⊢ 𝑋 = ( 𝑌 ∪ { 𝑍 } )
5 hsphoidmvle.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6 hsphoidmvle.h ⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑗 ∈ 𝑋 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) )
7 hsphoidmvle.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
8 hsphoidmvle.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
9 3 eldifad ⊢ ( 𝜑 → 𝑍 ∈ 𝑋 )
10 7 9 ffvelrnd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ )
11 8 9 ffvelrnd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
12 11 5 ifcld ⊢ ( 𝜑 → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ∈ ℝ )
13 volicore ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) ∈ ℝ )
14 10 12 13 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) ∈ ℝ )
15 volicore ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ∈ ℝ )
16 10 11 15 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ∈ ℝ )
17 difssd ⊢ ( 𝜑 → ( 𝑋 ∖ { 𝑍 } ) ⊆ 𝑋 )
18 ssfi ⊢ ( ( 𝑋 ∈ Fin ∧ ( 𝑋 ∖ { 𝑍 } ) ⊆ 𝑋 ) → ( 𝑋 ∖ { 𝑍 } ) ∈ Fin )
19 2 17 18 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∖ { 𝑍 } ) ∈ Fin )
20 eldifi ⊢ ( 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) → 𝑘 ∈ 𝑋 )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝑘 ∈ 𝑋 )
22 7 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
23 8 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
24 volicore ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
25 22 23 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
26 21 25 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
27 19 26 fprodrecl ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
28 nfv ⊢ Ⅎ 𝑘 𝜑
29 21 22 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
30 21 23 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
31 30 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* )
32 icombl ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ* ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ∈ dom vol )
33 29 31 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ∈ dom vol )
34 volge0 ⊢ ( ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ∈ dom vol → 0 ≤ ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
35 33 34 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 0 ≤ ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
36 28 19 26 35 fprodge0 ⊢ ( 𝜑 → 0 ≤ ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
37 12 rexrd ⊢ ( 𝜑 → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ∈ ℝ* )
38 icombl ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ∈ ℝ* ) → ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ∈ dom vol )
39 10 37 38 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ∈ dom vol )
40 11 rexrd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ* )
41 icombl ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ* ) → ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ∈ dom vol )
42 10 40 41 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ∈ dom vol )
43 10 rexrd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ* )
44 10 leidd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ≤ ( 𝐴 ‘ 𝑍 ) )
45 min1 ⊢ ( ( ( 𝐵 ‘ 𝑍 ) ∈ ℝ ∧ 𝐶 ∈ ℝ ) → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ≤ ( 𝐵 ‘ 𝑍 ) )
46 11 5 45 syl2anc ⊢ ( 𝜑 → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ≤ ( 𝐵 ‘ 𝑍 ) )
47 icossico ⊢ ( ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ* ) ∧ ( ( 𝐴 ‘ 𝑍 ) ≤ ( 𝐴 ‘ 𝑍 ) ∧ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ≤ ( 𝐵 ‘ 𝑍 ) ) ) → ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ⊆ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) )
48 43 40 44 46 47 syl22anc ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ⊆ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) )
49 volss ⊢ ( ( ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ∈ dom vol ∧ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ∈ dom vol ∧ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ⊆ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) ≤ ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) )
50 39 42 48 49 syl3anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) ≤ ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) )
51 14 16 27 36 50 lemul1ad ⊢ ( 𝜑 → ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) ≤ ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
52 9 ne0d ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
53 6 5 2 8 hsphoif ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) : 𝑋 ⟶ ℝ )
54 1 2 52 7 53 hoidmvn0val ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) )
55 53 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
56 volicore ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ∈ ℝ )
57 22 55 56 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ∈ ℝ )
58 57 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ∈ ℂ )
59 fveq2 ⊢ ( 𝑘 = 𝑍 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑍 ) )
60 fveq2 ⊢ ( 𝑘 = 𝑍 → ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) = ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) )
61 59 60 oveq12d ⊢ ( 𝑘 = 𝑍 → ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) ) )
62 61 fveq2d ⊢ ( 𝑘 = 𝑍 → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) )
63 62 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑍 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) )
64 6 5 2 8 9 hsphoival ⊢ ( 𝜑 → ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) = if ( 𝑍 ∈ 𝑌 , ( 𝐵 ‘ 𝑍 ) , if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) )
65 3 eldifbd ⊢ ( 𝜑 → ¬ 𝑍 ∈ 𝑌 )
66 65 iffalsed ⊢ ( 𝜑 → if ( 𝑍 ∈ 𝑌 , ( 𝐵 ‘ 𝑍 ) , if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) = if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) )
67 64 66 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) = if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) )
68 67 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) ) = ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) )
69 68 fveq2d ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑍 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) )
71 63 70 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑍 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) )
72 2 58 9 71 fprodsplit1 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ) )
73 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝐶 ∈ ℝ )
74 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝑋 ∈ Fin )
75 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝐵 : 𝑋 ⟶ ℝ )
76 6 73 74 75 21 hsphoival ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝑌 , ( 𝐵 ‘ 𝑘 ) , if ( ( 𝐵 ‘ 𝑘 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑘 ) , 𝐶 ) ) )
77 20 4 eleqtrdi ⊢ ( 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) → 𝑘 ∈ ( 𝑌 ∪ { 𝑍 } ) )
78 eldifn ⊢ ( 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) → ¬ 𝑘 ∈ { 𝑍 } )
79 elunnel2 ⊢ ( ( 𝑘 ∈ ( 𝑌 ∪ { 𝑍 } ) ∧ ¬ 𝑘 ∈ { 𝑍 } ) → 𝑘 ∈ 𝑌 )
80 77 78 79 syl2anc ⊢ ( 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) → 𝑘 ∈ 𝑌 )
81 80 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝑘 ∈ 𝑌 )
82 81 iftrued ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → if ( 𝑘 ∈ 𝑌 , ( 𝐵 ‘ 𝑘 ) , if ( ( 𝐵 ‘ 𝑘 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑘 ) , 𝐶 ) ) = ( 𝐵 ‘ 𝑘 ) )
83 76 82 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
84 83 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
85 84 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
86 85 prodeq2dv ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
87 86 oveq2d ⊢ ( 𝜑 → ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
88 54 72 87 3eqtrd ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
89 1 7 8 2 hoidmvval ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
90 52 neneqd ⊢ ( 𝜑 → ¬ 𝑋 = ∅ )
91 90 iffalsed ⊢ ( 𝜑 → if ( 𝑋 = ∅ , 0 , ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
92 25 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℂ )
93 fveq2 ⊢ ( 𝑘 = 𝑍 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑍 ) )
94 59 93 oveq12d ⊢ ( 𝑘 = 𝑍 → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) )
95 94 fveq2d ⊢ ( 𝑘 = 𝑍 → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) )
96 95 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑍 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) )
97 2 92 9 96 fprodsplit1 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
98 89 91 97 3eqtrd ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
99 88 98 breq12d ⊢ ( 𝜑 → ( ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ) ≤ ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ↔ ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) ≤ ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) ) )
100 51 99 mpbird ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ) ≤ ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )