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 
|- 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 ) ) ) ) ) )
hsphoidmvle2.x 
|- ( ph -> X e. Fin )
hsphoidmvle2.z 
|- ( ph -> Z e. ( X \ Y ) )
hsphoidmvle2.y 
|- X = ( Y u. { Z } )
hsphoidmvle2.c 
|- ( ph -> C e. RR )
hsphoidmvle2.d 
|- ( ph -> D e. RR )
hsphoidmvle2.e 
|- ( ph -> C <_ D )
hsphoidmvle2.h 
|- H = ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )
hsphoidmvle2.a 
|- ( ph -> A : X --> RR )
hsphoidmvle2.b 
|- ( ph -> B : X --> RR )
Assertion hsphoidmvle2 
|- ( ph -> ( A ( L ` X ) ( ( H ` C ) ` B ) ) <_ ( A ( L ` X ) ( ( H ` D ) ` B ) ) )

Proof

Step Hyp Ref Expression
1 hsphoidmvle2.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 ) ) ) ) ) )
2 hsphoidmvle2.x 
 |-  ( ph -> X e. Fin )
3 hsphoidmvle2.z 
 |-  ( ph -> Z e. ( X \ Y ) )
4 hsphoidmvle2.y 
 |-  X = ( Y u. { Z } )
5 hsphoidmvle2.c 
 |-  ( ph -> C e. RR )
6 hsphoidmvle2.d 
 |-  ( ph -> D e. RR )
7 hsphoidmvle2.e 
 |-  ( ph -> C <_ D )
8 hsphoidmvle2.h 
 |-  H = ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )
9 hsphoidmvle2.a 
 |-  ( ph -> A : X --> RR )
10 hsphoidmvle2.b 
 |-  ( ph -> B : X --> RR )
11 3 eldifad 
 |-  ( ph -> Z e. X )
12 9 11 ffvelrnd 
 |-  ( ph -> ( A ` Z ) e. RR )
13 10 11 ffvelrnd 
 |-  ( ph -> ( B ` Z ) e. RR )
14 13 5 ifcld 
 |-  ( ph -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) e. RR )
15 volicore 
 |-  ( ( ( A ` Z ) e. RR /\ if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) e. RR ) -> ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) e. RR )
16 12 14 15 syl2anc 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) e. RR )
17 13 6 ifcld 
 |-  ( ph -> if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) e. RR )
18 volicore 
 |-  ( ( ( A ` Z ) e. RR /\ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) e. RR ) -> ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) ) e. RR )
19 12 17 18 syl2anc 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) ) e. RR )
20 difssd 
 |-  ( ph -> ( X \ { Z } ) C_ X )
21 ssfi 
 |-  ( ( X e. Fin /\ ( X \ { Z } ) C_ X ) -> ( X \ { Z } ) e. Fin )
22 2 20 21 syl2anc 
 |-  ( ph -> ( X \ { Z } ) e. Fin )
23 eldifi 
 |-  ( k e. ( X \ { Z } ) -> k e. X )
24 23 adantl 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> k e. X )
25 9 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
26 10 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
27 volicore 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
28 25 26 27 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
29 24 28 syldan 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
30 22 29 fprodrecl 
 |-  ( ph -> prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
31 nfv 
 |-  F/ k ph
32 24 25 syldan 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( A ` k ) e. RR )
33 24 26 syldan 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( B ` k ) e. RR )
34 33 rexrd 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( B ` k ) e. RR* )
35 icombl 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR* ) -> ( ( A ` k ) [,) ( B ` k ) ) e. dom vol )
36 32 34 35 syl2anc 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( ( A ` k ) [,) ( B ` k ) ) e. dom vol )
37 volge0 
 |-  ( ( ( A ` k ) [,) ( B ` k ) ) e. dom vol -> 0 <_ ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
38 36 37 syl 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> 0 <_ ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
39 31 22 29 38 fprodge0 
 |-  ( ph -> 0 <_ prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
40 14 rexrd 
 |-  ( ph -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) e. RR* )
41 icombl 
 |-  ( ( ( A ` Z ) e. RR /\ if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) e. RR* ) -> ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) e. dom vol )
42 12 40 41 syl2anc 
 |-  ( ph -> ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) e. dom vol )
43 17 rexrd 
 |-  ( ph -> if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) e. RR* )
