Metamath Proof Explorer

Theorem ovolfiniun

Description: The Lebesgue outer measure function is finitely sub-additive. Finite sum version. (Contributed by Mario Carneiro, 19-Jun-2014)

Ref Expression
Assertion ovolfiniun 
|- ( ( A e. Fin /\ A. k e. A ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` U_ k e. A B ) <_ sum_ k e. A ( vol* ` B ) )

Proof

Step Hyp Ref Expression
1 raleq 
 |-  ( x = (/) -> ( A. k e. x ( B C_ RR /\ ( vol* ` B ) e. RR ) <-> A. k e. (/) ( B C_ RR /\ ( vol* ` B ) e. RR ) ) )
2 iuneq1 
 |-  ( x = (/) -> U_ k e. x B = U_ k e. (/) B )
3 2 fveq2d 
 |-  ( x = (/) -> ( vol* ` U_ k e. x B ) = ( vol* ` U_ k e. (/) B ) )
4 sumeq1 
 |-  ( x = (/) -> sum_ k e. x ( vol* ` B ) = sum_ k e. (/) ( vol* ` B ) )
5 3 4 breq12d 
 |-  ( x = (/) -> ( ( vol* ` U_ k e. x B ) <_ sum_ k e. x ( vol* ` B ) <-> ( vol* ` U_ k e. (/) B ) <_ sum_ k e. (/) ( vol* ` B ) ) )
6 1 5 imbi12d 
 |-  ( x = (/) -> ( ( A. k e. x ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. x B ) <_ sum_ k e. x ( vol* ` B ) ) <-> ( A. k e. (/) ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. (/) B ) <_ sum_ k e. (/) ( vol* ` B ) ) ) )
7 raleq 
 |-  ( x = y -> ( A. k e. x ( B C_ RR /\ ( vol* ` B ) e. RR ) <-> A. k e. y ( B C_ RR /\ ( vol* ` B ) e. RR ) ) )
8 iuneq1 
 |-  ( x = y -> U_ k e. x B = U_ k e. y B )
9 8 fveq2d 
 |-  ( x = y -> ( vol* ` U_ k e. x B ) = ( vol* ` U_ k e. y B ) )
10 sumeq1 
 |-  ( x = y -> sum_ k e. x ( vol* ` B ) = sum_ k e. y ( vol* ` B ) )
11 9 10 breq12d 
 |-  ( x = y -> ( ( vol* ` U_ k e. x B ) <_ sum_ k e. x ( vol* ` B ) <-> ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) )
12 7 11 imbi12d 
 |-  ( x = y -> ( ( A. k e. x ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. x B ) <_ sum_ k e. x ( vol* ` B ) ) <-> ( A. k e. y ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) )
13 raleq 
 |-  ( x = ( y u. { z } ) -> ( A. k e. x ( B C_ RR /\ ( vol* ` B ) e. RR ) <-> A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) ) )
14 iuneq1 
 |-  ( x = ( y u. { z } ) -> U_ k e. x B = U_ k e. ( y u. { z } ) B )
15 14 fveq2d 
 |-  ( x = ( y u. { z } ) -> ( vol* ` U_ k e. x B ) = ( vol* ` U_ k e. ( y u. { z } ) B ) )
16 sumeq1 
 |-  ( x = ( y u. { z } ) -> sum_ k e. x ( vol* ` B ) = sum_ k e. ( y u. { z } ) ( vol* ` B ) )
17 15 16 breq12d 
 |-  ( x = ( y u. { z } ) -> ( ( vol* ` U_ k e. x B ) <_ sum_ k e. x ( vol* ` B ) <-> ( vol* ` U_ k e. ( y u. { z } ) B ) <_ sum_ k e. ( y u. { z } ) ( vol* ` B ) ) )
18 13 17 imbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( A. k e. x ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. x B ) <_ sum_ k e. x ( vol* ` B ) ) <-> ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. ( y u. { z } ) B ) <_ sum_ k e. ( y u. { z } ) ( vol* ` B ) ) ) )
19 raleq 
 |-  ( x = A -> ( A. k e. x ( B C_ RR /\ ( vol* ` B ) e. RR ) <-> A. k e. A ( B C_ RR /\ ( vol* ` B ) e. RR ) ) )
20 iuneq1 
 |-  ( x = A -> U_ k e. x B = U_ k e. A B )
