Metamath Proof Explorer


Theorem uniioombllem5

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses uniioombl.1
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.2
|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
uniioombl.3
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
uniioombl.a
|- A = U. ran ( (,) o. F )
uniioombl.e
|- ( ph -> ( vol* ` E ) e. RR )
uniioombl.c
|- ( ph -> C e. RR+ )
uniioombl.g
|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.s
|- ( ph -> E C_ U. ran ( (,) o. G ) )
uniioombl.t
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
uniioombl.v
|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
uniioombl.m
|- ( ph -> M e. NN )
uniioombl.m2
|- ( ph -> ( abs ` ( ( T ` M ) - sup ( ran T , RR* , < ) ) ) < C )
uniioombl.k
|- K = U. ( ( (,) o. G ) " ( 1 ... M ) )
uniioombl.n
|- ( ph -> N e. NN )
uniioombl.n2
|- ( ph -> A. j e. ( 1 ... M ) ( abs ` ( sum_ i e. ( 1 ... N ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / M ) )
uniioombl.l
|- L = U. ( ( (,) o. F ) " ( 1 ... N ) )
Assertion uniioombllem5
|- ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )

Proof

Step Hyp Ref Expression
1 uniioombl.1
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
2 uniioombl.2
 |-  ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
3 uniioombl.3
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
4 uniioombl.a
 |-  A = U. ran ( (,) o. F )
5 uniioombl.e
 |-  ( ph -> ( vol* ` E ) e. RR )
6 uniioombl.c
 |-  ( ph -> C e. RR+ )
7 uniioombl.g
 |-  ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
8 uniioombl.s
 |-  ( ph -> E C_ U. ran ( (,) o. G ) )
9 uniioombl.t
 |-  T = seq 1 ( + , ( ( abs o. - ) o. G ) )
10 uniioombl.v
 |-  ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
11 uniioombl.m
 |-  ( ph -> M e. NN )
12 uniioombl.m2
 |-  ( ph -> ( abs ` ( ( T ` M ) - sup ( ran T , RR* , < ) ) ) < C )
13 uniioombl.k
 |-  K = U. ( ( (,) o. G ) " ( 1 ... M ) )
14 uniioombl.n
 |-  ( ph -> N e. NN )
15 uniioombl.n2
 |-  ( ph -> A. j e. ( 1 ... M ) ( abs ` ( sum_ i e. ( 1 ... N ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / M ) )
16 uniioombl.l
 |-  L = U. ( ( (,) o. F ) " ( 1 ... N ) )
17 inss1
 |-  ( E i^i A ) C_ E
18 7 uniiccdif
 |-  ( ph -> ( U. ran ( (,) o. G ) C_ U. ran ( [,] o. G ) /\ ( vol* ` ( U. ran ( [,] o. G ) \ U. ran ( (,) o. G ) ) ) = 0 ) )
19 18 simpld
 |-  ( ph -> U. ran ( (,) o. G ) C_ U. ran ( [,] o. G ) )
20 ovolficcss
 |-  ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. G ) C_ RR )
21 7 20 syl
 |-  ( ph -> U. ran ( [,] o. G ) C_ RR )
22 19 21 sstrd
 |-  ( ph -> U. ran ( (,) o. G ) C_ RR )
23 8 22 sstrd
 |-  ( ph -> E C_ RR )
24 ovolsscl
 |-  ( ( ( E i^i A ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E i^i A ) ) e. RR )
25 17 23 5 24 mp3an2i
 |-  ( ph -> ( vol* ` ( E i^i A ) ) e. RR )
26 difssd
 |-  ( ph -> ( E \ A ) C_ E )
27 ovolsscl
 |-  ( ( ( E \ A ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E \ A ) ) e. RR )
28 26 23 5 27 syl3anc
 |-  ( ph -> ( vol* ` ( E \ A ) ) e. RR )
29 25 28 readdcld
 |-  ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) e. RR )
30 inss1
 |-  ( K i^i A ) C_ K
31 imassrn
 |-  ( ( (,) o. G ) " ( 1 ... M ) ) C_ ran ( (,) o. G )
32 31 unissi
 |-  U. ( ( (,) o. G ) " ( 1 ... M ) ) C_ U. ran ( (,) o. G )
33 13 32 eqsstri
 |-  K C_ U. ran ( (,) o. G )
34 33 22 sstrid
 |-  ( ph -> K C_ RR )
35 1 2 3 4 5 6 7 8 9 10 uniioombllem1
 |-  ( ph -> sup ( ran T , RR* , < ) e. RR )
36 ssid
 |-  U. ran ( (,) o. G ) C_ U. ran ( (,) o. G )
37 9 ovollb
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ U. ran ( (,) o. G ) C_ U. ran ( (,) o. G ) ) -> ( vol* ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) )
38 7 36 37 sylancl
 |-  ( ph -> ( vol* ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) )
39 ovollecl
 |-  ( ( U. ran ( (,) o. G ) C_ RR /\ sup ( ran T , RR* , < ) e. RR /\ ( vol* ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) ) -> ( vol* ` U. ran ( (,) o. G ) ) e. RR )
40 22 35 38 39 syl3anc
 |-  ( ph -> ( vol* ` U. ran ( (,) o. G ) ) e. RR )
41 ovolsscl
 |-  ( ( K C_ U. ran ( (,) o. G ) /\ U. ran ( (,) o. G ) C_ RR /\ ( vol* ` U. ran ( (,) o. G ) ) e. RR ) -> ( vol* ` K ) e. RR )
42 33 22 40 41 mp3an2i
 |-  ( ph -> ( vol* ` K ) e. RR )
43 ovolsscl
 |-  ( ( ( K i^i A ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K i^i A ) ) e. RR )
44 30 34 42 43 mp3an2i
 |-  ( ph -> ( vol* ` ( K i^i A ) ) e. RR )
45 difssd
 |-  ( ph -> ( K \ A ) C_ K )
46 ovolsscl
 |-  ( ( ( K \ A ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K \ A ) ) e. RR )
47 45 34 42 46 syl3anc
 |-  ( ph -> ( vol* ` ( K \ A ) ) e. RR )
48 44 47 readdcld
 |-  ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) e. RR )
49 6 rpred
 |-  ( ph -> C e. RR )
50 49 49 readdcld
 |-  ( ph -> ( C + C ) e. RR )
51 48 50 readdcld
 |-  ( ph -> ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) e. RR )
52 4re
 |-  4 e. RR
53 remulcl
 |-  ( ( 4 e. RR /\ C e. RR ) -> ( 4 x. C ) e. RR )
54 52 49 53 sylancr
 |-  ( ph -> ( 4 x. C ) e. RR )
55 5 54 readdcld
 |-  ( ph -> ( ( vol* ` E ) + ( 4 x. C ) ) e. RR )
56 1 2 3 4 5 6 7 8 9 10 11 12 13 uniioombllem3
 |-  ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) < ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) )
57 29 51 56 ltled
 |-  ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) )
58 5 50 readdcld
 |-  ( ph -> ( ( vol* ` E ) + ( C + C ) ) e. RR )
59 42 49 readdcld
 |-  ( ph -> ( ( vol* ` K ) + C ) e. RR )
60 inss1
 |-  ( K i^i L ) C_ K
61 ovolsscl
 |-  ( ( ( K i^i L ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K i^i L ) ) e. RR )
62 60 34 42 61 mp3an2i
 |-  ( ph -> ( vol* ` ( K i^i L ) ) e. RR )
63 62 49 readdcld
 |-  ( ph -> ( ( vol* ` ( K i^i L ) ) + C ) e. RR )
64 difssd
 |-  ( ph -> ( K \ L ) C_ K )
65 ovolsscl
 |-  ( ( ( K \ L ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K \ L ) ) e. RR )
66 64 34 42 65 syl3anc
 |-  ( ph -> ( vol* ` ( K \ L ) ) e. RR )
67 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 uniioombllem4
 |-  ( ph -> ( vol* ` ( K i^i A ) ) <_ ( ( vol* ` ( K i^i L ) ) + C ) )
68 imassrn
 |-  ( ( (,) o. F ) " ( 1 ... N ) ) C_ ran ( (,) o. F )
69 68 unissi
 |-  U. ( ( (,) o. F ) " ( 1 ... N ) ) C_ U. ran ( (,) o. F )
70 69 16 4 3sstr4i
 |-  L C_ A
71 sscon
 |-  ( L C_ A -> ( K \ A ) C_ ( K \ L ) )
72 70 71 mp1i
 |-  ( ph -> ( K \ A ) C_ ( K \ L ) )
73 64 34 sstrd
 |-  ( ph -> ( K \ L ) C_ RR )
74 ovolss
 |-  ( ( ( K \ A ) C_ ( K \ L ) /\ ( K \ L ) C_ RR ) -> ( vol* ` ( K \ A ) ) <_ ( vol* ` ( K \ L ) ) )
75 72 73 74 syl2anc
 |-  ( ph -> ( vol* ` ( K \ A ) ) <_ ( vol* ` ( K \ L ) ) )
76 44 47 63 66 67 75 le2addd
 |-  ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) <_ ( ( ( vol* ` ( K i^i L ) ) + C ) + ( vol* ` ( K \ L ) ) ) )
77 62 recnd
 |-  ( ph -> ( vol* ` ( K i^i L ) ) e. CC )
78 49 recnd
 |-  ( ph -> C e. CC )
79 66 recnd
 |-  ( ph -> ( vol* ` ( K \ L ) ) e. CC )
80 77 78 79 add32d
 |-  ( ph -> ( ( ( vol* ` ( K i^i L ) ) + C ) + ( vol* ` ( K \ L ) ) ) = ( ( ( vol* ` ( K i^i L ) ) + ( vol* ` ( K \ L ) ) ) + C ) )
81 ioof
 |-  (,) : ( RR* X. RR* ) --> ~P RR
82 inss2
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
83 rexpssxrxp
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
84 82 83 sstri
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
85 fss
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> F : NN --> ( RR* X. RR* ) )
86 1 84 85 sylancl
 |-  ( ph -> F : NN --> ( RR* X. RR* ) )
87 fco
 |-  ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ F : NN --> ( RR* X. RR* ) ) -> ( (,) o. F ) : NN --> ~P RR )
88 81 86 87 sylancr
 |-  ( ph -> ( (,) o. F ) : NN --> ~P RR )
89 ffun
 |-  ( ( (,) o. F ) : NN --> ~P RR -> Fun ( (,) o. F ) )
90 funiunfv
 |-  ( Fun ( (,) o. F ) -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) = U. ( ( (,) o. F ) " ( 1 ... N ) ) )
91 88 89 90 3syl
 |-  ( ph -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) = U. ( ( (,) o. F ) " ( 1 ... N ) ) )
92 91 16 eqtr4di
 |-  ( ph -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) = L )
93 fzfid
 |-  ( ph -> ( 1 ... N ) e. Fin )
94 elfznn
 |-  ( n e. ( 1 ... N ) -> n e. NN )
95 fvco3
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( (,) o. F ) ` n ) = ( (,) ` ( F ` n ) ) )
96 1 94 95 syl2an
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( (,) o. F ) ` n ) = ( (,) ` ( F ` n ) ) )
97 ffvelrn
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( F ` n ) e. ( <_ i^i ( RR X. RR ) ) )
98 1 94 97 syl2an
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( F ` n ) e. ( <_ i^i ( RR X. RR ) ) )
99 98 elin2d
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( F ` n ) e. ( RR X. RR ) )
100 1st2nd2
 |-  ( ( F ` n ) e. ( RR X. RR ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
101 99 100 syl
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
102 101 fveq2d
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( (,) ` ( F ` n ) ) = ( (,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. ) )
103 df-ov
 |-  ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) = ( (,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
104 102 103 eqtr4di
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( (,) ` ( F ` n ) ) = ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) )
105 96 104 eqtrd
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( (,) o. F ) ` n ) = ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) )
106 ioombl
 |-  ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) e. dom vol
107 105 106 eqeltrdi
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( (,) o. F ) ` n ) e. dom vol )
108 107 ralrimiva
 |-  ( ph -> A. n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) e. dom vol )
