This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vitalilem5

Description: Lemma for vitali . (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Hypotheses vitali.1 
|- .~ = { <. x , y >. | ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) /\ ( x - y ) e. QQ ) }
vitali.2 
|- S = ( ( 0 [,] 1 ) /. .~ )
vitali.3 
|- ( ph -> F Fn S )
vitali.4 
|- ( ph -> A. z e. S ( z =/= (/) -> ( F ` z ) e. z ) )
vitali.5 
|- ( ph -> G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) )
vitali.6 
|- T = ( n e. NN |-> { s e. RR | ( s - ( G ` n ) ) e. ran F } )
vitali.7 
|- ( ph -> -. ran F e. ( ~P RR \ dom vol ) )
Assertion vitalilem5 
|- -. ph

Proof

Step Hyp Ref Expression
1 vitali.1 
 |-  .~ = { <. x , y >. | ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) /\ ( x - y ) e. QQ ) }
2 vitali.2 
 |-  S = ( ( 0 [,] 1 ) /. .~ )
3 vitali.3 
 |-  ( ph -> F Fn S )
4 vitali.4 
 |-  ( ph -> A. z e. S ( z =/= (/) -> ( F ` z ) e. z ) )
5 vitali.5 
 |-  ( ph -> G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) )
6 vitali.6 
 |-  T = ( n e. NN |-> { s e. RR | ( s - ( G ` n ) ) e. ran F } )
7 vitali.7 
 |-  ( ph -> -. ran F e. ( ~P RR \ dom vol ) )
8 0lt1 
 |-  0 < 1
9 0re 
 |-  0 e. RR
10 1re 
 |-  1 e. RR
11 0le1 
 |-  0 <_ 1
12 ovolicc 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ 0 <_ 1 ) -> ( vol* ` ( 0 [,] 1 ) ) = ( 1 - 0 ) )
13 9 10 11 12 mp3an 
 |-  ( vol* ` ( 0 [,] 1 ) ) = ( 1 - 0 )
14 1m0e1 
 |-  ( 1 - 0 ) = 1
15 13 14 eqtri 
 |-  ( vol* ` ( 0 [,] 1 ) ) = 1
16 8 15 breqtrri 
 |-  0 < ( vol* ` ( 0 [,] 1 ) )
17 15 10 eqeltri 
 |-  ( vol* ` ( 0 [,] 1 ) ) e. RR
18 9 17 ltnlei 
 |-  ( 0 < ( vol* ` ( 0 [,] 1 ) ) <-> -. ( vol* ` ( 0 [,] 1 ) ) <_ 0 )
19 16 18 mpbi 
 |-  -. ( vol* ` ( 0 [,] 1 ) ) <_ 0
20 1 2 3 4 5 6 7 vitalilem2 
 |-  ( ph -> ( ran F C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ U_ m e. NN ( T ` m ) /\ U_ m e. NN ( T ` m ) C_ ( -u 1 [,] 2 ) ) )
21 20 simp2d 
 |-  ( ph -> ( 0 [,] 1 ) C_ U_ m e. NN ( T ` m ) )
22 1 vitalilem1 
 |-  .~ Er ( 0 [,] 1 )
23 erdm 
 |-  ( .~ Er ( 0 [,] 1 ) -> dom .~ = ( 0 [,] 1 ) )
24 22 23 ax-mp 
 |-  dom .~ = ( 0 [,] 1 )
25 simpr 
 |-  ( ( ph /\ z e. S ) -> z e. S )
26 25 2 eleqtrdi 
 |-  ( ( ph /\ z e. S ) -> z e. ( ( 0 [,] 1 ) /. .~ ) )
27 elqsn0 
 |-  ( ( dom .~ = ( 0 [,] 1 ) /\ z e. ( ( 0 [,] 1 ) /. .~ ) ) -> z =/= (/) )
28 24 26 27 sylancr 
 |-  ( ( ph /\ z e. S ) -> z =/= (/) )
29 22 a1i 
 |-  ( ph -> .~ Er ( 0 [,] 1 ) )
30 29 qsss 
 |-  ( ph -> ( ( 0 [,] 1 ) /. .~ ) C_ ~P ( 0 [,] 1 ) )
31 2 30 eqsstrid 
 |-  ( ph -> S C_ ~P ( 0 [,] 1 ) )
32 31 sselda 
 |-  ( ( ph /\ z e. S ) -> z e. ~P ( 0 [,] 1 ) )
33 32 elpwid 
 |-  ( ( ph /\ z e. S ) -> z C_ ( 0 [,] 1 ) )
34 33 sseld 
 |-  ( ( ph /\ z e. S ) -> ( ( F ` z ) e. z -> ( F ` z ) e. ( 0 [,] 1 ) ) )
35 28 34 embantd 
 |-  ( ( ph /\ z e. S ) -> ( ( z =/= (/) -> ( F ` z ) e. z ) -> ( F ` z ) e. ( 0 [,] 1 ) ) )
36 35 ralimdva 
 |-  ( ph -> ( A. z e. S ( z =/= (/) -> ( F ` z ) e. z ) -> A. z e. S ( F ` z ) e. ( 0 [,] 1 ) ) )
37 4 36 mpd 
 |-  ( ph -> A. z e. S ( F ` z ) e. ( 0 [,] 1 ) )
