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 ) ) |