21 20 fveq2d 
 |-  ( x = A -> ( vol* ` U_ k e. x B ) = ( vol* ` U_ k e. A B ) )
22 sumeq1 
 |-  ( x = A -> sum_ k e. x ( vol* ` B ) = sum_ k e. A ( vol* ` B ) )
23 21 22 breq12d 
 |-  ( x = A -> ( ( vol* ` U_ k e. x B ) <_ sum_ k e. x ( vol* ` B ) <-> ( vol* ` U_ k e. A B ) <_ sum_ k e. A ( vol* ` B ) ) )
24 19 23 imbi12d 
 |-  ( x = A -> ( ( A. k e. x ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. x B ) <_ sum_ k e. x ( vol* ` B ) ) <-> ( A. k e. A ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. A B ) <_ sum_ k e. A ( vol* ` B ) ) ) )
25 0le0 
 |-  0 <_ 0
26 0iun 
 |-  U_ k e. (/) B = (/)
27 26 fveq2i 
 |-  ( vol* ` U_ k e. (/) B ) = ( vol* ` (/) )
28 ovol0 
 |-  ( vol* ` (/) ) = 0
29 27 28 eqtri 
 |-  ( vol* ` U_ k e. (/) B ) = 0
30 sum0 
 |-  sum_ k e. (/) ( vol* ` B ) = 0
31 25 29 30 3brtr4i 
 |-  ( vol* ` U_ k e. (/) B ) <_ sum_ k e. (/) ( vol* ` B )
32 31 a1i 
 |-  ( A. k e. (/) ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. (/) B ) <_ sum_ k e. (/) ( vol* ` B ) )
33 ssun1 
 |-  y C_ ( y u. { z } )
34 ssralv 
 |-  ( y C_ ( y u. { z } ) -> ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) -> A. k e. y ( B C_ RR /\ ( vol* ` B ) e. RR ) ) )
35 33 34 ax-mp 
 |-  ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) -> A. k e. y ( B C_ RR /\ ( vol* ` B ) e. RR ) )
36 35 imim1i 
 |-  ( ( A. k e. y ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) -> ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) )
37 simprl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) )
38 nfcsb1v 
 |-  F/_ k [_ m / k ]_ B
39 nfcv 
 |-  F/_ k RR
40 38 39 nfss 
 |-  F/ k [_ m / k ]_ B C_ RR
41 nfcv 
 |-  F/_ k vol*
42 41 38 nffv 
 |-  F/_ k ( vol* ` [_ m / k ]_ B )
43 42 nfel1 
 |-  F/ k ( vol* ` [_ m / k ]_ B ) e. RR
44 40 43 nfan 
 |-  F/ k ( [_ m / k ]_ B C_ RR /\ ( vol* ` [_ m / k ]_ B ) e. RR )
45 csbeq1a 
 |-  ( k = m -> B = [_ m / k ]_ B )
46 45 sseq1d 
 |-  ( k = m -> ( B C_ RR <-> [_ m / k ]_ B C_ RR ) )
47 45 fveq2d 
 |-  ( k = m -> ( vol* ` B ) = ( vol* ` [_ m / k ]_ B ) )
48 47 eleq1d 
 |-  ( k = m -> ( ( vol* ` B ) e. RR <-> ( vol* ` [_ m / k ]_ B ) e. RR ) )
49 46 48 anbi12d 
 |-  ( k = m -> ( ( B C_ RR /\ ( vol* ` B ) e. RR ) <-> ( [_ m / k ]_ B C_ RR /\ ( vol* ` [_ m / k ]_ B ) e. RR ) ) )
50 44 49 rspc 
 |-  ( m e. ( y u. { z } ) -> ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( [_ m / k ]_ B C_ RR /\ ( vol* ` [_ m / k ]_ B ) e. RR ) ) )