38 ffnfv 
 |-  ( F : S --> ( 0 [,] 1 ) <-> ( F Fn S /\ A. z e. S ( F ` z ) e. ( 0 [,] 1 ) ) )
39 3 37 38 sylanbrc 
 |-  ( ph -> F : S --> ( 0 [,] 1 ) )
40 39 frnd 
 |-  ( ph -> ran F C_ ( 0 [,] 1 ) )
41 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
42 40 41 sstrdi 
 |-  ( ph -> ran F C_ RR )
43 reex 
 |-  RR e. _V
44 43 elpw2 
 |-  ( ran F e. ~P RR <-> ran F C_ RR )
45 42 44 sylibr 
 |-  ( ph -> ran F e. ~P RR )
46 45 anim1i 
 |-  ( ( ph /\ -. ran F e. dom vol ) -> ( ran F e. ~P RR /\ -. ran F e. dom vol ) )
47 eldif 
 |-  ( ran F e. ( ~P RR \ dom vol ) <-> ( ran F e. ~P RR /\ -. ran F e. dom vol ) )
48 46 47 sylibr 
 |-  ( ( ph /\ -. ran F e. dom vol ) -> ran F e. ( ~P RR \ dom vol ) )
49 48 ex 
 |-  ( ph -> ( -. ran F e. dom vol -> ran F e. ( ~P RR \ dom vol ) ) )
50 7 49 mt3d 
 |-  ( ph -> ran F e. dom vol )
51 f1of 
 |-  ( G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) -> G : NN --> ( QQ i^i ( -u 1 [,] 1 ) ) )
52 5 51 syl 
 |-  ( ph -> G : NN --> ( QQ i^i ( -u 1 [,] 1 ) ) )
53 inss1 
 |-  ( QQ i^i ( -u 1 [,] 1 ) ) C_ QQ
54 qssre 
 |-  QQ C_ RR
55 53 54 sstri 
 |-  ( QQ i^i ( -u 1 [,] 1 ) ) C_ RR
56 fss 
 |-  ( ( G : NN --> ( QQ i^i ( -u 1 [,] 1 ) ) /\ ( QQ i^i ( -u 1 [,] 1 ) ) C_ RR ) -> G : NN --> RR )
57 52 55 56 sylancl 
 |-  ( ph -> G : NN --> RR )
58 57 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. RR )
59 shftmbl 
 |-  ( ( ran F e. dom vol /\ ( G ` n ) e. RR ) -> { s e. RR | ( s - ( G ` n ) ) e. ran F } e. dom vol )
60 50 58 59 syl2an2r 
 |-  ( ( ph /\ n e. NN ) -> { s e. RR | ( s - ( G ` n ) ) e. ran F } e. dom vol )
61 60 6 fmptd 
 |-  ( ph -> T : NN --> dom vol )
62 61 ffvelcdmda 
 |-  ( ( ph /\ m e. NN ) -> ( T ` m ) e. dom vol )
63 62 ralrimiva 
 |-  ( ph -> A. m e. NN ( T ` m ) e. dom vol )
64 iunmbl 
 |-  ( A. m e. NN ( T ` m ) e. dom vol -> U_ m e. NN ( T ` m ) e. dom vol )
65 63 64 syl 
 |-  ( ph -> U_ m e. NN ( T ` m ) e. dom vol )
66 mblss 
 |-  ( U_ m e. NN ( T ` m ) e. dom vol -> U_ m e. NN ( T ` m ) C_ RR )
67 65 66 syl 
 |-  ( ph -> U_ m e. NN ( T ` m ) C_ RR )
68 ovolss 
 |-  ( ( ( 0 [,] 1 ) C_ U_ m e. NN ( T ` m ) /\ U_ m e. NN ( T ` m ) C_ RR ) -> ( vol* ` ( 0 [,] 1 ) ) <_ ( vol* ` U_ m e. NN ( T ` m ) ) )
69 21 67 68 syl2anc 
 |-  ( ph -> ( vol* ` ( 0 [,] 1 ) ) <_ ( vol* ` U_ m e. NN ( T ` m ) ) )
70 eqid 
 |-  seq 1 ( + , ( m e. NN |-> ( vol* ` ( T ` m ) ) ) ) = seq 1 ( + , ( m e. NN |-> ( vol* ` ( T ` m ) ) ) )
71 eqid 
 |-  ( m e. NN |-> ( vol* ` ( T ` m ) ) ) = ( m e. NN |-> ( vol* ` ( T ` m ) ) )
72 mblss 
 |-  ( ( T ` m ) e. dom vol -> ( T ` m ) C_ RR )