109 finiunmbl
 |-  ( ( ( 1 ... N ) e. Fin /\ A. n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) e. dom vol ) -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) e. dom vol )
110 93 108 109 syl2anc
 |-  ( ph -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) e. dom vol )
111 92 110 eqeltrrd
 |-  ( ph -> L e. dom vol )
112 mblsplit
 |-  ( ( L e. dom vol /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` K ) = ( ( vol* ` ( K i^i L ) ) + ( vol* ` ( K \ L ) ) ) )
113 111 34 42 112 syl3anc
 |-  ( ph -> ( vol* ` K ) = ( ( vol* ` ( K i^i L ) ) + ( vol* ` ( K \ L ) ) ) )
114 113 oveq1d
 |-  ( ph -> ( ( vol* ` K ) + C ) = ( ( ( vol* ` ( K i^i L ) ) + ( vol* ` ( K \ L ) ) ) + C ) )
115 80 114 eqtr4d
 |-  ( ph -> ( ( ( vol* ` ( K i^i L ) ) + C ) + ( vol* ` ( K \ L ) ) ) = ( ( vol* ` K ) + C ) )
116 76 115 breqtrd
 |-  ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) <_ ( ( vol* ` K ) + C ) )
117 5 49 readdcld
 |-  ( ph -> ( ( vol* ` E ) + C ) e. RR )