44 icombl 
 |-  ( ( ( A ` Z ) e. RR /\ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) e. RR* ) -> ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) e. dom vol )
45 12 43 44 syl2anc 
 |-  ( ph -> ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) e. dom vol )
46 12 rexrd 
 |-  ( ph -> ( A ` Z ) e. RR* )
47 12 leidd 
 |-  ( ph -> ( A ` Z ) <_ ( A ` Z ) )
48 13 leidd 
 |-  ( ph -> ( B ` Z ) <_ ( B ` Z ) )
49 48 adantr 
 |-  ( ( ph /\ ( B ` Z ) <_ C ) -> ( B ` Z ) <_ ( B ` Z ) )
50 iftrue 
 |-  ( ( B ` Z ) <_ C -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) = ( B ` Z ) )
51 50 adantl 
 |-  ( ( ph /\ ( B ` Z ) <_ C ) -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) = ( B ` Z ) )
52 13 adantr 
 |-  ( ( ph /\ ( B ` Z ) <_ C ) -> ( B ` Z ) e. RR )
53 5 adantr 
 |-  ( ( ph /\ ( B ` Z ) <_ C ) -> C e. RR )
54 6 adantr 
 |-  ( ( ph /\ ( B ` Z ) <_ C ) -> D e. RR )
55 simpr 
 |-  ( ( ph /\ ( B ` Z ) <_ C ) -> ( B ` Z ) <_ C )
56 7 adantr 
 |-  ( ( ph /\ ( B ` Z ) <_ C ) -> C <_ D )