73 62 72 syl 
 |-  ( ( ph /\ m e. NN ) -> ( T ` m ) C_ RR )
74 1 2 3 4 5 6 7 vitalilem4 
 |-  ( ( ph /\ m e. NN ) -> ( vol* ` ( T ` m ) ) = 0 )
75 74 9 eqeltrdi 
 |-  ( ( ph /\ m e. NN ) -> ( vol* ` ( T ` m ) ) e. RR )
76 74 mpteq2dva 
 |-  ( ph -> ( m e. NN |-> ( vol* ` ( T ` m ) ) ) = ( m e. NN |-> 0 ) )
77 fconstmpt 
 |-  ( NN X. { 0 } ) = ( m e. NN |-> 0 )
78 nnuz 
 |-  NN = ( ZZ>= ` 1 )
79 78 xpeq1i 
 |-  ( NN X. { 0 } ) = ( ( ZZ>= ` 1 ) X. { 0 } )
80 77 79 eqtr3i 
 |-  ( m e. NN |-> 0 ) = ( ( ZZ>= ` 1 ) X. { 0 } )
81 76 80 eqtrdi 
 |-  ( ph -> ( m e. NN |-> ( vol* ` ( T ` m ) ) ) = ( ( ZZ>= ` 1 ) X. { 0 } ) )
82 81 seqeq3d 
 |-  ( ph -> seq 1 ( + , ( m e. NN |-> ( vol* ` ( T ` m ) ) ) ) = seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) )
83 1z 
 |-  1 e. ZZ
84 serclim0 
 |-  ( 1 e. ZZ -> seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> 0 )
85 83 84 ax-mp 
 |-  seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> 0
86 82 85 eqbrtrdi 
 |-  ( ph -> seq 1 ( + , ( m e. NN |-> ( vol* ` ( T ` m ) ) ) ) ~~> 0 )
87 seqex 
 |-  seq 1 ( + , ( m e. NN |-> ( vol* ` ( T ` m ) ) ) ) e. _V
88 c0ex 
 |-  0 e. _V
89 87 88 breldm 
 |-  ( seq 1 ( + , ( m e. NN |-> ( vol* ` ( T ` m ) ) ) ) ~~> 0 -> seq 1 ( + , ( m e. NN |-> ( vol* ` ( T ` m ) ) ) ) e. dom ~~> )
90 86 89 syl 
 |-  ( ph -> seq 1 ( + , ( m e. NN |-> ( vol* ` ( T ` m ) ) ) ) e. dom ~~> )
91 70 71 73 75 90 ovoliun2 
 |-  ( ph -> ( vol* ` U_ m e. NN ( T ` m ) ) <_ sum_ m e. NN ( vol* ` ( T ` m ) ) )
92 74 sumeq2dv 
 |-  ( ph -> sum_ m e. NN ( vol* ` ( T ` m ) ) = sum_ m e. NN 0 )
93 78 eqimssi 
 |-  NN C_ ( ZZ>= ` 1 )
94 93 orci 
 |-  ( NN C_ ( ZZ>= ` 1 ) \/ NN e. Fin )
95 sumz 
 |-  ( ( NN C_ ( ZZ>= ` 1 ) \/ NN e. Fin ) -> sum_ m e. NN 0 = 0 )
96 94 95 ax-mp 
 |-  sum_ m e. NN 0 = 0
97 92 96 eqtrdi 
 |-  ( ph -> sum_ m e. NN ( vol* ` ( T ` m ) ) = 0 )
98 91 97 breqtrd 
 |-  ( ph -> ( vol* ` U_ m e. NN ( T ` m ) ) <_ 0 )
99 ovolge0 
 |-  ( U_ m e. NN ( T ` m ) C_ RR -> 0 <_ ( vol* ` U_ m e. NN ( T ` m ) ) )
100 67 99 syl 
 |-  ( ph -> 0 <_ ( vol* ` U_ m e. NN ( T ` m ) ) )
101 ovolcl 
 |-  ( U_ m e. NN ( T ` m ) C_ RR -> ( vol* ` U_ m e. NN ( T ` m ) ) e. RR* )
102 67 101 syl 
 |-  ( ph -> ( vol* ` U_ m e. NN ( T ` m ) ) e. RR* )
103 0xr 
 |-  0 e. RR*
104 xrletri3 
 |-  ( ( ( vol* ` U_ m e. NN ( T ` m ) ) e. RR* /\ 0 e. RR* ) -> ( ( vol* ` U_ m e. NN ( T ` m ) ) = 0 <-> ( ( vol* ` U_ m e. NN ( T ` m ) ) <_ 0 /\ 0 <_ ( vol* ` U_ m e. NN ( T ` m ) ) ) ) )
105 102 103 104 sylancl 
 |-  ( ph -> ( ( vol* ` U_ m e. NN ( T ` m ) ) = 0 <-> ( ( vol* ` U_ m e. NN ( T ` m ) ) <_ 0 /\ 0 <_ ( vol* ` U_ m e. NN ( T ` m ) ) ) ) )
106 98 100 105 mpbir2and 
 |-  ( ph -> ( vol* ` U_ m e. NN ( T ` m ) ) = 0 )
107 69 106 breqtrd 
 |-  ( ph -> ( vol* ` ( 0 [,] 1 ) ) <_ 0 )
108 19 107 mto 
 |-  -. ph