Step |
Hyp |
Ref |
Expression |
1 |
|
ovncvrrp.x |
|- ( ph -> X e. Fin ) |
2 |
|
ovncvrrp.n0 |
|- ( ph -> X =/= (/) ) |
3 |
|
ovncvrrp.a |
|- ( ph -> A C_ ( RR ^m X ) ) |
4 |
|
ovncvrrp.e |
|- ( ph -> E e. RR+ ) |
5 |
|
ovncvrrp.c |
|- C = ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) |
6 |
|
ovncvrrp.l |
|- L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) |
7 |
|
ovncvrrp.d |
|- D = ( a e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) ) |
8 |
|
eqid |
|- { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } |
9 |
1 2 3 4 8
|
ovnlerp |
|- ( ph -> E. z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) |
10 |
|
simp1 |
|- ( ( ph /\ z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> ph ) |
11 |
|
simp3 |
|- ( ( ph /\ z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) |
12 |
|
rabid |
|- ( z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } <-> ( z e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) ) |
13 |
12
|
biimpi |
|- ( z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } -> ( z e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) ) |
14 |
13
|
simprd |
|- ( z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) |
15 |
14
|
adantr |
|- ( ( z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) |
16 |
15
|
3adant1 |
|- ( ( ph /\ z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) |
17 |
|
nfv |
|- F/ i ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) |
18 |
|
nfe1 |
|- F/ i E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) |
19 |
|
simp1l |
|- ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> ph ) |
20 |
|
simp2 |
|- ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) |
21 |
|
simp3l |
|- ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) |
22 |
|
id |
|- ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) ) |
23 |
|
fveq1 |
|- ( l = i -> ( l ` j ) = ( i ` j ) ) |
24 |
23
|
coeq2d |
|- ( l = i -> ( [,) o. ( l ` j ) ) = ( [,) o. ( i ` j ) ) ) |
25 |
24
|
fveq1d |
|- ( l = i -> ( ( [,) o. ( l ` j ) ) ` k ) = ( ( [,) o. ( i ` j ) ) ` k ) ) |
26 |
25
|
ixpeq2dv |
|- ( l = i -> X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) |
27 |
26
|
iuneq2d |
|- ( l = i -> U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) |
28 |
27
|
sseq2d |
|- ( l = i -> ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) <-> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) ) |
29 |
28
|
elrab |
|- ( i e. { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } <-> ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) ) |
30 |
22 29
|
sylibr |
|- ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> i e. { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) |
31 |
30
|
3adant1 |
|- ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> i e. { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) |
32 |
|
sseq1 |
|- ( a = A -> ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) <-> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) ) ) |
33 |
32
|
rabbidv |
|- ( a = A -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } = { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) |
34 |
|
ovexd |
|- ( ph -> ( RR ^m X ) e. _V ) |
35 |
34 3
|
ssexd |
|- ( ph -> A e. _V ) |
36 |
|
elpwg |
|- ( A e. _V -> ( A e. ~P ( RR ^m X ) <-> A C_ ( RR ^m X ) ) ) |
37 |
35 36
|
syl |
|- ( ph -> ( A e. ~P ( RR ^m X ) <-> A C_ ( RR ^m X ) ) ) |
38 |
3 37
|
mpbird |
|- ( ph -> A e. ~P ( RR ^m X ) ) |
39 |
|
ovex |
|- ( ( ( RR X. RR ) ^m X ) ^m NN ) e. _V |
40 |
39
|
rabex |
|- { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } e. _V |
41 |
40
|
a1i |
|- ( ph -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } e. _V ) |
42 |
5 33 38 41
|
fvmptd3 |
|- ( ph -> ( C ` A ) = { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) |
43 |
42
|
eqcomd |
|- ( ph -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } = ( C ` A ) ) |
44 |
43
|
3ad2ant1 |
|- ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } = ( C ` A ) ) |
45 |
31 44
|
eleqtrd |
|- ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> i e. ( C ` A ) ) |
46 |
19 20 21 45
|
syl3anc |
|- ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> i e. ( C ` A ) ) |
47 |
|
coeq2 |
|- ( h = ( i ` j ) -> ( [,) o. h ) = ( [,) o. ( i ` j ) ) ) |
48 |
47
|
fveq1d |
|- ( h = ( i ` j ) -> ( ( [,) o. h ) ` k ) = ( ( [,) o. ( i ` j ) ) ` k ) ) |
49 |
48
|
fveq2d |
|- ( h = ( i ` j ) -> ( vol ` ( ( [,) o. h ) ` k ) ) = ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) |
50 |
49
|
prodeq2ad |
|- ( h = ( i ` j ) -> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) |
51 |
|
elmapi |
|- ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> i : NN --> ( ( RR X. RR ) ^m X ) ) |
52 |
51
|
adantr |
|- ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> i : NN --> ( ( RR X. RR ) ^m X ) ) |
53 |
|
simpr |
|- ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> j e. NN ) |
54 |
52 53
|
ffvelrnd |
|- ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> ( i ` j ) e. ( ( RR X. RR ) ^m X ) ) |
55 |
|
prodex |
|- prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) e. _V |
56 |
55
|
a1i |
|- ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) e. _V ) |
57 |
6 50 54 56
|
fvmptd3 |
|- ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> ( L ` ( i ` j ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) |
58 |
57
|
mpteq2dva |
|- ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( j e. NN |-> ( L ` ( i ` j ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) |
59 |
58
|
fveq2d |
|- ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) |
60 |
59
|
adantr |
|- ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) |
61 |
|
id |
|- ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) -> z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) |
62 |
61
|
eqcomd |
|- ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) = z ) |
63 |
62
|
adantl |
|- ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) = z ) |
64 |
60 63
|
eqtrd |
|- ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) = z ) |
65 |
64
|
3adant1 |
|- ( ( z <_ ( ( ( voln* ` X ) ` A ) +e E ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) = z ) |
66 |
|
simp1 |
|- ( ( z <_ ( ( ( voln* ` X ) ` A ) +e E ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) |
67 |
65 66
|
eqbrtrd |
|- ( ( z <_ ( ( ( voln* ` X ) ` A ) +e E ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) |
68 |
67
|
3adant1l |
|- ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) |
69 |
68
|
3adant3l |
|- ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) |
70 |
46 69
|
jca |
|- ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) |
71 |
70
|
19.8ad |
|- ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) |
72 |
71
|
3exp |
|- ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) ) ) |
73 |
17 18 72
|
rexlimd |
|- ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> ( E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) ) |
74 |
73
|
imp |
|- ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) |
75 |
10 11 16 74
|
syl21anc |
|- ( ( ph /\ z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) |
76 |
75
|
3exp |
|- ( ph -> ( z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } -> ( z <_ ( ( ( voln* ` X ) ` A ) +e E ) -> E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) ) ) |
77 |
76
|
rexlimdv |
|- ( ph -> ( E. z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } z <_ ( ( ( voln* ` X ) ` A ) +e E ) -> E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) ) |
78 |
9 77
|
mpd |
|- ( ph -> E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) |
79 |
|
rabid |
|- ( i e. { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } <-> ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) |
80 |
79
|
bicomi |
|- ( ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) <-> i e. { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } ) |
81 |
80
|
biimpi |
|- ( ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> i e. { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } ) |
82 |
81
|
adantl |
|- ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> i e. { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } ) |
83 |
|
nfcv |
|- F/_ b ( e e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) |
84 |
|
nfcv |
|- F/_ a RR+ |
85 |
|
nfv |
|- F/ a ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) |
86 |
|
nfmpt1 |
|- F/_ a ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) |
87 |
5 86
|
nfcxfr |
|- F/_ a C |
88 |
|
nfcv |
|- F/_ a b |
89 |
87 88
|
nffv |
|- F/_ a ( C ` b ) |
90 |
85 89
|
nfrabw |
|- F/_ a { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } |
91 |
84 90
|
nfmpt |
|- F/_ a ( e e. RR+ |-> { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } ) |
92 |
|
fveq2 |
|- ( a = b -> ( C ` a ) = ( C ` b ) ) |
93 |
92
|
eleq2d |
|- ( a = b -> ( i e. ( C ` a ) <-> i e. ( C ` b ) ) ) |
94 |
|
fveq2 |
|- ( a = b -> ( ( voln* ` X ) ` a ) = ( ( voln* ` X ) ` b ) ) |
95 |
94
|
oveq1d |
|- ( a = b -> ( ( ( voln* ` X ) ` a ) +e e ) = ( ( ( voln* ` X ) ` b ) +e e ) ) |
96 |
95
|
breq2d |
|- ( a = b -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) ) ) |
97 |
93 96
|
anbi12d |
|- ( a = b -> ( ( i e. ( C ` a ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) ) <-> ( i e. ( C ` b ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) ) ) ) |
98 |
97
|
rabbidva2 |
|- ( a = b -> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } = { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } ) |
99 |
98
|
mpteq2dv |
|- ( a = b -> ( e e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) = ( e e. RR+ |-> { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } ) ) |
100 |
83 91 99
|
cbvmpt |
|- ( a e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) ) = ( b e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } ) ) |
101 |
7 100
|
eqtri |
|- D = ( b e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } ) ) |
102 |
|
fveq2 |
|- ( b = A -> ( C ` b ) = ( C ` A ) ) |
103 |
102
|
eleq2d |
|- ( b = A -> ( i e. ( C ` b ) <-> i e. ( C ` A ) ) ) |
104 |
|
fveq2 |
|- ( b = A -> ( ( voln* ` X ) ` b ) = ( ( voln* ` X ) ` A ) ) |
105 |
104
|
oveq1d |
|- ( b = A -> ( ( ( voln* ` X ) ` b ) +e e ) = ( ( ( voln* ` X ) ` A ) +e e ) ) |
106 |
105
|
breq2d |
|- ( b = A -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) ) ) |
107 |
103 106
|
anbi12d |
|- ( b = A -> ( ( i e. ( C ` b ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) ) <-> ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) ) ) ) |
108 |
107
|
rabbidva2 |
|- ( b = A -> { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } = { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } ) |
109 |
108
|
mpteq2dv |
|- ( b = A -> ( e e. RR+ |-> { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } ) = ( e e. RR+ |-> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } ) ) |
110 |
38
|
adantr |
|- ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> A e. ~P ( RR ^m X ) ) |
111 |
|
rpex |
|- RR+ e. _V |
112 |
111
|
mptex |
|- ( e e. RR+ |-> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } ) e. _V |
113 |
112
|
a1i |
|- ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> ( e e. RR+ |-> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } ) e. _V ) |
114 |
101 109 110 113
|
fvmptd3 |
|- ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> ( D ` A ) = ( e e. RR+ |-> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } ) ) |
115 |
|
oveq2 |
|- ( e = E -> ( ( ( voln* ` X ) ` A ) +e e ) = ( ( ( voln* ` X ) ` A ) +e E ) ) |
116 |
115
|
breq2d |
|- ( e = E -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) |
117 |
116
|
rabbidv |
|- ( e = E -> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } = { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } ) |
118 |
117
|
adantl |
|- ( ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) /\ e = E ) -> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } = { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } ) |
119 |
4
|
adantr |
|- ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> E e. RR+ ) |
120 |
|
fvex |
|- ( C ` A ) e. _V |
121 |
120
|
rabex |
|- { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } e. _V |
122 |
121
|
a1i |
|- ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } e. _V ) |
123 |
114 118 119 122
|
fvmptd |
|- ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> ( ( D ` A ) ` E ) = { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } ) |
124 |
123
|
eqcomd |
|- ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } = ( ( D ` A ) ` E ) ) |
125 |
82 124
|
eleqtrd |
|- ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> i e. ( ( D ` A ) ` E ) ) |
126 |
125
|
ex |
|- ( ph -> ( ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> i e. ( ( D ` A ) ` E ) ) ) |
127 |
126
|
eximdv |
|- ( ph -> ( E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> E. i i e. ( ( D ` A ) ` E ) ) ) |
128 |
78 127
|
mpd |
|- ( ph -> E. i i e. ( ( D ` A ) ` E ) ) |