57 52 53 54 55 56 letrd 
 |-  ( ( ph /\ ( B ` Z ) <_ C ) -> ( B ` Z ) <_ D )
58 57 iftrued 
 |-  ( ( ph /\ ( B ` Z ) <_ C ) -> if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) = ( B ` Z ) )
59 51 58 breq12d 
 |-  ( ( ph /\ ( B ` Z ) <_ C ) -> ( if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) <_ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) <-> ( B ` Z ) <_ ( B ` Z ) ) )
60 49 59 mpbird 
 |-  ( ( ph /\ ( B ` Z ) <_ C ) -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) <_ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
61 simpl 
 |-  ( ( ph /\ -. ( B ` Z ) <_ C ) -> ph )
62 simpr 
 |-  ( ( ph /\ -. ( B ` Z ) <_ C ) -> -. ( B ` Z ) <_ C )
63 61 5 syl 
 |-  ( ( ph /\ -. ( B ` Z ) <_ C ) -> C e. RR )
64 61 13 syl 
 |-  ( ( ph /\ -. ( B ` Z ) <_ C ) -> ( B ` Z ) e. RR )
65 63 64 ltnled 
 |-  ( ( ph /\ -. ( B ` Z ) <_ C ) -> ( C < ( B ` Z ) <-> -. ( B ` Z ) <_ C ) )
66 62 65 mpbird 
 |-  ( ( ph /\ -. ( B ` Z ) <_ C ) -> C < ( B ` Z ) )
67 5 adantr 
 |-  ( ( ph /\ C < ( B ` Z ) ) -> C e. RR )
68 13 adantr 
 |-  ( ( ph /\ C < ( B ` Z ) ) -> ( B ` Z ) e. RR )
69 simpr 
 |-  ( ( ph /\ C < ( B ` Z ) ) -> C < ( B ` Z ) )
70 67 68 69 ltled 
 |-  ( ( ph /\ C < ( B ` Z ) ) -> C <_ ( B ` Z ) )
71 70 adantr 
 |-  ( ( ( ph /\ C < ( B ` Z ) ) /\ ( B ` Z ) <_ D ) -> C <_ ( B ` Z ) )
72 iftrue 
 |-  ( ( B ` Z ) <_ D -> if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) = ( B ` Z ) )
73 72 eqcomd 
 |-  ( ( B ` Z ) <_ D -> ( B ` Z ) = if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
74 73 adantl 
 |-  ( ( ( ph /\ C < ( B ` Z ) ) /\ ( B ` Z ) <_ D ) -> ( B ` Z ) = if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
75 71 74 breqtrd 
 |-  ( ( ( ph /\ C < ( B ` Z ) ) /\ ( B ` Z ) <_ D ) -> C <_ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
76 7 ad2antrr 
 |-  ( ( ( ph /\ C < ( B ` Z ) ) /\ -. ( B ` Z ) <_ D ) -> C <_ D )
77 iffalse 
 |-  ( -. ( B ` Z ) <_ D -> if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) = D )
78 77 eqcomd 
 |-  ( -. ( B ` Z ) <_ D -> D = if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
79 78 adantl 
 |-  ( ( ( ph /\ C < ( B ` Z ) ) /\ -. ( B ` Z ) <_ D ) -> D = if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
80 76 79 breqtrd 
 |-  ( ( ( ph /\ C < ( B ` Z ) ) /\ -. ( B ` Z ) <_ D ) -> C <_ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
81 75 80 pm2.61dan 
 |-  ( ( ph /\ C < ( B ` Z ) ) -> C <_ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
82 61 66 81 syl2anc 
 |-  ( ( ph /\ -. ( B ` Z ) <_ C ) -> C <_ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
83 iffalse 
 |-  ( -. ( B ` Z ) <_ C -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) = C )
84 83 adantl 
 |-  ( ( ph /\ -. ( B ` Z ) <_ C ) -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) = C )
85 84 breq1d 
 |-  ( ( ph /\ -. ( B ` Z ) <_ C ) -> ( if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) <_ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) <-> C <_ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) )
86 82 85 mpbird 
 |-  ( ( ph /\ -. ( B ` Z ) <_ C ) -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) <_ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
87 60 86 pm2.61dan 
 |-  ( ph -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) <_ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
88 icossico 
 |-  ( ( ( ( A ` Z ) e. RR* /\ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) e. RR* ) /\ ( ( A ` Z ) <_ ( A ` Z ) /\ if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) <_ if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) ) -> ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) C_ ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) )
89 46 43 47 87 88 syl22anc 
 |-  ( ph -> ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) C_ ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) )
90 volss 
 |-  ( ( ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) e. dom vol /\ ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) e. dom vol /\ ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) C_ ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) ) -> ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) <_ ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) ) )
91 42 45 89 90 syl3anc 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) <_ ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) ) )
92 16 19 30 39 91 lemul1ad 
 |-  ( ph -> ( ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) <_ ( ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
93 11 ne0d 
 |-  ( ph -> X =/= (/) )
94 8 5 2 10 hsphoif 
 |-  ( ph -> ( ( H ` C ) ` B ) : X --> RR )
95 1 2 93 9 94 hoidmvn0val 
 |-  ( ph -> ( A ( L ` X ) ( ( H ` C ) ` B ) ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) )
96 94 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( ( ( H ` C ) ` B ) ` k ) e. RR )
97 volicore 
 |-  ( ( ( A ` k ) e. RR /\ ( ( ( H ` C ) ` B ) ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) e. RR )
98 25 96 97 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) e. RR )
99 98 recnd 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) e. CC )
100 fveq2 
 |-  ( k = Z -> ( A ` k ) = ( A ` Z ) )
101 fveq2 
 |-  ( k = Z -> ( ( ( H ` C ) ` B ) ` k ) = ( ( ( H ` C ) ` B ) ` Z ) )
102 100 101 oveq12d 
 |-  ( k = Z -> ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) = ( ( A ` Z ) [,) ( ( ( H ` C ) ` B ) ` Z ) ) )
103 102 fveq2d 
 |-  ( k = Z -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( ( ( H ` C ) ` B ) ` Z ) ) ) )
104 103 adantl 
 |-  ( ( ph /\ k = Z ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( ( ( H ` C ) ` B ) ` Z ) ) ) )
105 8 5 2 10 11 hsphoival 
 |-  ( ph -> ( ( ( H ` C ) ` B ) ` Z ) = if ( Z e. Y , ( B ` Z ) , if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) )
106 3 eldifbd 
 |-  ( ph -> -. Z e. Y )
107 106 iffalsed 
 |-  ( ph -> if ( Z e. Y , ( B ` Z ) , if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) = if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) )
108 105 107 eqtrd 
 |-  ( ph -> ( ( ( H ` C ) ` B ) ` Z ) = if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) )
109 108 oveq2d 
 |-  ( ph -> ( ( A ` Z ) [,) ( ( ( H ` C ) ` B ) ` Z ) ) = ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) )
110 109 fveq2d 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) ( ( ( H ` C ) ` B ) ` Z ) ) ) = ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) )
111 110 adantr 
 |-  ( ( ph /\ k = Z ) -> ( vol ` ( ( A ` Z ) [,) ( ( ( H ` C ) ` B ) ` Z ) ) ) = ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) )
112 104 111 eqtrd 
 |-  ( ( ph /\ k = Z ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) )
113 2 99 11 112 fprodsplit1 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) = ( ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) ) )
114 5 adantr 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> C e. RR )
115 2 adantr 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> X e. Fin )
116 10 adantr 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> B : X --> RR )
117 8 114 115 116 24 hsphoival 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( ( ( H ` C ) ` B ) ` k ) = if ( k e. Y , ( B ` k ) , if ( ( B ` k ) <_ C , ( B ` k ) , C ) ) )
118 23 4 eleqtrdi 
 |-  ( k e. ( X \ { Z } ) -> k e. ( Y u. { Z } ) )
119 eldifn 
 |-  ( k e. ( X \ { Z } ) -> -. k e. { Z } )
120 elunnel2 
 |-  ( ( k e. ( Y u. { Z } ) /\ -. k e. { Z } ) -> k e. Y )
