Metamath Proof Explorer


Theorem vitalilem4

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

Ref Expression
Hypotheses vitali.1 ˙=xy|x01y01xy
vitali.2 S=01/˙
vitali.3 φFFnS
vitali.4 φzSzFzz
vitali.5 φG:1-1 onto11
vitali.6 T=ns|sGnranF
vitali.7 φ¬ranF𝒫domvol
Assertion vitalilem4 φmvol*Tm=0

Proof

Step Hyp Ref Expression
1 vitali.1 ˙=xy|x01y01xy
2 vitali.2 S=01/˙
3 vitali.3 φFFnS
4 vitali.4 φzSzFzz
5 vitali.5 φG:1-1 onto11
6 vitali.6 T=ns|sGnranF
7 vitali.7 φ¬ranF𝒫domvol
8 fveq2 n=mGn=Gm
9 8 oveq2d n=msGn=sGm
10 9 eleq1d n=msGnranFsGmranF
11 10 rabbidv n=ms|sGnranF=s|sGmranF
12 reex V
13 12 rabex s|sGmranFV
14 11 6 13 fvmpt mTm=s|sGmranF
15 14 adantl φmTm=s|sGmranF
16 15 fveq2d φmvol*Tm=vol*s|sGmranF
17 1 2 3 4 5 6 7 vitalilem2 φranF0101mTmmTm12
18 17 simp1d φranF01
19 unitssre 01
20 18 19 sstrdi φranF
21 20 adantr φmranF
22 neg1rr 1
23 1re 1
24 iccssre 1111
25 22 23 24 mp2an 11
26 f1of G:1-1 onto11G:11
27 5 26 syl φG:11
28 27 ffvelrnda φmGm11
29 28 elin2d φmGm11
30 25 29 sselid φmGm
31 eqidd φms|sGmranF=s|sGmranF
32 21 30 31 ovolshft φmvol*ranF=vol*s|sGmranF
33 16 32 eqtr4d φmvol*Tm=vol*ranF
34 3re 3
35 34 rexri 3*
36 35 a1i φ0<vol*ranF3*
37 3rp 3+
38 0re 0
39 0le1 01
40 ovolicc 0101vol*01=10
41 38 23 39 40 mp3an vol*01=10
42 1m0e1 10=1
43 41 42 eqtri vol*01=1
44 43 23 eqeltri vol*01
45 ovolsscl ranF0101vol*01vol*ranF
46 19 44 45 mp3an23 ranF01vol*ranF
47 18 46 syl φvol*ranF
48 47 adantr φ0<vol*ranFvol*ranF
49 simpr φ0<vol*ranF0<vol*ranF
50 48 49 elrpd φ0<vol*ranFvol*ranF+
51 rpdivcl 3+vol*ranF+3vol*ranF+
52 37 50 51 sylancr φ0<vol*ranF3vol*ranF+
53 52 rpred φ0<vol*ranF3vol*ranF
54 52 rpge0d φ0<vol*ranF03vol*ranF
55 flge0nn0 3vol*ranF03vol*ranF3vol*ranF0
56 53 54 55 syl2anc φ0<vol*ranF3vol*ranF0
57 nn0p1nn 3vol*ranF03vol*ranF+1
58 56 57 syl φ0<vol*ranF3vol*ranF+1
59 58 nnred φ0<vol*ranF3vol*ranF+1
60 59 48 remulcld φ0<vol*ranF3vol*ranF+1vol*ranF
61 60 rexrd φ0<vol*ranF3vol*ranF+1vol*ranF*
62 12 elpw2 ranF𝒫ranF
63 20 62 sylibr φranF𝒫
64 63 anim1i φ¬ranFdomvolranF𝒫¬ranFdomvol
65 eldif ranF𝒫domvolranF𝒫¬ranFdomvol
66 64 65 sylibr φ¬ranFdomvolranF𝒫domvol
67 66 ex φ¬ranFdomvolranF𝒫domvol
68 7 67 mt3d φranFdomvol
69 inss1 11
70 qssre
71 69 70 sstri 11
72 fss G:1111G:
73 27 71 72 sylancl φG:
74 73 ffvelrnda φnGn
75 shftmbl ranFdomvolGns|sGnranFdomvol
76 68 74 75 syl2an2r φns|sGnranFdomvol
77 76 6 fmptd φT:domvol
78 77 ffvelrnda φmTmdomvol
79 78 ralrimiva φmTmdomvol
80 iunmbl mTmdomvolmTmdomvol
81 79 80 syl φmTmdomvol
82 mblss mTmdomvolmTm
83 ovolcl mTmvol*mTm*
84 81 82 83 3syl φvol*mTm*
85 84 adantr φ0<vol*ranFvol*mTm*
86 flltp1 3vol*ranF3vol*ranF<3vol*ranF+1
87 53 86 syl φ0<vol*ranF3vol*ranF<3vol*ranF+1
88 34 a1i φ0<vol*ranF3
89 88 59 50 ltdivmul2d φ0<vol*ranF3vol*ranF<3vol*ranF+13<3vol*ranF+1vol*ranF
90 87 89 mpbid φ0<vol*ranF3<3vol*ranF+1vol*ranF
91 nnuz =1
92 1zzd φ0<vol*ranF1
93 mblvol TmdomvolvolTm=vol*Tm
94 78 93 syl φmvolTm=vol*Tm
95 94 33 eqtrd φmvolTm=vol*ranF
96 47 adantr φmvol*ranF
97 95 96 eqeltrd φmvolTm
98 97 adantlr φ0<vol*ranFmvolTm
99 eqid mvolTm=mvolTm
100 98 99 fmptd φ0<vol*ranFmvolTm:
101 100 ffvelrnda φ0<vol*ranFkmvolTmk
102 91 92 101 serfre φ0<vol*ranFseq1+mvolTm:
103 102 frnd φ0<vol*ranFranseq1+mvolTm
104 ressxr *
105 103 104 sstrdi φ0<vol*ranFranseq1+mvolTm*
106 95 adantlr φ0<vol*ranFmvolTm=vol*ranF
107 106 mpteq2dva φ0<vol*ranFmvolTm=mvol*ranF
108 fconstmpt ×vol*ranF=mvol*ranF
109 107 108 eqtr4di φ0<vol*ranFmvolTm=×vol*ranF
110 109 seqeq3d φ0<vol*ranFseq1+mvolTm=seq1+×vol*ranF
111 110 fveq1d φ0<vol*ranFseq1+mvolTm3vol*ranF+1=seq1+×vol*ranF3vol*ranF+1
112 48 recnd φ0<vol*ranFvol*ranF
113 ser1const vol*ranF3vol*ranF+1seq1+×vol*ranF3vol*ranF+1=3vol*ranF+1vol*ranF
114 112 58 113 syl2anc φ0<vol*ranFseq1+×vol*ranF3vol*ranF+1=3vol*ranF+1vol*ranF
115 111 114 eqtrd φ0<vol*ranFseq1+mvolTm3vol*ranF+1=3vol*ranF+1vol*ranF
116 102 ffnd φ0<vol*ranFseq1+mvolTmFn
117 fnfvelrn seq1+mvolTmFn3vol*ranF+1seq1+mvolTm3vol*ranF+1ranseq1+mvolTm
118 116 58 117 syl2anc φ0<vol*ranFseq1+mvolTm3vol*ranF+1ranseq1+mvolTm
119 115 118 eqeltrrd φ0<vol*ranF3vol*ranF+1vol*ranFranseq1+mvolTm
120 supxrub ranseq1+mvolTm*3vol*ranF+1vol*ranFranseq1+mvolTm3vol*ranF+1vol*ranFsupranseq1+mvolTm*<
121 105 119 120 syl2anc φ0<vol*ranF3vol*ranF+1vol*ranFsupranseq1+mvolTm*<
122 81 adantr φ0<vol*ranFmTmdomvol
123 mblvol mTmdomvolvolmTm=vol*mTm
124 122 123 syl φ0<vol*ranFvolmTm=vol*mTm
125 78 97 jca φmTmdomvolvolTm
126 125 ralrimiva φmTmdomvolvolTm
127 1 2 3 4 5 6 7 vitalilem3 φDisjmTm
128 127 adantr φ0<vol*ranFDisjmTm
129 eqid seq1+mvolTm=seq1+mvolTm
130 129 99 voliun mTmdomvolvolTmDisjmTmvolmTm=supranseq1+mvolTm*<
131 126 128 130 syl2an2r φ0<vol*ranFvolmTm=supranseq1+mvolTm*<
132 124 131 eqtr3d φ0<vol*ranFvol*mTm=supranseq1+mvolTm*<
133 121 132 breqtrrd φ0<vol*ranF3vol*ranF+1vol*ranFvol*mTm
134 36 61 85 90 133 xrltletrd φ0<vol*ranF3<vol*mTm
135 17 simp3d φmTm12
136 135 adantr φ0<vol*ranFmTm12
137 2re 2
138 iccssre 1212
139 22 137 138 mp2an 12
140 ovolss mTm1212vol*mTmvol*12
141 136 139 140 sylancl φ0<vol*ranFvol*mTmvol*12
142 2cn 2
143 ax-1cn 1
144 142 143 subnegi 2-1=2+1
145 neg1lt0 1<0
146 2pos 0<2
147 22 38 137 lttri 1<00<21<2
148 145 146 147 mp2an 1<2
149 22 137 148 ltleii 12
150 ovolicc 1212vol*12=2-1
151 22 137 149 150 mp3an vol*12=2-1
152 df-3 3=2+1
153 144 151 152 3eqtr4i vol*12=3
154 141 153 breqtrdi φ0<vol*ranFvol*mTm3
155 xrlenlt vol*mTm*3*vol*mTm3¬3<vol*mTm
156 85 35 155 sylancl φ0<vol*ranFvol*mTm3¬3<vol*mTm
157 154 156 mpbid φ0<vol*ranF¬3<vol*mTm
158 134 157 pm2.65da φ¬0<vol*ranF
159 ovolge0 ranF0vol*ranF
160 20 159 syl φ0vol*ranF
161 0xr 0*
162 ovolcl ranFvol*ranF*
163 20 162 syl φvol*ranF*
164 xrleloe 0*vol*ranF*0vol*ranF0<vol*ranF0=vol*ranF
165 161 163 164 sylancr φ0vol*ranF0<vol*ranF0=vol*ranF
166 160 165 mpbid φ0<vol*ranF0=vol*ranF
167 166 ord φ¬0<vol*ranF0=vol*ranF
168 158 167 mpd φ0=vol*ranF
169 168 adantr φm0=vol*ranF
170 33 169 eqtr4d φmvol*Tm=0