Metamath Proof Explorer

Theorem hsphoidmvle

Description: The dimensional volume of a half-open interval intersected with a half-space, is less than or equal to the dimensional volume of the original half-open interval. Used in the last inequality of step (e) of Lemma 115B of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hsphoidmvle.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 ) ) ) ) ) )
hsphoidmvle.x 
|- ( ph -> X e. Fin )
hsphoidmvle.z 
|- ( ph -> Z e. ( X \ Y ) )
hsphoidmvle.y 
|- X = ( Y u. { Z } )
hsphoidmvle.c 
|- ( ph -> C e. RR )
hsphoidmvle.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 ) ) ) ) )
hsphoidmvle.a 
|- ( ph -> A : X --> RR )
hsphoidmvle.b 
|- ( ph -> B : X --> RR )
Assertion hsphoidmvle 
|- ( ph -> ( A ( L ` X ) ( ( H ` C ) ` B ) ) <_ ( A ( L ` X ) B ) )

Proof

Step Hyp Ref Expression
1 hsphoidmvle.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 hsphoidmvle.x 
 |-  ( ph -> X e. Fin )
3 hsphoidmvle.z 
 |-  ( ph -> Z e. ( X \ Y ) )
4 hsphoidmvle.y 
 |-  X = ( Y u. { Z } )
5 hsphoidmvle.c 
 |-  ( ph -> C e. RR )
6 hsphoidmvle.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 ) ) ) ) )
7 hsphoidmvle.a 
 |-  ( ph -> A : X --> RR )
8 hsphoidmvle.b 
 |-  ( ph -> B : X --> RR )
9 3 eldifad 
 |-  ( ph -> Z e. X )
10 7 9 ffvelrnd 
 |-  ( ph -> ( A ` Z ) e. RR )
11 8 9 ffvelrnd 
 |-  ( ph -> ( B ` Z ) e. RR )
12 11 5 ifcld 
 |-  ( ph -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) e. RR )
13 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 )
14 10 12 13 syl2anc 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) e. RR )
15 volicore 
 |-  ( ( ( A ` Z ) e. RR /\ ( B ` Z ) e. RR ) -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) e. RR )
16 10 11 15 syl2anc 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) e. RR )
17 difssd 
 |-  ( ph -> ( X \ { Z } ) C_ X )
18 ssfi 
 |-  ( ( X e. Fin /\ ( X \ { Z } ) C_ X ) -> ( X \ { Z } ) e. Fin )
19 2 17 18 syl2anc 
 |-  ( ph -> ( X \ { Z } ) e. Fin )
20 eldifi 
 |-  ( k e. ( X \ { Z } ) -> k e. X )
21 20 adantl 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> k e. X )
22 7 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
23 8 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
24 volicore 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
25 22 23 24 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
26 21 25 syldan 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
27 19 26 fprodrecl 
 |-  ( ph -> prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
28 nfv 
 |-  F/ k ph
29 21 22 syldan 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( A ` k ) e. RR )
30 21 23 syldan 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( B ` k ) e. RR )
31 30 rexrd 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( B ` k ) e. RR* )
32 icombl 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR* ) -> ( ( A ` k ) [,) ( B ` k ) ) e. dom vol )
33 29 31 32 syl2anc 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( ( A ` k ) [,) ( B ` k ) ) e. dom vol )
34 volge0 
 |-  ( ( ( A ` k ) [,) ( B ` k ) ) e. dom vol -> 0 <_ ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
35 33 34 syl 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> 0 <_ ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
36 28 19 26 35 fprodge0 
 |-  ( ph -> 0 <_ prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
37 12 rexrd 
 |-  ( ph -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) e. RR* )
38 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 )
39 10 37 38 syl2anc 
 |-  ( ph -> ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) e. dom vol )
40 11 rexrd 
 |-  ( ph -> ( B ` Z ) e. RR* )
41 icombl 
 |-  ( ( ( A ` Z ) e. RR /\ ( B ` Z ) e. RR* ) -> ( ( A ` Z ) [,) ( B ` Z ) ) e. dom vol )
42 10 40 41 syl2anc 
 |-  ( ph -> ( ( A ` Z ) [,) ( B ` Z ) ) e. dom vol )
43 10 rexrd 
 |-  ( ph -> ( A ` Z ) e. RR* )
44 10 leidd 
 |-  ( ph -> ( A ` Z ) <_ ( A ` Z ) )
45 min1 
 |-  ( ( ( B ` Z ) e. RR /\ C e. RR ) -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) <_ ( B ` Z ) )
46 11 5 45 syl2anc 
 |-  ( ph -> if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) <_ ( B ` Z ) )