121 118 119 120 syl2anc 
 |-  ( k e. ( X \ { Z } ) -> k e. Y )
122 121 adantl 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> k e. Y )
123 122 iftrued 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> if ( k e. Y , ( B ` k ) , if ( ( B ` k ) <_ C , ( B ` k ) , C ) ) = ( B ` k ) )
124 117 123 eqtrd 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( ( ( H ` C ) ` B ) ` k ) = ( B ` k ) )
125 124 oveq2d 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
126 125 fveq2d 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) = ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
127 126 prodeq2dv 
 |-  ( ph -> prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) = prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
128 127 oveq2d 
 |-  ( ph -> ( ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) ) = ( ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
129 95 113 128 3eqtrd 
 |-  ( ph -> ( A ( L ` X ) ( ( H ` C ) ` B ) ) = ( ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
130 8 6 2 10 hsphoif 
 |-  ( ph -> ( ( H ` D ) ` B ) : X --> RR )
131 1 2 93 9 130 hoidmvn0val 
 |-  ( ph -> ( A ( L ` X ) ( ( H ` D ) ` B ) ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) ) )
132 130 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( ( ( H ` D ) ` B ) ` k ) e. RR )
133 volicore 
 |-  ( ( ( A ` k ) e. RR /\ ( ( ( H ` D ) ` B ) ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) ) e. RR )
134 25 132 133 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) ) e. RR )
135 134 recnd 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) ) e. CC )
136 fveq2 
 |-  ( k = Z -> ( ( ( H ` D ) ` B ) ` k ) = ( ( ( H ` D ) ` B ) ` Z ) )
137 100 136 oveq12d 
 |-  ( k = Z -> ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) = ( ( A ` Z ) [,) ( ( ( H ` D ) ` B ) ` Z ) ) )
138 137 fveq2d 
 |-  ( k = Z -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( ( ( H ` D ) ` B ) ` Z ) ) ) )
139 138 adantl 
 |-  ( ( ph /\ k = Z ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( ( ( H ` D ) ` B ) ` Z ) ) ) )
140 2 135 11 139 fprodsplit1 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) ) = ( ( vol ` ( ( A ` Z ) [,) ( ( ( H ` D ) ` B ) ` Z ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) ) ) )
141 8 6 2 10 11 hsphoival 
 |-  ( ph -> ( ( ( H ` D ) ` B ) ` Z ) = if ( Z e. Y , ( B ` Z ) , if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) )
142 106 iffalsed 
 |-  ( ph -> if ( Z e. Y , ( B ` Z ) , if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) = if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
143 141 142 eqtrd 
 |-  ( ph -> ( ( ( H ` D ) ` B ) ` Z ) = if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) )
144 143 oveq2d 
 |-  ( ph -> ( ( A ` Z ) [,) ( ( ( H ` D ) ` B ) ` Z ) ) = ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) )
145 144 fveq2d 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) ( ( ( H ` D ) ` B ) ` Z ) ) ) = ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) ) )
146 6 adantr 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> D e. RR )
147 8 146 115 116 24 hsphoival 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( ( ( H ` D ) ` B ) ` k ) = if ( k e. Y , ( B ` k ) , if ( ( B ` k ) <_ D , ( B ` k ) , D ) ) )
148 122 iftrued 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> if ( k e. Y , ( B ` k ) , if ( ( B ` k ) <_ D , ( B ` k ) , D ) ) = ( B ` k ) )
149 147 148 eqtrd 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( ( ( H ` D ) ` B ) ` k ) = ( B ` k ) )
150 149 oveq2d 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
151 150 fveq2d 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) ) = ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
152 151 prodeq2dv 
 |-  ( ph -> prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) ) = prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
153 145 152 oveq12d 
 |-  ( ph -> ( ( vol ` ( ( A ` Z ) [,) ( ( ( H ` D ) ` B ) ` Z ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( ( ( H ` D ) ` B ) ` k ) ) ) ) = ( ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
154 131 140 153 3eqtrd 
 |-  ( ph -> ( A ( L ` X ) ( ( H ` D ) ` B ) ) = ( ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
155 129 154 breq12d 
 |-  ( ph -> ( ( A ( L ` X ) ( ( H ` C ) ` B ) ) <_ ( A ( L ` X ) ( ( H ` D ) ` B ) ) <-> ( ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) <_ ( ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ D , ( B ` Z ) , D ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) ) )
156 92 155 mpbird 
 |-  ( ph -> ( A ( L ` X ) ( ( H ` C ) ` B ) ) <_ ( A ( L ` X ) ( ( H ` D ) ` B ) ) )