118 9 ovollb
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ K C_ U. ran ( (,) o. G ) ) -> ( vol* ` K ) <_ sup ( ran T , RR* , < ) )
119 7 33 118 sylancl
 |-  ( ph -> ( vol* ` K ) <_ sup ( ran T , RR* , < ) )
120 42 35 117 119 10 letrd
 |-  ( ph -> ( vol* ` K ) <_ ( ( vol* ` E ) + C ) )
121 42 117 49 120 leadd1dd
 |-  ( ph -> ( ( vol* ` K ) + C ) <_ ( ( ( vol* ` E ) + C ) + C ) )
122 5 recnd
 |-  ( ph -> ( vol* ` E ) e. CC )
123 122 78 78 addassd
 |-  ( ph -> ( ( ( vol* ` E ) + C ) + C ) = ( ( vol* ` E ) + ( C + C ) ) )
124 121 123 breqtrd
 |-  ( ph -> ( ( vol* ` K ) + C ) <_ ( ( vol* ` E ) + ( C + C ) ) )
125 48 59 58 116 124 letrd
 |-  ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) <_ ( ( vol* ` E ) + ( C + C ) ) )
126 48 58 50 125 leadd1dd
 |-  ( ph -> ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) <_ ( ( ( vol* ` E ) + ( C + C ) ) + ( C + C ) ) )
127 50 recnd
 |-  ( ph -> ( C + C ) e. CC )
128 122 127 127 addassd
 |-  ( ph -> ( ( ( vol* ` E ) + ( C + C ) ) + ( C + C ) ) = ( ( vol* ` E ) + ( ( C + C ) + ( C + C ) ) ) )
129 2t2e4
 |-  ( 2 x. 2 ) = 4
130 129 oveq1i
 |-  ( ( 2 x. 2 ) x. C ) = ( 4 x. C )
131 2cnd
 |-  ( ph -> 2 e. CC )
132 131 131 78 mulassd
 |-  ( ph -> ( ( 2 x. 2 ) x. C ) = ( 2 x. ( 2 x. C ) ) )
133 78 2timesd
 |-  ( ph -> ( 2 x. C ) = ( C + C ) )
134 133 oveq2d
 |-  ( ph -> ( 2 x. ( 2 x. C ) ) = ( 2 x. ( C + C ) ) )
135 127 2timesd
 |-  ( ph -> ( 2 x. ( C + C ) ) = ( ( C + C ) + ( C + C ) ) )
136 132 134 135 3eqtrd
 |-  ( ph -> ( ( 2 x. 2 ) x. C ) = ( ( C + C ) + ( C + C ) ) )
137 130 136 eqtr3id
 |-  ( ph -> ( 4 x. C ) = ( ( C + C ) + ( C + C ) ) )
138 137 oveq2d
 |-  ( ph -> ( ( vol* ` E ) + ( 4 x. C ) ) = ( ( vol* ` E ) + ( ( C + C ) + ( C + C ) ) ) )
139 128 138 eqtr4d
 |-  ( ph -> ( ( ( vol* ` E ) + ( C + C ) ) + ( C + C ) ) = ( ( vol* ` E ) + ( 4 x. C ) ) )
140 126 139 breqtrd
 |-  ( ph -> ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )
141 29 51 55 57 140 letrd
 |-  ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )