Metamath Proof Explorer

Theorem ovnsubadd

Description: ( voln*X ) is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnsubadd.1 
|- ( ph -> X e. Fin )
ovnsubadd.2 
|- ( ph -> A : NN --> ~P ( RR ^m X ) )
Assertion ovnsubadd 
|- ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnsubadd.1 
 |-  ( ph -> X e. Fin )
2 ovnsubadd.2 
 |-  ( ph -> A : NN --> ~P ( RR ^m X ) )
3 fveq2 
 |-  ( X = (/) -> ( voln* ` X ) = ( voln* ` (/) ) )
4 3 fveq1d 
 |-  ( X = (/) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) = ( ( voln* ` (/) ) ` U_ n e. NN ( A ` n ) ) )
5 4 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) = ( ( voln* ` (/) ) ` U_ n e. NN ( A ` n ) ) )
6 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> A : NN --> ~P ( RR ^m X ) )
7 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
8 6 7 ffvelrnd 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) e. ~P ( RR ^m X ) )
9 elpwi 
 |-  ( ( A ` n ) e. ~P ( RR ^m X ) -> ( A ` n ) C_ ( RR ^m X ) )
10 8 9 syl 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) C_ ( RR ^m X ) )
11 10 ralrimiva 
 |-  ( ph -> A. n e. NN ( A ` n ) C_ ( RR ^m X ) )
12 iunss 
 |-  ( U_ n e. NN ( A ` n ) C_ ( RR ^m X ) <-> A. n e. NN ( A ` n ) C_ ( RR ^m X ) )
13 11 12 sylibr 
 |-  ( ph -> U_ n e. NN ( A ` n ) C_ ( RR ^m X ) )
14 13 adantr 
 |-  ( ( ph /\ X = (/) ) -> U_ n e. NN ( A ` n ) C_ ( RR ^m X ) )
15 oveq2 
 |-  ( X = (/) -> ( RR ^m X ) = ( RR ^m (/) ) )
16 15 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( RR ^m X ) = ( RR ^m (/) ) )
17 14 16 sseqtrd 
 |-  ( ( ph /\ X = (/) ) -> U_ n e. NN ( A ` n ) C_ ( RR ^m (/) ) )
18 17 ovn0val 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` (/) ) ` U_ n e. NN ( A ` n ) ) = 0 )
19 5 18 eqtrd 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) = 0 )
20 nnex 
 |-  NN e. _V
21 20 a1i 
 |-  ( ph -> NN e. _V )
22 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. Fin )
23 22 10 ovncl 
 |-  ( ( ph /\ n e. NN ) -> ( ( voln* ` X ) ` ( A ` n ) ) e. ( 0 [,] +oo ) )
24 eqid 
 |-  ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) = ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) )
25 23 24 fmptd 
 |-  ( ph -> ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) : NN --> ( 0 [,] +oo ) )
26 21 25 sge0ge0 
 |-  ( ph -> 0 <_ ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) )
27 26 adantr 
 |-  ( ( ph /\ X = (/) ) -> 0 <_ ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) )
28 19 27 eqbrtrd 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) )
29 1 13 ovnxrcl 
 |-  ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) e. RR* )
30 29 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) e. RR* )
31 21 25 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) e. RR* )
32 31 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) e. RR* )
33 1 ad2antrr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ y e. RR+ ) -> X e. Fin )
34 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
35 34 ad2antlr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ y e. RR+ ) -> X =/= (/) )
36 2 ad2antrr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ y e. RR+ ) -> A : NN --> ~P ( RR ^m X ) )
37 simpr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ y e. RR+ ) -> y e. RR+ )
38 eqid 
 |-  ( a e. ~P ( RR ^m X ) |-> { 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 ) ) ) ) ) } ) = ( a e. ~P ( RR ^m X ) |-> { 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 ) ) ) ) ) } )
39 sseq1 
 |-  ( b = a -> ( b 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 ) ) )
40 39 rabbidv 
 |-  ( b = a -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b 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 ) } )
41 40 cbvmptv 
 |-  ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) = ( 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 ) } )
42 eqid 
 |-  ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )
43 fveq2 
 |-  ( o = j -> ( l ` o ) = ( l ` j ) )
44 43 coeq2d 
 |-  ( o = j -> ( [,) o. ( l ` o ) ) = ( [,) o. ( l ` j ) ) )
45 44 fveq1d 
 |-  ( o = j -> ( ( [,) o. ( l ` o ) ) ` d ) = ( ( [,) o. ( l ` j ) ) ` d ) )
46 45 ixpeq2dv 
 |-  ( o = j -> X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) = X_ d e. X ( ( [,) o. ( l ` j ) ) ` d ) )
47 fveq2 
 |-  ( d = k -> ( ( [,) o. ( l ` j ) ) ` d ) = ( ( [,) o. ( l ` j ) ) ` k ) )
48 47 cbvixpv 
 |-  X_ d e. X ( ( [,) o. ( l ` j ) ) ` d ) = X_ k e. X ( ( [,) o. ( l ` j ) ) ` k )
49 46 48 eqtrdi 
 |-  ( o = j -> X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) = X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) )
50 49 cbviunv 
 |-  U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) = U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k )
51 50 sseq2i 
 |-  ( b C_ U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) <-> b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) )
52 51 rabbii 
 |-  { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) } = { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) }
53 52 mpteq2i 
 |-  ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) } ) = ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
54 53 fveq1i 
 |-  ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) } ) ` d ) = ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` d )