47 icossico 
 |-  ( ( ( ( A ` Z ) e. RR* /\ ( B ` Z ) e. RR* ) /\ ( ( A ` Z ) <_ ( A ` Z ) /\ if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) <_ ( B ` Z ) ) ) -> ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) C_ ( ( A ` Z ) [,) ( B ` Z ) ) )
48 43 40 44 46 47 syl22anc 
 |-  ( ph -> ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) C_ ( ( A ` Z ) [,) ( B ` Z ) ) )
49 volss 
 |-  ( ( ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) e. dom vol /\ ( ( A ` Z ) [,) ( B ` Z ) ) e. dom vol /\ ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) C_ ( ( A ` Z ) [,) ( B ` Z ) ) ) -> ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) <_ ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) )
50 39 42 48 49 syl3anc 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) <_ ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) )
51 14 16 27 36 50 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 ) [,) ( B ` Z ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
52 9 ne0d 
 |-  ( ph -> X =/= (/) )
53 6 5 2 8 hsphoif 
 |-  ( ph -> ( ( H ` C ) ` B ) : X --> RR )
54 1 2 52 7 53 hoidmvn0val 
 |-  ( ph -> ( A ( L ` X ) ( ( H ` C ) ` B ) ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) )
55 53 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( ( ( H ` C ) ` B ) ` k ) e. RR )
56 volicore 
 |-  ( ( ( A ` k ) e. RR /\ ( ( ( H ` C ) ` B ) ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) e. RR )
57 22 55 56 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) e. RR )
58 57 recnd 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) e. CC )
59 fveq2 
 |-  ( k = Z -> ( A ` k ) = ( A ` Z ) )
60 fveq2 
 |-  ( k = Z -> ( ( ( H ` C ) ` B ) ` k ) = ( ( ( H ` C ) ` B ) ` Z ) )
61 59 60 oveq12d 
 |-  ( k = Z -> ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) = ( ( A ` Z ) [,) ( ( ( H ` C ) ` B ) ` Z ) ) )
62 61 fveq2d 
 |-  ( k = Z -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( ( ( H ` C ) ` B ) ` Z ) ) ) )
63 62 adantl 
 |-  ( ( ph /\ k = Z ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( ( ( H ` C ) ` B ) ` Z ) ) ) )
64 6 5 2 8 9 hsphoival 
 |-  ( ph -> ( ( ( H ` C ) ` B ) ` Z ) = if ( Z e. Y , ( B ` Z ) , if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) )
65 3 eldifbd 
 |-  ( ph -> -. Z e. Y )
66 65 iffalsed 
 |-  ( ph -> if ( Z e. Y , ( B ` Z ) , if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) = if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) )
67 64 66 eqtrd 
 |-  ( ph -> ( ( ( H ` C ) ` B ) ` Z ) = if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) )
68 67 oveq2d 
 |-  ( ph -> ( ( A ` Z ) [,) ( ( ( H ` C ) ` B ) ` Z ) ) = ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) )
69 68 fveq2d 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) ( ( ( H ` C ) ` B ) ` Z ) ) ) = ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) )
70 69 adantr 
 |-  ( ( ph /\ k = Z ) -> ( vol ` ( ( A ` Z ) [,) ( ( ( H ` C ) ` B ) ` Z ) ) ) = ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) )
71 63 70 eqtrd 
 |-  ( ( ph /\ k = Z ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) if ( ( B ` Z ) <_ C , ( B ` Z ) , C ) ) ) )
72 2 58 9 71 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 ) ) ) ) )
73 5 adantr 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> C e. RR )
74 2 adantr 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> X e. Fin )
75 8 adantr 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> B : X --> RR )
76 6 73 74 75 21 hsphoival 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( ( ( H ` C ) ` B ) ` k ) = if ( k e. Y , ( B ` k ) , if ( ( B ` k ) <_ C , ( B ` k ) , C ) ) )
77 20 4 eleqtrdi 
 |-  ( k e. ( X \ { Z } ) -> k e. ( Y u. { Z } ) )
78 eldifn 
 |-  ( k e. ( X \ { Z } ) -> -. k e. { Z } )
79 elunnel2 
 |-  ( ( k e. ( Y u. { Z } ) /\ -. k e. { Z } ) -> k e. Y )
80 77 78 79 syl2anc 
 |-  ( k e. ( X \ { Z } ) -> k e. Y )
81 80 adantl 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> k e. Y )
82 81 iftrued 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> if ( k e. Y , ( B ` k ) , if ( ( B ` k ) <_ C , ( B ` k ) , C ) ) = ( B ` k ) )
83 76 82 eqtrd 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( ( ( H ` C ) ` B ) ` k ) = ( B ` k ) )
84 83 oveq2d 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
85 84 fveq2d 
 |-  ( ( ph /\ k e. ( X \ { Z } ) ) -> ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) = ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
86 85 prodeq2dv 
 |-  ( ph -> prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( ( ( H ` C ) ` B ) ` k ) ) ) = prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
87 86 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 ) ) ) ) )
88 54 72 87 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 ) ) ) ) )
89 1 7 8 2 hoidmvval 
 |-  ( ph -> ( A ( L ` X ) B ) = if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
90 52 neneqd 
 |-  ( ph -> -. X = (/) )
91 90 iffalsed 
 |-  ( ph -> if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
92 25 recnd 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. CC )
93 fveq2 
 |-  ( k = Z -> ( B ` k ) = ( B ` Z ) )
94 59 93 oveq12d 
 |-  ( k = Z -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
95 94 fveq2d 
 |-  ( k = Z -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) )
96 95 adantl 
 |-  ( ( ph /\ k = Z ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) )
97 2 92 9 96 fprodsplit1 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
98 89 91 97 3eqtrd 
 |-  ( ph -> ( A ( L ` X ) B ) = ( ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
99 88 98 breq12d 
 |-  ( ph -> ( ( A ( L ` X ) ( ( H ` C ) ` B ) ) <_ ( A ( L ` X ) 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 ) [,) ( B ` Z ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) ) )
100 51 99 mpbird 
 |-  ( ph -> ( A ( L ` X ) ( ( H ` C ) ` B ) ) <_ ( A ( L ` X ) B ) )