51 37 50 mpan9 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) /\ m e. ( y u. { z } ) ) -> ( [_ m / k ]_ B C_ RR /\ ( vol* ` [_ m / k ]_ B ) e. RR ) )
52 51 simpld 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) /\ m e. ( y u. { z } ) ) -> [_ m / k ]_ B C_ RR )
53 52 ralrimiva 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> A. m e. ( y u. { z } ) [_ m / k ]_ B C_ RR )
54 iunss 
 |-  ( U_ m e. ( y u. { z } ) [_ m / k ]_ B C_ RR <-> A. m e. ( y u. { z } ) [_ m / k ]_ B C_ RR )
55 53 54 sylibr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> U_ m e. ( y u. { z } ) [_ m / k ]_ B C_ RR )
56 iunss1 
 |-  ( y C_ ( y u. { z } ) -> U_ m e. y [_ m / k ]_ B C_ U_ m e. ( y u. { z } ) [_ m / k ]_ B )
57 33 56 ax-mp 
 |-  U_ m e. y [_ m / k ]_ B C_ U_ m e. ( y u. { z } ) [_ m / k ]_ B
58 57 55 sstrid 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> U_ m e. y [_ m / k ]_ B C_ RR )
59 simpll 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> y e. Fin )
60 elun1 
 |-  ( m e. y -> m e. ( y u. { z } ) )
61 51 simprd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) /\ m e. ( y u. { z } ) ) -> ( vol* ` [_ m / k ]_ B ) e. RR )
62 60 61 sylan2 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) /\ m e. y ) -> ( vol* ` [_ m / k ]_ B ) e. RR )
63 59 62 fsumrecl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> sum_ m e. y ( vol* ` [_ m / k ]_ B ) e. RR )
64 simprr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) )
65 nfcv 
 |-  F/_ m B
66 65 38 45 cbviun 
 |-  U_ k e. y B = U_ m e. y [_ m / k ]_ B
67 66 fveq2i 
 |-  ( vol* ` U_ k e. y B ) = ( vol* ` U_ m e. y [_ m / k ]_ B )
68 nfcv 
 |-  F/_ m ( vol* ` B )
69 68 42 47 cbvsumi 
 |-  sum_ k e. y ( vol* ` B ) = sum_ m e. y ( vol* ` [_ m / k ]_ B )
70 64 67 69 3brtr3g 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( vol* ` U_ m e. y [_ m / k ]_ B ) <_ sum_ m e. y ( vol* ` [_ m / k ]_ B ) )
71 ovollecl 
 |-  ( ( U_ m e. y [_ m / k ]_ B C_ RR /\ sum_ m e. y ( vol* ` [_ m / k ]_ B ) e. RR /\ ( vol* ` U_ m e. y [_ m / k ]_ B ) <_ sum_ m e. y ( vol* ` [_ m / k ]_ B ) ) -> ( vol* ` U_ m e. y [_ m / k ]_ B ) e. RR )
72 58 63 70 71 syl3anc 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( vol* ` U_ m e. y [_ m / k ]_ B ) e. RR )
73 ssun2 
 |-  { z } C_ ( y u. { z } )
74 vsnid 
 |-  z e. { z }
75 73 74 sselii 
 |-  z e. ( y u. { z } )
76 nfcsb1v 
 |-  F/_ k [_ z / k ]_ B
77 76 39 nfss 
 |-  F/ k [_ z / k ]_ B C_ RR
78 41 76 nffv 
 |-  F/_ k ( vol* ` [_ z / k ]_ B )
79 78 nfel1 
 |-  F/ k ( vol* ` [_ z / k ]_ B ) e. RR
80 77 79 nfan 
 |-  F/ k ( [_ z / k ]_ B C_ RR /\ ( vol* ` [_ z / k ]_ B ) e. RR )
81 csbeq1a 
 |-  ( k = z -> B = [_ z / k ]_ B )
82 81 sseq1d 
 |-  ( k = z -> ( B C_ RR <-> [_ z / k ]_ B C_ RR ) )
83 81 fveq2d 
 |-  ( k = z -> ( vol* ` B ) = ( vol* ` [_ z / k ]_ B ) )
84 83 eleq1d 
 |-  ( k = z -> ( ( vol* ` B ) e. RR <-> ( vol* ` [_ z / k ]_ B ) e. RR ) )
85 82 84 anbi12d 
 |-  ( k = z -> ( ( B C_ RR /\ ( vol* ` B ) e. RR ) <-> ( [_ z / k ]_ B C_ RR /\ ( vol* ` [_ z / k ]_ B ) e. RR ) ) )
86 80 85 rspc 
 |-  ( z e. ( y u. { z } ) -> ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( [_ z / k ]_ B C_ RR /\ ( vol* ` [_ z / k ]_ B ) e. RR ) ) )
