Metamath Proof Explorer

Theorem hsphoidmvle2

Description: The dimensional volume of a half-open interval intersected with a two half-spaces. Used in the last inequality of step (c) of Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

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

Proof

Step Hyp Ref Expression
1 hsphoidmvle2.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
2 hsphoidmvle2.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 hsphoidmvle2.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) )
4 hsphoidmvle2.y ⊢ 𝑋 = ( 𝑌 ∪ { 𝑍 } )
5 hsphoidmvle2.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6 hsphoidmvle2.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
7 hsphoidmvle2.e ⊢ ( 𝜑 → 𝐶 ≤ 𝐷 )
8 hsphoidmvle2.h ⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑗 ∈ 𝑋 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) )
9 hsphoidmvle2.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
10 hsphoidmvle2.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
11 3 eldifad ⊢ ( 𝜑 → 𝑍 ∈ 𝑋 )
12 9 11 ffvelrnd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ )
13 10 11 ffvelrnd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
14 13 5 ifcld ⊢ ( 𝜑 → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ∈ ℝ )
15 volicore ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) ∈ ℝ )
16 12 14 15 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) ∈ ℝ )
17 13 6 ifcld ⊢ ( 𝜑 → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ∈ ℝ )
18 volicore ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ) ∈ ℝ )
19 12 17 18 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ) ∈ ℝ )
20 difssd ⊢ ( 𝜑 → ( 𝑋 ∖ { 𝑍 } ) ⊆ 𝑋 )
21 ssfi ⊢ ( ( 𝑋 ∈ Fin ∧ ( 𝑋 ∖ { 𝑍 } ) ⊆ 𝑋 ) → ( 𝑋 ∖ { 𝑍 } ) ∈ Fin )
22 2 20 21 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∖ { 𝑍 } ) ∈ Fin )
23 eldifi ⊢ ( 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) → 𝑘 ∈ 𝑋 )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝑘 ∈ 𝑋 )
25 9 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
26 10 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
27 volicore ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
28 25 26 27 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
29 24 28 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
30 22 29 fprodrecl ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
31 nfv ⊢ Ⅎ 𝑘 𝜑
32 24 25 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
33 24 26 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
34 33 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* )
35 icombl ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ* ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ∈ dom vol )
36 32 34 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ∈ dom vol )
37 volge0 ⊢ ( ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ∈ dom vol → 0 ≤ ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
38 36 37 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 0 ≤ ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
39 31 22 29 38 fprodge0 ⊢ ( 𝜑 → 0 ≤ ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
40 14 rexrd ⊢ ( 𝜑 → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ∈ ℝ* )
41 icombl ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ∈ ℝ* ) → ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ∈ dom vol )
42 12 40 41 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ∈ dom vol )
43 17 rexrd ⊢ ( 𝜑 → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ∈ ℝ* )
44 icombl ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ∈ ℝ* ) → ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ∈ dom vol )
45 12 43 44 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ∈ dom vol )
46 12 rexrd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ* )
47 12 leidd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ≤ ( 𝐴 ‘ 𝑍 ) )
48 13 leidd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ≤ ( 𝐵 ‘ 𝑍 ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → ( 𝐵 ‘ 𝑍 ) ≤ ( 𝐵 ‘ 𝑍 ) )
50 iftrue ⊢ ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) = ( 𝐵 ‘ 𝑍 ) )
51 50 adantl ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) = ( 𝐵 ‘ 𝑍 ) )
52 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
53 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → 𝐶 ∈ ℝ )
54 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → 𝐷 ∈ ℝ )
55 simpr ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 )
56 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → 𝐶 ≤ 𝐷 )
57 52 53 54 55 56 letrd ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 )
58 57 iftrued ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) = ( 𝐵 ‘ 𝑍 ) )
59 51 58 breq12d ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → ( if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ≤ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ↔ ( 𝐵 ‘ 𝑍 ) ≤ ( 𝐵 ‘ 𝑍 ) ) )
60 49 59 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ≤ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
61 simpl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → 𝜑 )
62 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 )
63 61 5 syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → 𝐶 ∈ ℝ )
64 61 13 syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
65 63 64 ltnled ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → ( 𝐶 < ( 𝐵 ‘ 𝑍 ) ↔ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) )
66 62 65 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → 𝐶 < ( 𝐵 ‘ 𝑍 ) )
67 5 adantr ⊢ ( ( 𝜑 ∧ 𝐶 < ( 𝐵 ‘ 𝑍 ) ) → 𝐶 ∈ ℝ )
68 13 adantr ⊢ ( ( 𝜑 ∧ 𝐶 < ( 𝐵 ‘ 𝑍 ) ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
69 simpr ⊢ ( ( 𝜑 ∧ 𝐶 < ( 𝐵 ‘ 𝑍 ) ) → 𝐶 < ( 𝐵 ‘ 𝑍 ) )
70 67 68 69 ltled ⊢ ( ( 𝜑 ∧ 𝐶 < ( 𝐵 ‘ 𝑍 ) ) → 𝐶 ≤ ( 𝐵 ‘ 𝑍 ) )
71 70 adantr ⊢ ( ( ( 𝜑 ∧ 𝐶 < ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 ) → 𝐶 ≤ ( 𝐵 ‘ 𝑍 ) )
72 iftrue ⊢ ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) = ( 𝐵 ‘ 𝑍 ) )
73 72 eqcomd ⊢ ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 → ( 𝐵 ‘ 𝑍 ) = if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
74 73 adantl ⊢ ( ( ( 𝜑 ∧ 𝐶 < ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 ) → ( 𝐵 ‘ 𝑍 ) = if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
75 71 74 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝐶 < ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 ) → 𝐶 ≤ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
76 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 < ( 𝐵 ‘ 𝑍 ) ) ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 ) → 𝐶 ≤ 𝐷 )
77 iffalse ⊢ ( ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) = 𝐷 )
78 77 eqcomd ⊢ ( ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 → 𝐷 = if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
79 78 adantl ⊢ ( ( ( 𝜑 ∧ 𝐶 < ( 𝐵 ‘ 𝑍 ) ) ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 ) → 𝐷 = if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
80 76 79 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝐶 < ( 𝐵 ‘ 𝑍 ) ) ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 ) → 𝐶 ≤ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
81 75 80 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝐶 < ( 𝐵 ‘ 𝑍 ) ) → 𝐶 ≤ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
82 61 66 81 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → 𝐶 ≤ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
83 iffalse ⊢ ( ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) = 𝐶 )
84 83 adantl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) = 𝐶 )
85 84 breq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → ( if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ≤ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ↔ 𝐶 ≤ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) )
86 82 85 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 ) → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ≤ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
87 60 86 pm2.61dan ⊢ ( 𝜑 → if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ≤ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
88 icossico ⊢ ( ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ* ∧ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ∈ ℝ* ) ∧ ( ( 𝐴 ‘ 𝑍 ) ≤ ( 𝐴 ‘ 𝑍 ) ∧ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ≤ if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ) → ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ⊆ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) )
89 46 43 47 87 88 syl22anc ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ⊆ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) )
90 volss ⊢ ( ( ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ∈ dom vol ∧ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ∈ dom vol ∧ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ⊆ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) ≤ ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ) )
91 42 45 89 90 syl3anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) ≤ ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ) )
92 16 19 30 39 91 lemul1ad ⊢ ( 𝜑 → ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) ≤ ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
93 11 ne0d ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
94 8 5 2 10 hsphoif ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) : 𝑋 ⟶ ℝ )
95 1 2 93 9 94 hoidmvn0val ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) )
96 94 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
97 volicore ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ∈ ℝ )
98 25 96 97 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ∈ ℝ )
99 98 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ∈ ℂ )
100 fveq2 ⊢ ( 𝑘 = 𝑍 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑍 ) )
101 fveq2 ⊢ ( 𝑘 = 𝑍 → ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) = ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) )
102 100 101 oveq12d ⊢ ( 𝑘 = 𝑍 → ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) ) )
103 102 fveq2d ⊢ ( 𝑘 = 𝑍 → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) )
104 103 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑍 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) )
105 8 5 2 10 11 hsphoival ⊢ ( 𝜑 → ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) = if ( 𝑍 ∈ 𝑌 , ( 𝐵 ‘ 𝑍 ) , if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) )
106 3 eldifbd ⊢ ( 𝜑 → ¬ 𝑍 ∈ 𝑌 )
107 106 iffalsed ⊢ ( 𝜑 → if ( 𝑍 ∈ 𝑌 , ( 𝐵 ‘ 𝑍 ) , if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) = if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) )
108 105 107 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) = if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) )
109 108 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) ) = ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) )
110 109 fveq2d ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) )
111 110 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑍 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) )
112 104 111 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑍 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) )
113 2 99 11 112 fprodsplit1 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ) )
114 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝐶 ∈ ℝ )
115 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝑋 ∈ Fin )
116 10 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝐵 : 𝑋 ⟶ ℝ )
117 8 114 115 116 24 hsphoival ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝑌 , ( 𝐵 ‘ 𝑘 ) , if ( ( 𝐵 ‘ 𝑘 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑘 ) , 𝐶 ) ) )
118 23 4 eleqtrdi ⊢ ( 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) → 𝑘 ∈ ( 𝑌 ∪ { 𝑍 } ) )
119 eldifn ⊢ ( 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) → ¬ 𝑘 ∈ { 𝑍 } )
120 elunnel2 ⊢ ( ( 𝑘 ∈ ( 𝑌 ∪ { 𝑍 } ) ∧ ¬ 𝑘 ∈ { 𝑍 } ) → 𝑘 ∈ 𝑌 )
121 118 119 120 syl2anc ⊢ ( 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) → 𝑘 ∈ 𝑌 )
122 121 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝑘 ∈ 𝑌 )
123 122 iftrued ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → if ( 𝑘 ∈ 𝑌 , ( 𝐵 ‘ 𝑘 ) , if ( ( 𝐵 ‘ 𝑘 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑘 ) , 𝐶 ) ) = ( 𝐵 ‘ 𝑘 ) )
124 117 123 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
125 124 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
126 125 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
127 126 prodeq2dv ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
128 127 oveq2d ⊢ ( 𝜑 → ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
129 95 113 128 3eqtrd ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
130 8 6 2 10 hsphoif ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) : 𝑋 ⟶ ℝ )
131 1 2 93 9 130 hoidmvn0val ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) )
132 130 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
133 volicore ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ∈ ℝ )
134 25 132 133 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ∈ ℝ )
135 134 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ∈ ℂ )
136 fveq2 ⊢ ( 𝑘 = 𝑍 → ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) = ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑍 ) )
137 100 136 oveq12d ⊢ ( 𝑘 = 𝑍 → ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑍 ) ) )
138 137 fveq2d ⊢ ( 𝑘 = 𝑍 → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) )
139 138 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑍 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) )
140 2 135 11 139 fprodsplit1 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ) )
141 8 6 2 10 11 hsphoival ⊢ ( 𝜑 → ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑍 ) = if ( 𝑍 ∈ 𝑌 , ( 𝐵 ‘ 𝑍 ) , if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) )
142 106 iffalsed ⊢ ( 𝜑 → if ( 𝑍 ∈ 𝑌 , ( 𝐵 ‘ 𝑍 ) , if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) = if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
143 141 142 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑍 ) = if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) )
144 143 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑍 ) ) = ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) )
145 144 fveq2d ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ) )
146 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝐷 ∈ ℝ )
147 8 146 115 116 24 hsphoival ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝑌 , ( 𝐵 ‘ 𝑘 ) , if ( ( 𝐵 ‘ 𝑘 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑘 ) , 𝐷 ) ) )
148 122 iftrued ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → if ( 𝑘 ∈ 𝑌 , ( 𝐵 ‘ 𝑘 ) , if ( ( 𝐵 ‘ 𝑘 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑘 ) , 𝐷 ) ) = ( 𝐵 ‘ 𝑘 ) )
149 147 148 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
150 149 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
151 150 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
152 151 prodeq2dv ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
153 145 152 oveq12d ⊢ ( 𝜑 → ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑍 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
154 131 140 153 3eqtrd ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
155 129 154 breq12d ⊢ ( 𝜑 → ( ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ) ≤ ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ) ↔ ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐶 , ( 𝐵 ‘ 𝑍 ) , 𝐶 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) ≤ ( ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) if ( ( 𝐵 ‘ 𝑍 ) ≤ 𝐷 , ( 𝐵 ‘ 𝑍 ) , 𝐷 ) ) ) · ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝑍 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) ) )
156 92 155 mpbird ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐶 ) ‘ 𝐵 ) ) ≤ ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝐻 ‘ 𝐷 ) ‘ 𝐵 ) ) )