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 
|- ( ph -> X e. Fin )
hspmbllem1.k 
|- ( ph -> K e. X )
hspmbllem1.y 
|- ( ph -> Y e. RR )
hspmbllem1.a 
|- ( ph -> A : X --> RR )
hspmbllem1.b 
|- ( ph -> B : X --> RR )
hspmbllem1.l 
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
hspmbllem1.t 
|- T = ( y e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) )
hspmbllem1.s 
|- S = ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h = K , if ( x <_ ( c ` h ) , ( c ` h ) , x ) , ( c ` h ) ) ) ) )
Assertion hspmbllem1 
|- ( ph -> ( A ( L ` X ) B ) = ( ( A ( L ` X ) ( ( T ` Y ) ` B ) ) +e ( ( ( S ` Y ) ` A ) ( L ` X ) B ) ) )

Proof

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