87 75 37 86 mpsyl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( [_ z / k ]_ B C_ RR /\ ( vol* ` [_ z / k ]_ B ) e. RR ) )
88 87 simprd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( vol* ` [_ z / k ]_ B ) e. RR )
89 72 88 readdcld 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( ( vol* ` U_ m e. y [_ m / k ]_ B ) + ( vol* ` [_ z / k ]_ B ) ) e. RR )
90 iunxun 
 |-  U_ m e. ( y u. { z } ) [_ m / k ]_ B = ( U_ m e. y [_ m / k ]_ B u. U_ m e. { z } [_ m / k ]_ B )
91 vex 
 |-  z e. _V
92 csbeq1 
 |-  ( m = z -> [_ m / k ]_ B = [_ z / k ]_ B )
93 91 92 iunxsn 
 |-  U_ m e. { z } [_ m / k ]_ B = [_ z / k ]_ B
94 93 uneq2i 
 |-  ( U_ m e. y [_ m / k ]_ B u. U_ m e. { z } [_ m / k ]_ B ) = ( U_ m e. y [_ m / k ]_ B u. [_ z / k ]_ B )
95 90 94 eqtri 
 |-  U_ m e. ( y u. { z } ) [_ m / k ]_ B = ( U_ m e. y [_ m / k ]_ B u. [_ z / k ]_ B )
96 95 fveq2i 
 |-  ( vol* ` U_ m e. ( y u. { z } ) [_ m / k ]_ B ) = ( vol* ` ( U_ m e. y [_ m / k ]_ B u. [_ z / k ]_ B ) )
97 ovolun 
 |-  ( ( ( U_ m e. y [_ m / k ]_ B C_ RR /\ ( vol* ` U_ m e. y [_ m / k ]_ B ) e. RR ) /\ ( [_ z / k ]_ B C_ RR /\ ( vol* ` [_ z / k ]_ B ) e. RR ) ) -> ( vol* ` ( U_ m e. y [_ m / k ]_ B u. [_ z / k ]_ B ) ) <_ ( ( vol* ` U_ m e. y [_ m / k ]_ B ) + ( vol* ` [_ z / k ]_ B ) ) )
98 58 72 87 97 syl21anc 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( vol* ` ( U_ m e. y [_ m / k ]_ B u. [_ z / k ]_ B ) ) <_ ( ( vol* ` U_ m e. y [_ m / k ]_ B ) + ( vol* ` [_ z / k ]_ B ) ) )
99 96 98 eqbrtrid 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( vol* ` U_ m e. ( y u. { z } ) [_ m / k ]_ B ) <_ ( ( vol* ` U_ m e. y [_ m / k ]_ B ) + ( vol* ` [_ z / k ]_ B ) ) )
100 ovollecl 
 |-  ( ( U_ m e. ( y u. { z } ) [_ m / k ]_ B C_ RR /\ ( ( vol* ` U_ m e. y [_ m / k ]_ B ) + ( vol* ` [_ z / k ]_ B ) ) e. RR /\ ( vol* ` U_ m e. ( y u. { z } ) [_ m / k ]_ B ) <_ ( ( vol* ` U_ m e. y [_ m / k ]_ B ) + ( vol* ` [_ z / k ]_ B ) ) ) -> ( vol* ` U_ m e. ( y u. { z } ) [_ m / k ]_ B ) e. RR )
101 55 89 99 100 syl3anc 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( vol* ` U_ m e. ( y u. { z } ) [_ m / k ]_ B ) e. RR )
102 snfi 
 |-  { z } e. Fin
103 unfi 
 |-  ( ( y e. Fin /\ { z } e. Fin ) -> ( y u. { z } ) e. Fin )
104 102 103 mpan2 
 |-  ( y e. Fin -> ( y u. { z } ) e. Fin )
