Metamath Proof Explorer

Theorem hoidifhspdmvle

Description: The dimensional volume of the difference of a half-open interval and a half-space is less than or equal to the dimensional volume of the whole half-open interval. Used in Lemma 115F of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoidifhspdmvle.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 ) ) ) ) ) )
hoidifhspdmvle.x 
|- ( ph -> X e. Fin )
hoidifhspdmvle.a 
|- ( ph -> A : X --> RR )
hoidifhspdmvle.b 
|- ( ph -> B : X --> RR )
hoidifhspdmvle.k 
|- ( ph -> K e. X )
hoidifhspdmvle.d 
|- D = ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h = K , if ( x <_ ( c ` h ) , ( c ` h ) , x ) , ( c ` h ) ) ) ) )
hoidifhspdmvle.y 
|- ( ph -> Y e. RR )
Assertion hoidifhspdmvle 
|- ( ph -> ( ( ( D ` Y ) ` A ) ( L ` X ) B ) <_ ( A ( L ` X ) B ) )

Proof

Step Hyp Ref Expression
1 hoidifhspdmvle.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 hoidifhspdmvle.x 
 |-  ( ph -> X e. Fin )
3 hoidifhspdmvle.a 
 |-  ( ph -> A : X --> RR )
4 hoidifhspdmvle.b 
 |-  ( ph -> B : X --> RR )
5 hoidifhspdmvle.k 
 |-  ( ph -> K e. X )
6 hoidifhspdmvle.d 
 |-  D = ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h = K , if ( x <_ ( c ` h ) , ( c ` h ) , x ) , ( c ` h ) ) ) ) )
7 hoidifhspdmvle.y 
 |-  ( ph -> Y e. RR )
8 nfv 
 |-  F/ k ph
9 6 7 2 3 hoidifhspf 
 |-  ( ph -> ( ( D ` Y ) ` A ) : X --> RR )
10 9 ffvelcdmda 
 |-  ( ( ph /\ k e. X ) -> ( ( ( D ` Y ) ` A ) ` k ) e. RR )
11 4 ffvelcdmda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
12 volicore 
 |-  ( ( ( ( ( D ` Y ) ` A ) ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) ) e. RR )
13 10 11 12 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) ) e. RR )
14 11 rexrd 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR* )
15 icombl 
 |-  ( ( ( ( ( D ` Y ) ` A ) ` k ) e. RR /\ ( B ` k ) e. RR* ) -> ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) e. dom vol )
16 10 14 15 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) e. dom vol )
17 volge0 
 |-  ( ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) e. dom vol -> 0 <_ ( vol ` ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) ) )
18 16 17 syl 
 |-  ( ( ph /\ k e. X ) -> 0 <_ ( vol ` ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) ) )
19 3 ffvelcdmda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
20 volicore 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
21 19 11 20 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
22 icombl 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR* ) -> ( ( A ` k ) [,) ( B ` k ) ) e. dom vol )
23 19 14 22 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( ( A ` k ) [,) ( B ` k ) ) e. dom vol )
24 19 rexrd 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR* )
25 7 adantr 
 |-  ( ( ph /\ k e. X ) -> Y e. RR )
26 25 adantr 
 |-  ( ( ( ph /\ k e. X ) /\ k = K ) -> Y e. RR )
27 19 adantr 
 |-  ( ( ( ph /\ k e. X ) /\ k = K ) -> ( A ` k ) e. RR )
28 max2 
 |-  ( ( Y e. RR /\ ( A ` k ) e. RR ) -> ( A ` k ) <_ if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) )
29 26 27 28 syl2anc 
 |-  ( ( ( ph /\ k e. X ) /\ k = K ) -> ( A ` k ) <_ if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) )
30 2 adantr 
 |-  ( ( ph /\ k e. X ) -> X e. Fin )
31 3 adantr 
 |-  ( ( ph /\ k e. X ) -> A : X --> RR )
32 simpr 
 |-  ( ( ph /\ k e. X ) -> k e. X )
33 6 25 30 31 32 hoidifhspval3 
 |-  ( ( ph /\ k e. X ) -> ( ( ( D ` Y ) ` A ) ` k ) = if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) )
