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	sselid	⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ) ∈ ℝ )
13	8 3 1 4	hoidifhspf	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) : 𝑋 ⟶ ℝ )
14	6 1 13 5	hoidmvcl	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) ∈ ( 0 [,) +∞ ) )
15	9 14	sselid	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) ∈ ℝ )
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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
37	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → 𝑌 ∈ ℝ )
38	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → 𝑋 ∈ Fin )
39	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → 𝐵 : 𝑋 ⟶ ℝ )
40	7 37 38 39	hsphoif	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) : 𝑋 ⟶ ℝ )
41	40 35	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
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	ffvelcdmd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ∈ ℝ )
50	10 2	ffvelcdmd	⊢ ( 𝜑 → ( ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ‘ 𝐾 ) ∈ ℝ )
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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℝ )
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	ffvelcdmd	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐾 ) ∈ ℝ )
77	5 2	ffvelcdmd	⊢ ( 𝜑 → ( 𝐵 ‘ 𝐾 ) ∈ ℝ )
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	addridd	⊢ ( 𝜑 → ( ( 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	addlidd	⊢ ( 𝜑 → ( 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	⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( ( 𝐴 ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ 𝐵 ) ) +𝑒 ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) ) )