105 104 ad2antrr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( y u. { z } ) e. Fin )
106 105 61 fsumrecl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> sum_ m e. ( y u. { z } ) ( vol* ` [_ m / k ]_ B ) e. RR )
107 72 63 88 70 leadd1dd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( ( vol* ` U_ m e. y [_ m / k ]_ B ) + ( vol* ` [_ z / k ]_ B ) ) <_ ( sum_ m e. y ( vol* ` [_ m / k ]_ B ) + ( vol* ` [_ z / k ]_ B ) ) )
108 simplr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> -. z e. y )
109 disjsn 
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
110 108 109 sylibr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( y i^i { z } ) = (/) )
111 eqidd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( y u. { z } ) = ( y u. { z } ) )
112 61 recnd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) /\ m e. ( y u. { z } ) ) -> ( vol* ` [_ m / k ]_ B ) e. CC )
113 110 111 105 112 fsumsplit 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> sum_ m e. ( y u. { z } ) ( vol* ` [_ m / k ]_ B ) = ( sum_ m e. y ( vol* ` [_ m / k ]_ B ) + sum_ m e. { z } ( vol* ` [_ m / k ]_ B ) ) )
114 88 recnd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( vol* ` [_ z / k ]_ B ) e. CC )
115 92 fveq2d 
 |-  ( m = z -> ( vol* ` [_ m / k ]_ B ) = ( vol* ` [_ z / k ]_ B ) )
116 115 sumsn 
 |-  ( ( z e. _V /\ ( vol* ` [_ z / k ]_ B ) e. CC ) -> sum_ m e. { z } ( vol* ` [_ m / k ]_ B ) = ( vol* ` [_ z / k ]_ B ) )
117 91 114 116 sylancr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> sum_ m e. { z } ( vol* ` [_ m / k ]_ B ) = ( vol* ` [_ z / k ]_ B ) )
118 117 oveq2d 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( sum_ m e. y ( vol* ` [_ m / k ]_ B ) + sum_ m e. { z } ( vol* ` [_ m / k ]_ B ) ) = ( sum_ m e. y ( vol* ` [_ m / k ]_ B ) + ( vol* ` [_ z / k ]_ B ) ) )
119 113 118 eqtrd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> sum_ m e. ( y u. { z } ) ( vol* ` [_ m / k ]_ B ) = ( sum_ m e. y ( vol* ` [_ m / k ]_ B ) + ( vol* ` [_ z / k ]_ B ) ) )
120 107 119 breqtrrd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( ( vol* ` U_ m e. y [_ m / k ]_ B ) + ( vol* ` [_ z / k ]_ B ) ) <_ sum_ m e. ( y u. { z } ) ( vol* ` [_ m / k ]_ B ) )
121 101 89 106 99 120 letrd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( vol* ` U_ m e. ( y u. { z } ) [_ m / k ]_ B ) <_ sum_ m e. ( y u. { z } ) ( vol* ` [_ m / k ]_ B ) )
122 65 38 45 cbviun 
 |-  U_ k e. ( y u. { z } ) B = U_ m e. ( y u. { z } ) [_ m / k ]_ B
123 122 fveq2i 
 |-  ( vol* ` U_ k e. ( y u. { z } ) B ) = ( vol* ` U_ m e. ( y u. { z } ) [_ m / k ]_ B )
124 68 42 47 cbvsumi 
 |-  sum_ k e. ( y u. { z } ) ( vol* ` B ) = sum_ m e. ( y u. { z } ) ( vol* ` [_ m / k ]_ B )
125 121 123 124 3brtr4g 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) ) -> ( vol* ` U_ k e. ( y u. { z } ) B ) <_ sum_ k e. ( y u. { z } ) ( vol* ` B ) )
126 125 exp32 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) -> ( vol* ` U_ k e. ( y u. { z } ) B ) <_ sum_ k e. ( y u. { z } ) ( vol* ` B ) ) ) )
127 126 a2d 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) -> ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. ( y u. { z } ) B ) <_ sum_ k e. ( y u. { z } ) ( vol* ` B ) ) ) )
128 36 127 syl5 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( A. k e. y ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. y B ) <_ sum_ k e. y ( vol* ` B ) ) -> ( A. k e. ( y u. { z } ) ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. ( y u. { z } ) B ) <_ sum_ k e. ( y u. { z } ) ( vol* ` B ) ) ) )
129 6 12 18 24 32 128 findcard2s 
 |-  ( A e. Fin -> ( A. k e. A ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` U_ k e. A B ) <_ sum_ k e. A ( vol* ` B ) ) )
130 129 imp 
 |-  ( ( A e. Fin /\ A. k e. A ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` U_ k e. A B ) <_ sum_ k e. A ( vol* ` B ) )