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 ffvelrnda
 |-  ( ( ph /\ k e. X ) -> ( ( ( D ` Y ) ` A ) ` k ) e. RR )
11 4 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( 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 ) )