Metamath Proof Explorer


Theorem uniioombllem3a

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 8-May-2015)

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 ) )
Assertion uniioombllem3a
|- ( ph -> ( K = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) /\ ( vol* ` K ) e. RR ) )

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 ioof
 |-  (,) : ( RR* X. RR* ) --> ~P RR
15 inss2
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
16 rexpssxrxp
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
17 15 16 sstri
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
18 fss
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> G : NN --> ( RR* X. RR* ) )
19 7 17 18 sylancl
 |-  ( ph -> G : NN --> ( RR* X. RR* ) )
20 fco
 |-  ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ G : NN --> ( RR* X. RR* ) ) -> ( (,) o. G ) : NN --> ~P RR )
21 14 19 20 sylancr
 |-  ( ph -> ( (,) o. G ) : NN --> ~P RR )
22 ffun
 |-  ( ( (,) o. G ) : NN --> ~P RR -> Fun ( (,) o. G ) )
23 funiunfv
 |-  ( Fun ( (,) o. G ) -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U. ( ( (,) o. G ) " ( 1 ... M ) ) )
24 21 22 23 3syl
 |-  ( ph -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U. ( ( (,) o. G ) " ( 1 ... M ) ) )
25 elfznn
 |-  ( j e. ( 1 ... M ) -> j e. NN )
26 fvco3
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( ( (,) o. G ) ` j ) = ( (,) ` ( G ` j ) ) )
27 7 25 26 syl2an
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) o. G ) ` j ) = ( (,) ` ( G ` j ) ) )
28 27 iuneq2dv
 |-  ( ph -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
29 24 28 eqtr3d
 |-  ( ph -> U. ( ( (,) o. G ) " ( 1 ... M ) ) = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
30 13 29 syl5eq
 |-  ( ph -> K = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
31 ffvelrn
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) )
32 7 25 31 syl2an
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) )
33 32 elin2d
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) e. ( RR X. RR ) )
34 1st2nd2
 |-  ( ( G ` j ) e. ( RR X. RR ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
35 33 34 syl
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
36 35 fveq2d
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) )
37 df-ov
 |-  ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
38 36 37 eqtr4di
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) = ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) )
39 ioossre
 |-  ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) C_ RR
40 38 39 eqsstrdi
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) C_ RR )
41 40 ralrimiva
 |-  ( ph -> A. j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) C_ RR )
42 iunss
 |-  ( U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) C_ RR <-> A. j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) C_ RR )
43 41 42 sylibr
 |-  ( ph -> U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) C_ RR )
44 30 43 eqsstrd
 |-  ( ph -> K C_ RR )
45 fzfid
 |-  ( ph -> ( 1 ... M ) e. Fin )
46 38 fveq2d
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) = ( vol* ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) )
47 ovolfcl
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) )
48 7 25 47 syl2an
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) )
49 ovolioo
 |-  ( ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) -> ( vol* ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) )
50 48 49 syl
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) )
51 46 50 eqtrd
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) )
52 48 simp2d
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( 2nd ` ( G ` j ) ) e. RR )
53 48 simp1d
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( 1st ` ( G ` j ) ) e. RR )
54 52 53 resubcld
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. RR )
55 51 54 eqeltrd
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR )
56 45 55 fsumrecl
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR )
57 30 fveq2d
 |-  ( ph -> ( vol* ` K ) = ( vol* ` U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) ) )
58 40 55 jca
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) C_ RR /\ ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR ) )
59 58 ralrimiva
 |-  ( ph -> A. j e. ( 1 ... M ) ( ( (,) ` ( G ` j ) ) C_ RR /\ ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR ) )
60 ovolfiniun
 |-  ( ( ( 1 ... M ) e. Fin /\ A. j e. ( 1 ... M ) ( ( (,) ` ( G ` j ) ) C_ RR /\ ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR ) ) -> ( vol* ` U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) ) <_ sum_ j e. ( 1 ... M ) ( vol* ` ( (,) ` ( G ` j ) ) ) )
61 45 59 60 syl2anc
 |-  ( ph -> ( vol* ` U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) ) <_ sum_ j e. ( 1 ... M ) ( vol* ` ( (,) ` ( G ` j ) ) ) )
62 57 61 eqbrtrd
 |-  ( ph -> ( vol* ` K ) <_ sum_ j e. ( 1 ... M ) ( vol* ` ( (,) ` ( G ` j ) ) ) )
63 ovollecl
 |-  ( ( K C_ RR /\ sum_ j e. ( 1 ... M ) ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR /\ ( vol* ` K ) <_ sum_ j e. ( 1 ... M ) ( vol* ` ( (,) ` ( G ` j ) ) ) ) -> ( vol* ` K ) e. RR )
64 44 56 62 63 syl3anc
 |-  ( ph -> ( vol* ` K ) e. RR )
65 30 64 jca
 |-  ( ph -> ( K = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) /\ ( vol* ` K ) e. RR ) )