55 fveq2 
 |-  ( d = a -> ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` d ) = ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) )
56 54 55 syl5eq 
 |-  ( d = a -> ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) } ) ` d ) = ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) )
57 56 eleq2d 
 |-  ( d = a -> ( m e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) } ) ` d ) <-> m e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) ) )
58 2fveq3 
 |-  ( d = k -> ( vol ` ( ( [,) o. h ) ` d ) ) = ( vol ` ( ( [,) o. h ) ` k ) ) )
59 58 cbvprodv 
 |-  prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) = prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) )
60 59 mpteq2i 
 |-  ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )
61 60 a1i 
 |-  ( o = j -> ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) )
62 fveq2 
 |-  ( o = j -> ( m ` o ) = ( m ` j ) )
63 61 62 fveq12d 
 |-  ( o = j -> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) ` ( m ` o ) ) = ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( m ` j ) ) )
64 63 cbvmptv 
 |-  ( o e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) ` ( m ` o ) ) ) = ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( m ` j ) ) )
65 64 fveq2i 
 |-  ( sum^ ` ( o e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) ` ( m ` o ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( m ` j ) ) ) )
66 65 a1i 
 |-  ( d = a -> ( sum^ ` ( o e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) ` ( m ` o ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( m ` j ) ) ) ) )
67 fveq2 
 |-  ( d = a -> ( ( voln* ` X ) ` d ) = ( ( voln* ` X ) ` a ) )
68 67 oveq1d 
 |-  ( d = a -> ( ( ( voln* ` X ) ` d ) +e f ) = ( ( ( voln* ` X ) ` a ) +e f ) )
69 66 68 breq12d 
 |-  ( d = a -> ( ( sum^ ` ( o e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) ` ( m ` o ) ) ) ) <_ ( ( ( voln* ` X ) ` d ) +e f ) <-> ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( m ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e f ) ) )
70 57 69 anbi12d 
 |-  ( d = a -> ( ( m e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) } ) ` d ) /\ ( sum^ ` ( o e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) ` ( m ` o ) ) ) ) <_ ( ( ( voln* ` X ) ` d ) +e f ) ) <-> ( m e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) /\ ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( m ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e f ) ) ) )
71 70 rabbidva2 
 |-  ( d = a -> { m e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) } ) ` d ) | ( sum^ ` ( o e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) ` ( m ` o ) ) ) ) <_ ( ( ( voln* ` X ) ` d ) +e f ) } = { m e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) | ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( m ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e f ) } )
72 fveq1 
 |-  ( m = i -> ( m ` j ) = ( i ` j ) )
73 72 fveq2d 
 |-  ( m = i -> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( m ` j ) ) = ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) )
74 73 mpteq2dv 
 |-  ( m = i -> ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( m ` j ) ) ) = ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) )
75 74 fveq2d 
 |-  ( m = i -> ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( m ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) )
76 75 breq1d 
 |-  ( m = i -> ( ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( m ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e f ) <-> ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e f ) ) )
77 76 cbvrabv 
 |-  { m e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) | ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( m ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e f ) } = { i e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) | ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e f ) }
78 71 77 eqtrdi 
 |-  ( d = a -> { m e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) } ) ` d ) | ( sum^ ` ( o e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) ` ( m ` o ) ) ) ) <_ ( ( ( voln* ` X ) ` d ) +e f ) } = { i e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) | ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e f ) } )
79 78 mpteq2dv 
 |-  ( d = a -> ( f e. RR+ |-> { m e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) } ) ` d ) | ( sum^ ` ( o e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) ` ( m ` o ) ) ) ) <_ ( ( ( voln* ` X ) ` d ) +e f ) } ) = ( f e. RR+ |-> { i e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) | ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e f ) } ) )
80 oveq2 
 |-  ( f = e -> ( ( ( voln* ` X ) ` a ) +e f ) = ( ( ( voln* ` X ) ` a ) +e e ) )
81 80 breq2d 
 |-  ( f = e -> ( ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e f ) <-> ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) ) )
82 81 rabbidv 
 |-  ( f = e -> { i e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) | ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e f ) } = { i e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) | ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } )
83 82 cbvmptv 
 |-  ( f e. RR+ |-> { i e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) | ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e f ) } ) = ( e e. RR+ |-> { i e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) | ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } )
84 79 83 eqtrdi 
 |-  ( d = a -> ( f e. RR+ |-> { m e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) } ) ` d ) | ( sum^ ` ( o e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) ` ( m ` o ) ) ) ) <_ ( ( ( voln* ` X ) ` d ) +e f ) } ) = ( e e. RR+ |-> { i e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) | ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) )
85 84 cbvmptv 
 |-  ( d e. ~P ( RR ^m X ) |-> ( f e. RR+ |-> { m e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ o e. NN X_ d e. X ( ( [,) o. ( l ` o ) ) ` d ) } ) ` d ) | ( sum^ ` ( o e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ d e. X ( vol ` ( ( [,) o. h ) ` d ) ) ) ` ( m ` o ) ) ) ) <_ ( ( ( voln* ` X ) ` d ) +e f ) } ) ) = ( a e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } ) ` a ) | ( sum^ ` ( j e. NN |-> ( ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) )
86 33 35 36 37 38 41 42 85 ovnsubaddlem2 
 |-  ( ( ( ph /\ -. X = (/) ) /\ y e. RR+ ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e y ) )
87 30 32 86 xrlexaddrp 
 |-  ( ( ph /\ -. X = (/) ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) )
88 28 87 pm2.61dan 
 |-  ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) )