34 33 adantr 
 |-  ( ( ( ph /\ k e. X ) /\ k = K ) -> ( ( ( D ` Y ) ` A ) ` k ) = if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) )
35 iftrue 
 |-  ( k = K -> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) = if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) )
36 35 adantl 
 |-  ( ( ( ph /\ k e. X ) /\ k = K ) -> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) = if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) )
37 34 36 eqtr2d 
 |-  ( ( ( ph /\ k e. X ) /\ k = K ) -> if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) = ( ( ( D ` Y ) ` A ) ` k ) )
38 29 37 breqtrd 
 |-  ( ( ( ph /\ k e. X ) /\ k = K ) -> ( A ` k ) <_ ( ( ( D ` Y ) ` A ) ` k ) )
39 19 leidd 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) <_ ( A ` k ) )
40 39 adantr 
 |-  ( ( ( ph /\ k e. X ) /\ -. k = K ) -> ( A ` k ) <_ ( A ` k ) )
41 33 adantr 
 |-  ( ( ( ph /\ k e. X ) /\ -. k = K ) -> ( ( ( D ` Y ) ` A ) ` k ) = if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) )
42 iffalse 
 |-  ( -. k = K -> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) = ( A ` k ) )
43 42 adantl 
 |-  ( ( ( ph /\ k e. X ) /\ -. k = K ) -> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) = ( A ` k ) )
44 41 43 eqtr2d 
 |-  ( ( ( ph /\ k e. X ) /\ -. k = K ) -> ( A ` k ) = ( ( ( D ` Y ) ` A ) ` k ) )
45 40 44 breqtrd 
 |-  ( ( ( ph /\ k e. X ) /\ -. k = K ) -> ( A ` k ) <_ ( ( ( D ` Y ) ` A ) ` k ) )
46 38 45 pm2.61dan 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) <_ ( ( ( D ` Y ) ` A ) ` k ) )
47 11 leidd 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) <_ ( B ` k ) )
48 icossico 
 |-  ( ( ( ( A ` k ) e. RR* /\ ( B ` k ) e. RR* ) /\ ( ( A ` k ) <_ ( ( ( D ` Y ) ` A ) ` k ) /\ ( B ` k ) <_ ( B ` k ) ) ) -> ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) C_ ( ( A ` k ) [,) ( B ` k ) ) )
49 24 14 46 47 48 syl22anc 
 |-  ( ( ph /\ k e. X ) -> ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) C_ ( ( A ` k ) [,) ( B ` k ) ) )
50 volss 
 |-  ( ( ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) e. dom vol /\ ( ( A ` k ) [,) ( B ` k ) ) e. dom vol /\ ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) C_ ( ( A ` k ) [,) ( B ` k ) ) ) -> ( vol ` ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) ) <_ ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
51 16 23 49 50 syl3anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) ) <_ ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
52 8 2 13 18 21 51 fprodle 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
53 5 ne0d 
 |-  ( ph -> X =/= (/) )
54 1 2 53 9 4 hoidmvn0val 
 |-  ( ph -> ( ( ( D ` Y ) ` A ) ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) ) )
55 1 2 53 3 4 hoidmvn0val 
 |-  ( ph -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
56 54 55 breq12d 
 |-  ( ph -> ( ( ( ( D ` Y ) ` A ) ( L ` X ) B ) <_ ( A ( L ` X ) B ) <-> prod_ k e. X ( vol ` ( ( ( ( D ` Y ) ` A ) ` k ) [,) ( B ` k ) ) ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
57 52 56 mpbird 
 |-  ( ph -> ( ( ( D ` Y ) ` A ) ( L ` X ) B ) <_ ( A ( L ` X ) B ) )