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 ) )