Metamath Proof Explorer

Theorem hspmbllem1

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (a) of Lemma 115F of Fremlin1 p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hspmbllem1.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hspmbllem1.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑋 )
hspmbllem1.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
hspmbllem1.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
hspmbllem1.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
hspmbllem1.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
hspmbllem1.t ⊢ 𝑇 = ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) )
hspmbllem1.s ⊢ 𝑆 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ = 𝐾 , if ( 𝑥 ≤ ( 𝑐 ‘ ℎ ) , ( 𝑐 ‘ ℎ ) , 𝑥 ) , ( 𝑐 ‘ ℎ ) ) ) ) )
Assertion hspmbllem1 ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ) +𝑒 ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 hspmbllem1.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 hspmbllem1.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑋 )
3 hspmbllem1.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
4 hspmbllem1.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
5 hspmbllem1.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
6 hspmbllem1.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
7 hspmbllem1.t ⊢ 𝑇 = ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) )
8 hspmbllem1.s ⊢ 𝑆 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ = 𝐾 , if ( 𝑥 ≤ ( 𝑐 ‘ ℎ ) , ( 𝑐 ‘ ℎ ) , 𝑥 ) , ( 𝑐 ‘ ℎ ) ) ) ) )
9 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
10 7 3 1 5 hsphoif ⊢ ( 𝜑 → ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) : 𝑋 ⟶ ℝ )
11 6 1 4 10 hoidmvcl ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ) ∈ ( 0 [,) +∞ ) )
12 9 11 sseldi ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ) ∈ ℝ )
13 8 3 1 4 hoidifhspf ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) : 𝑋 ⟶ ℝ )
14 6 1 13 5 hoidmvcl ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) ∈ ( 0 [,) +∞ ) )
15 9 14 sseldi ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) ∈ ℝ )
16 12 15 rexaddd ⊢ ( 𝜑 → ( ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ) +𝑒 ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) ) = ( ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ) + ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) ) )
17 2 ne0d ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
18 6 1 17 4 10 hoidmvn0val ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) )
19 6 1 17 13 5 hoidmvn0val ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
20 18 19 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ) + ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) ) = ( ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) + ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) )
21 uncom ⊢ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = ( { 𝐾 } ∪ ( 𝑋 ∖ { 𝐾 } ) )
22 21 a1i ⊢ ( 𝜑 → ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = ( { 𝐾 } ∪ ( 𝑋 ∖ { 𝐾 } ) ) )
23 2 snssd ⊢ ( 𝜑 → { 𝐾 } ⊆ 𝑋 )
24 undif ⊢ ( { 𝐾 } ⊆ 𝑋 ↔ ( { 𝐾 } ∪ ( 𝑋 ∖ { 𝐾 } ) ) = 𝑋 )
25 23 24 sylib ⊢ ( 𝜑 → ( { 𝐾 } ∪ ( 𝑋 ∖ { 𝐾 } ) ) = 𝑋 )
26 22 25 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = 𝑋 )
27 26 eqcomd ⊢ ( 𝜑 → 𝑋 = ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) )
28 27 prodeq1d ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) )
29 nfv ⊢ Ⅎ 𝑘 𝜑
30 nfcv ⊢ Ⅎ 𝑘 ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) )
31 difssd ⊢ ( 𝜑 → ( 𝑋 ∖ { 𝐾 } ) ⊆ 𝑋 )
32 1 31 ssfid ⊢ ( 𝜑 → ( 𝑋 ∖ { 𝐾 } ) ∈ Fin )
33 neldifsnd ⊢ ( 𝜑 → ¬ 𝐾 ∈ ( 𝑋 ∖ { 𝐾 } ) )
34 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → 𝐴 : 𝑋 ⟶ ℝ )
35 31 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → 𝑘 ∈ 𝑋 )
36 34 35 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
37 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → 𝑌 ∈ ℝ )
38 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → 𝑋 ∈ Fin )
39 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → 𝐵 : 𝑋 ⟶ ℝ )
40 7 37 38 39 hsphoif ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) : 𝑋 ⟶ ℝ )
41 40 35 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
42 volicore ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ∈ ℝ )
43 36 41 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ∈ ℝ )
44 43 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) ∈ ℂ )
45 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝐾 ) )
46 fveq2 ⊢ ( 𝑘 = 𝐾 → ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) = ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) )
47 45 46 oveq12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) )
48 47 fveq2d ⊢ ( 𝑘 = 𝐾 → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) )
49 4 2 ffvelrnd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ∈ ℝ )
50 10 2 ffvelrnd ⊢ ( 𝜑 → ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ∈ ℝ )
51 volicore ⊢ ( ( ( 𝐴 ‘ 𝐾 ) ∈ ℝ ∧ ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) ∈ ℝ )
52 49 50 51 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) ∈ ℝ )
53 52 recnd ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) ∈ ℂ )
54 29 30 32 2 33 44 48 53 fprodsplitsn ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) ) )
55 7 37 38 39 35 hsphoival ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝐵 ‘ 𝑘 ) , if ( ( 𝐵 ‘ 𝑘 ) ≤ 𝑌 , ( 𝐵 ‘ 𝑘 ) , 𝑌 ) ) )
56 iftrue ⊢ ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) → if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝐵 ‘ 𝑘 ) , if ( ( 𝐵 ‘ 𝑘 ) ≤ 𝑌 , ( 𝐵 ‘ 𝑘 ) , 𝑌 ) ) = ( 𝐵 ‘ 𝑘 ) )
57 56 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝐵 ‘ 𝑘 ) , if ( ( 𝐵 ‘ 𝑘 ) ≤ 𝑌 , ( 𝐵 ‘ 𝑘 ) , 𝑌 ) ) = ( 𝐵 ‘ 𝑘 ) )
58 55 57 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
59 58 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
60 59 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
61 60 prodeq2dv ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
62 61 oveq1d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) ) = ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) ) )
63 28 54 62 3eqtrd ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) = ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) ) )
64 27 prodeq1d ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
65 nfcv ⊢ Ⅎ 𝑘 ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) )
66 13 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) : 𝑋 ⟶ ℝ )
67 66 35 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℝ )
68 58 41 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
69 volicore ⊢ ( ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
70 67 68 69 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
71 70 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℂ )
72 fveq2 ⊢ ( 𝑘 = 𝐾 → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) = ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) )
73 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝐾 ) )
74 72 73 oveq12d ⊢ ( 𝑘 = 𝐾 → ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) )
75 74 fveq2d ⊢ ( 𝑘 = 𝐾 → ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
76 13 2 ffvelrnd ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) ∈ ℝ )
77 5 2 ffvelrnd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐾 ) ∈ ℝ )
78 volicore ⊢ ( ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝐾 ) ∈ ℝ ) → ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ∈ ℝ )
79 76 77 78 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ∈ ℝ )
80 79 recnd ⊢ ( 𝜑 → ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ∈ ℂ )
81 29 65 32 2 33 71 75 80 fprodsplitsn ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
82 8 37 38 34 35 hoidifhspval3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) = if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) )
83 eldifsni ⊢ ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) → 𝑘 ≠ 𝐾 )
84 neneq ⊢ ( 𝑘 ≠ 𝐾 → ¬ 𝑘 = 𝐾 )
85 83 84 syl ⊢ ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) → ¬ 𝑘 = 𝐾 )
86 85 iffalsed ⊢ ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) → if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) = ( 𝐴 ‘ 𝑘 ) )
87 86 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) = ( 𝐴 ‘ 𝑘 ) )
88 82 87 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
89 88 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
90 89 prodeq2dv ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
91 90 oveq1d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
92 64 81 91 3eqtrd ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
93 63 92 oveq12d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ) ) + ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) = ( ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) ) + ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) ) )
94 27 prodeq1d ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
95 nfcv ⊢ Ⅎ 𝑘 ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) )
96 60 44 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℂ )
97 45 73 oveq12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) )
98 97 fveq2d ⊢ ( 𝑘 = 𝐾 → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
99 volicore ⊢ ( ( ( 𝐴 ‘ 𝐾 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝐾 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ∈ ℝ )
100 49 77 99 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ∈ ℝ )
101 100 recnd ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ∈ ℂ )
102 29 95 32 2 33 96 98 101 fprodsplitsn ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
103 94 102 eqtrd ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
104 7 3 1 5 2 hsphoival ⊢ ( 𝜑 → ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) = if ( 𝐾 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝐵 ‘ 𝐾 ) , if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) )
105 33 iffalsed ⊢ ( 𝜑 → if ( 𝐾 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝐵 ‘ 𝐾 ) , if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) = if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) )
106 104 105 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) = if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) )
107 106 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) = ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) )
108 107 fveq2d ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) ) )
109 8 3 1 4 2 hoidifhspval3 ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) = if ( 𝐾 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) , ( 𝐴 ‘ 𝐾 ) ) )
110 eqid ⊢ 𝐾 = 𝐾
111 110 iftruei ⊢ if ( 𝐾 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) , ( 𝐴 ‘ 𝐾 ) ) = if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 )
112 111 a1i ⊢ ( 𝜑 → if ( 𝐾 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) , ( 𝐴 ‘ 𝐾 ) ) = if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) )
113 109 112 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) = if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) )
114 113 fvoveq1d ⊢ ( 𝜑 → ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) = ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
115 108 114 oveq12d ⊢ ( 𝜑 → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) + ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
116 iftrue ⊢ ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 → if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) = ( 𝐵 ‘ 𝐾 ) )
117 116 oveq2d ⊢ ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 → ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) = ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) )
118 117 fveq2d ⊢ ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
119 118 oveq1d ⊢ ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
120 119 adantl ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
121 iftrue ⊢ ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) → if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) = ( 𝐴 ‘ 𝐾 ) )
122 121 oveq1d ⊢ ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) → ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) = ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) )
123 122 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) = ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) )
124 77 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 𝐵 ‘ 𝐾 ) ∈ ℝ )
125 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → 𝑌 ∈ ℝ )
126 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 𝐴 ‘ 𝐾 ) ∈ ℝ )
127 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 )
128 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) )
129 124 125 126 127 128 letrd ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 𝐵 ‘ 𝐾 ) ≤ ( 𝐴 ‘ 𝐾 ) )
130 126 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 𝐴 ‘ 𝐾 ) ∈ ℝ* )
131 124 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 𝐵 ‘ 𝐾 ) ∈ ℝ* )
132 ico0 ⊢ ( ( ( 𝐴 ‘ 𝐾 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝐾 ) ∈ ℝ* ) → ( ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) = ∅ ↔ ( 𝐵 ‘ 𝐾 ) ≤ ( 𝐴 ‘ 𝐾 ) ) )
133 130 131 132 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) = ∅ ↔ ( 𝐵 ‘ 𝐾 ) ≤ ( 𝐴 ‘ 𝐾 ) ) )
134 129 133 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) = ∅ )
135 123 134 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) = ∅ )
136 iffalse ⊢ ( ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) → if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) = 𝑌 )
137 136 oveq1d ⊢ ( ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) → ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) = ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) )
138 137 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) = ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) )
139 simpr ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 )
140 3 rexrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
141 140 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → 𝑌 ∈ ℝ* )
142 77 rexrd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐾 ) ∈ ℝ* )
143 142 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( 𝐵 ‘ 𝐾 ) ∈ ℝ* )
144 ico0 ⊢ ( ( 𝑌 ∈ ℝ* ∧ ( 𝐵 ‘ 𝐾 ) ∈ ℝ* ) → ( ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) = ∅ ↔ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) )
145 141 143 144 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) = ∅ ↔ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) )
146 139 145 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) = ∅ )
147 146 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) = ∅ )
148 138 147 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) = ∅ )
149 135 148 pm2.61dan ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) = ∅ )
150 149 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) = ( vol ‘ ∅ ) )
151 vol0 ⊢ ( vol ‘ ∅ ) = 0
152 151 a1i ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( vol ‘ ∅ ) = 0 )
153 150 152 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) = 0 )
154 153 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) + 0 ) )
155 101 addid1d ⊢ ( 𝜑 → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) + 0 ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
156 155 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) + 0 ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
157 120 154 156 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
158 iffalse ⊢ ( ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 → if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) = 𝑌 )
159 158 oveq2d ⊢ ( ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 → ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) = ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) )
160 159 fveq2d ⊢ ( ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) )
161 160 adantl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) )
162 161 oveq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
163 simpl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → 𝜑 )
164 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 )
165 163 3 syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → 𝑌 ∈ ℝ )
166 163 77 syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( 𝐵 ‘ 𝐾 ) ∈ ℝ )
167 165 166 ltnled ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( 𝑌 < ( 𝐵 ‘ 𝐾 ) ↔ ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) )
168 164 167 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → 𝑌 < ( 𝐵 ‘ 𝐾 ) )
169 121 fvoveq1d ⊢ ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) → ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
170 169 oveq2d ⊢ ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
171 170 adantl ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
172 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) )
173 49 rexrd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ∈ ℝ* )
174 173 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 𝐴 ‘ 𝐾 ) ∈ ℝ* )
175 140 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → 𝑌 ∈ ℝ* )
176 ico0 ⊢ ( ( ( 𝐴 ‘ 𝐾 ) ∈ ℝ* ∧ 𝑌 ∈ ℝ* ) → ( ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) = ∅ ↔ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) )
177 174 175 176 syl2anc ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) = ∅ ↔ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) )
178 172 177 mpbird ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) = ∅ )
179 178 fveq2d ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) = ( vol ‘ ∅ ) )
180 151 a1i ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( vol ‘ ∅ ) = 0 )
181 179 180 eqtrd ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) = 0 )
182 181 oveq1d ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( 0 + ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
183 182 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( 0 + ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
184 101 addid2d ⊢ ( 𝜑 → ( 0 + ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
185 184 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 0 + ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
186 171 183 185 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
187 136 fvoveq1d ⊢ ( ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) → ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) = ( vol ‘ ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) ) )
188 187 oveq2d ⊢ ( ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
189 188 adantl ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
190 simpl ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) )
191 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) )
192 49 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 𝐴 ‘ 𝐾 ) ∈ ℝ )
193 3 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → 𝑌 ∈ ℝ )
194 192 193 ltnled ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( 𝐴 ‘ 𝐾 ) < 𝑌 ↔ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) )
195 191 194 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 𝐴 ‘ 𝐾 ) < 𝑌 )
196 195 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( 𝐴 ‘ 𝐾 ) < 𝑌 )
197 49 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( 𝐴 ‘ 𝐾 ) ∈ ℝ )
198 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → 𝑌 ∈ ℝ )
199 volico ⊢ ( ( ( 𝐴 ‘ 𝐾 ) ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) = if ( ( 𝐴 ‘ 𝐾 ) < 𝑌 , ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) , 0 ) )
200 197 198 199 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) = if ( ( 𝐴 ‘ 𝐾 ) < 𝑌 , ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) , 0 ) )
201 iftrue ⊢ ( ( 𝐴 ‘ 𝐾 ) < 𝑌 → if ( ( 𝐴 ‘ 𝐾 ) < 𝑌 , ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) , 0 ) = ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) )
202 201 adantl ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → if ( ( 𝐴 ‘ 𝐾 ) < 𝑌 , ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) , 0 ) = ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) )
203 200 202 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) = ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) )
204 203 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) = ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) )
205 3 adantr ⊢ ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) → 𝑌 ∈ ℝ )
206 77 adantr ⊢ ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) → ( 𝐵 ‘ 𝐾 ) ∈ ℝ )
207 volico ⊢ ( ( 𝑌 ∈ ℝ ∧ ( 𝐵 ‘ 𝐾 ) ∈ ℝ ) → ( vol ‘ ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) ) = if ( 𝑌 < ( 𝐵 ‘ 𝐾 ) , ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) , 0 ) )
208 205 206 207 syl2anc ⊢ ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) → ( vol ‘ ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) ) = if ( 𝑌 < ( 𝐵 ‘ 𝐾 ) , ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) , 0 ) )
209 iftrue ⊢ ( 𝑌 < ( 𝐵 ‘ 𝐾 ) → if ( 𝑌 < ( 𝐵 ‘ 𝐾 ) , ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) , 0 ) = ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) )
210 209 adantl ⊢ ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) → if ( 𝑌 < ( 𝐵 ‘ 𝐾 ) , ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) , 0 ) = ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) )
211 208 210 eqtrd ⊢ ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) → ( vol ‘ ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) ) = ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) )
212 211 adantr ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( vol ‘ ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) ) = ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) )
213 204 212 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) + ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) ) )
214 190 196 213 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( 𝑌 [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) + ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) ) )
215 197 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( 𝐴 ‘ 𝐾 ) ∈ ℝ )
216 205 adantr ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → 𝑌 ∈ ℝ )
217 206 adantr ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( 𝐵 ‘ 𝐾 ) ∈ ℝ )
218 simpr ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( 𝐴 ‘ 𝐾 ) < 𝑌 )
219 simplr ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → 𝑌 < ( 𝐵 ‘ 𝐾 ) )
220 215 216 217 218 219 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( 𝐴 ‘ 𝐾 ) < ( 𝐵 ‘ 𝐾 ) )
221 220 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → if ( ( 𝐴 ‘ 𝐾 ) < ( 𝐵 ‘ 𝐾 ) , ( ( 𝐵 ‘ 𝐾 ) − ( 𝐴 ‘ 𝐾 ) ) , 0 ) = ( ( 𝐵 ‘ 𝐾 ) − ( 𝐴 ‘ 𝐾 ) ) )
222 221 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( ( 𝐵 ‘ 𝐾 ) − ( 𝐴 ‘ 𝐾 ) ) = if ( ( 𝐴 ‘ 𝐾 ) < ( 𝐵 ‘ 𝐾 ) , ( ( 𝐵 ‘ 𝐾 ) − ( 𝐴 ‘ 𝐾 ) ) , 0 ) )
223 3 49 resubcld ⊢ ( 𝜑 → ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) ∈ ℝ )
224 223 recnd ⊢ ( 𝜑 → ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) ∈ ℂ )
225 77 3 resubcld ⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) ∈ ℝ )
226 225 recnd ⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) ∈ ℂ )
227 224 226 addcomd ⊢ ( 𝜑 → ( ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) + ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) ) = ( ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) + ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) ) )
228 77 recnd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐾 ) ∈ ℂ )
229 3 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
230 49 recnd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ∈ ℂ )
231 228 229 230 npncand ⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) + ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) ) = ( ( 𝐵 ‘ 𝐾 ) − ( 𝐴 ‘ 𝐾 ) ) )
232 227 231 eqtrd ⊢ ( 𝜑 → ( ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) + ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) ) = ( ( 𝐵 ‘ 𝐾 ) − ( 𝐴 ‘ 𝐾 ) ) )
233 232 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) + ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) ) = ( ( 𝐵 ‘ 𝐾 ) − ( 𝐴 ‘ 𝐾 ) ) )
234 volico ⊢ ( ( ( 𝐴 ‘ 𝐾 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝐾 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) = if ( ( 𝐴 ‘ 𝐾 ) < ( 𝐵 ‘ 𝐾 ) , ( ( 𝐵 ‘ 𝐾 ) − ( 𝐴 ‘ 𝐾 ) ) , 0 ) )
235 215 217 234 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) = if ( ( 𝐴 ‘ 𝐾 ) < ( 𝐵 ‘ 𝐾 ) , ( ( 𝐵 ‘ 𝐾 ) − ( 𝐴 ‘ 𝐾 ) ) , 0 ) )
236 222 233 235 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ( 𝐴 ‘ 𝐾 ) < 𝑌 ) → ( ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) + ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
237 190 196 236 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( 𝑌 − ( 𝐴 ‘ 𝐾 ) ) + ( ( 𝐵 ‘ 𝐾 ) − 𝑌 ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
238 189 214 237 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) ∧ ¬ 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
239 186 238 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑌 < ( 𝐵 ‘ 𝐾 ) ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
240 163 168 239 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) 𝑌 ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
241 162 240 eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 ) → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
242 157 241 pm2.61dan ⊢ ( 𝜑 → ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) if ( ( 𝐵 ‘ 𝐾 ) ≤ 𝑌 , ( 𝐵 ‘ 𝐾 ) , 𝑌 ) ) ) + ( vol ‘ ( if ( 𝑌 ≤ ( 𝐴 ‘ 𝐾 ) , ( 𝐴 ‘ 𝐾 ) , 𝑌 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) )
243 115 242 eqtr2d ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) = ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) + ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) )
244 243 oveq2d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) = ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) + ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) ) )
245 32 96 fprodcl ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℂ )
246 245 53 80 adddid ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) + ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) ) = ( ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) ) + ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) ) )
247 103 244 246 3eqtrrd ⊢ ( 𝜑 → ( ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝐾 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ) ) ) + ( ∏ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) [,) ( 𝐵 ‘ 𝐾 ) ) ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
248 20 93 247 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ) + ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
249 6 1 17 4 5 hoidmvn0val ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
250 249 eqcomd ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
251 16 248 250 3eqtrrd ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ) +𝑒 ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) ) )