Metamath Proof Explorer


Theorem voliunlem1

Description: Lemma for voliun . (Contributed by Mario Carneiro, 20-Mar-2014)

Ref Expression
Hypotheses voliunlem.3 φ F : dom vol
voliunlem.5 φ Disj i F i
voliunlem1.6 H = n vol * E F n
voliunlem1.7 φ E
voliunlem1.8 φ vol * E
Assertion voliunlem1 φ k seq 1 + H k + vol * E ran F vol * E

Proof

Step Hyp Ref Expression
1 voliunlem.3 φ F : dom vol
2 voliunlem.5 φ Disj i F i
3 voliunlem1.6 H = n vol * E F n
4 voliunlem1.7 φ E
5 voliunlem1.8 φ vol * E
6 difss E ran F E
7 5 adantr φ k vol * E
8 ovolsscl E ran F E E vol * E vol * E ran F
9 6 4 7 8 mp3an2ani φ k vol * E ran F
10 difss E n = 1 k F n E
11 ovolsscl E n = 1 k F n E E vol * E vol * E n = 1 k F n
12 10 4 7 11 mp3an2ani φ k vol * E n = 1 k F n
13 inss1 E n = 1 k F n E
14 ovolsscl E n = 1 k F n E E vol * E vol * E n = 1 k F n
15 13 4 7 14 mp3an2ani φ k vol * E n = 1 k F n
16 elfznn n 1 k n
17 1 ffnd φ F Fn
18 fnfvelrn F Fn n F n ran F
19 17 18 sylan φ n F n ran F
20 elssuni F n ran F F n ran F
21 19 20 syl φ n F n ran F
22 16 21 sylan2 φ n 1 k F n ran F
23 22 ralrimiva φ n 1 k F n ran F
24 23 adantr φ k n 1 k F n ran F
25 iunss n = 1 k F n ran F n 1 k F n ran F
26 24 25 sylibr φ k n = 1 k F n ran F
27 26 sscond φ k E ran F E n = 1 k F n
28 4 adantr φ k E
29 10 28 sstrid φ k E n = 1 k F n
30 ovolss E ran F E n = 1 k F n E n = 1 k F n vol * E ran F vol * E n = 1 k F n
31 27 29 30 syl2anc φ k vol * E ran F vol * E n = 1 k F n
32 9 12 15 31 leadd2dd φ k vol * E n = 1 k F n + vol * E ran F vol * E n = 1 k F n + vol * E n = 1 k F n
33 oveq2 z = 1 1 z = 1 1
34 33 iuneq1d z = 1 n = 1 z F n = n = 1 1 F n
35 34 eleq1d z = 1 n = 1 z F n dom vol n = 1 1 F n dom vol
36 34 ineq2d z = 1 E n = 1 z F n = E n = 1 1 F n
37 36 fveq2d z = 1 vol * E n = 1 z F n = vol * E n = 1 1 F n
38 fveq2 z = 1 seq 1 + H z = seq 1 + H 1
39 37 38 eqeq12d z = 1 vol * E n = 1 z F n = seq 1 + H z vol * E n = 1 1 F n = seq 1 + H 1
40 35 39 anbi12d z = 1 n = 1 z F n dom vol vol * E n = 1 z F n = seq 1 + H z n = 1 1 F n dom vol vol * E n = 1 1 F n = seq 1 + H 1
41 40 imbi2d z = 1 φ n = 1 z F n dom vol vol * E n = 1 z F n = seq 1 + H z φ n = 1 1 F n dom vol vol * E n = 1 1 F n = seq 1 + H 1
42 oveq2 z = k 1 z = 1 k
43 42 iuneq1d z = k n = 1 z F n = n = 1 k F n
44 43 eleq1d z = k n = 1 z F n dom vol n = 1 k F n dom vol
45 43 ineq2d z = k E n = 1 z F n = E n = 1 k F n
46 45 fveq2d z = k vol * E n = 1 z F n = vol * E n = 1 k F n
47 fveq2 z = k seq 1 + H z = seq 1 + H k
48 46 47 eqeq12d z = k vol * E n = 1 z F n = seq 1 + H z vol * E n = 1 k F n = seq 1 + H k
49 44 48 anbi12d z = k n = 1 z F n dom vol vol * E n = 1 z F n = seq 1 + H z n = 1 k F n dom vol vol * E n = 1 k F n = seq 1 + H k
50 49 imbi2d z = k φ n = 1 z F n dom vol vol * E n = 1 z F n = seq 1 + H z φ n = 1 k F n dom vol vol * E n = 1 k F n = seq 1 + H k
51 oveq2 z = k + 1 1 z = 1 k + 1
52 51 iuneq1d z = k + 1 n = 1 z F n = n = 1 k + 1 F n
53 52 eleq1d z = k + 1 n = 1 z F n dom vol n = 1 k + 1 F n dom vol
54 52 ineq2d z = k + 1 E n = 1 z F n = E n = 1 k + 1 F n
55 54 fveq2d z = k + 1 vol * E n = 1 z F n = vol * E n = 1 k + 1 F n
56 fveq2 z = k + 1 seq 1 + H z = seq 1 + H k + 1
57 55 56 eqeq12d z = k + 1 vol * E n = 1 z F n = seq 1 + H z vol * E n = 1 k + 1 F n = seq 1 + H k + 1
58 53 57 anbi12d z = k + 1 n = 1 z F n dom vol vol * E n = 1 z F n = seq 1 + H z n = 1 k + 1 F n dom vol vol * E n = 1 k + 1 F n = seq 1 + H k + 1
59 58 imbi2d z = k + 1 φ n = 1 z F n dom vol vol * E n = 1 z F n = seq 1 + H z φ n = 1 k + 1 F n dom vol vol * E n = 1 k + 1 F n = seq 1 + H k + 1
60 1z 1
61 fzsn 1 1 1 = 1
62 iuneq1 1 1 = 1 n = 1 1 F n = n 1 F n
63 60 61 62 mp2b n = 1 1 F n = n 1 F n
64 1ex 1 V
65 fveq2 n = 1 F n = F 1
66 64 65 iunxsn n 1 F n = F 1
67 63 66 eqtri n = 1 1 F n = F 1
68 1nn 1
69 ffvelrn F : dom vol 1 F 1 dom vol
70 1 68 69 sylancl φ F 1 dom vol
71 67 70 eqeltrid φ n = 1 1 F n dom vol
72 65 ineq2d n = 1 E F n = E F 1
73 72 fveq2d n = 1 vol * E F n = vol * E F 1
74 fvex vol * E F 1 V
75 73 3 74 fvmpt 1 H 1 = vol * E F 1
76 68 75 ax-mp H 1 = vol * E F 1
77 seq1 1 seq 1 + H 1 = H 1
78 60 77 ax-mp seq 1 + H 1 = H 1
79 67 ineq2i E n = 1 1 F n = E F 1
80 79 fveq2i vol * E n = 1 1 F n = vol * E F 1
81 76 78 80 3eqtr4ri vol * E n = 1 1 F n = seq 1 + H 1
82 71 81 jctir φ n = 1 1 F n dom vol vol * E n = 1 1 F n = seq 1 + H 1
83 peano2nn k k + 1
84 ffvelrn F : dom vol k + 1 F k + 1 dom vol
85 1 83 84 syl2an φ k F k + 1 dom vol
86 unmbl n = 1 k F n dom vol F k + 1 dom vol n = 1 k F n F k + 1 dom vol
87 86 ex n = 1 k F n dom vol F k + 1 dom vol n = 1 k F n F k + 1 dom vol
88 85 87 syl5com φ k n = 1 k F n dom vol n = 1 k F n F k + 1 dom vol
89 simpr φ k k
90 nnuz = 1
91 89 90 eleqtrdi φ k k 1
92 fzsuc k 1 1 k + 1 = 1 k k + 1
93 iuneq1 1 k + 1 = 1 k k + 1 n = 1 k + 1 F n = n 1 k k + 1 F n
94 91 92 93 3syl φ k n = 1 k + 1 F n = n 1 k k + 1 F n
95 iunxun n 1 k k + 1 F n = n = 1 k F n n k + 1 F n
96 ovex k + 1 V
97 fveq2 n = k + 1 F n = F k + 1
98 96 97 iunxsn n k + 1 F n = F k + 1
99 98 uneq2i n = 1 k F n n k + 1 F n = n = 1 k F n F k + 1
100 95 99 eqtri n 1 k k + 1 F n = n = 1 k F n F k + 1
101 94 100 eqtrdi φ k n = 1 k + 1 F n = n = 1 k F n F k + 1
102 101 eleq1d φ k n = 1 k + 1 F n dom vol n = 1 k F n F k + 1 dom vol
103 88 102 sylibrd φ k n = 1 k F n dom vol n = 1 k + 1 F n dom vol
104 oveq1 vol * E n = 1 k F n = seq 1 + H k vol * E n = 1 k F n + vol * E F k + 1 = seq 1 + H k + vol * E F k + 1
105 inss1 E n = 1 k + 1 F n E
106 105 28 sstrid φ k E n = 1 k + 1 F n
107 ovolsscl E n = 1 k + 1 F n E E vol * E vol * E n = 1 k + 1 F n
108 105 4 7 107 mp3an2ani φ k vol * E n = 1 k + 1 F n
109 mblsplit F k + 1 dom vol E n = 1 k + 1 F n vol * E n = 1 k + 1 F n vol * E n = 1 k + 1 F n = vol * E n = 1 k + 1 F n F k + 1 + vol * E n = 1 k + 1 F n F k + 1
110 85 106 108 109 syl3anc φ k vol * E n = 1 k + 1 F n = vol * E n = 1 k + 1 F n F k + 1 + vol * E n = 1 k + 1 F n F k + 1
111 in32 E n = 1 k + 1 F n F k + 1 = E F k + 1 n = 1 k + 1 F n
112 inss2 E F k + 1 F k + 1
113 83 adantl φ k k + 1
114 113 90 eleqtrdi φ k k + 1 1
115 eluzfz2 k + 1 1 k + 1 1 k + 1
116 97 ssiun2s k + 1 1 k + 1 F k + 1 n = 1 k + 1 F n
117 114 115 116 3syl φ k F k + 1 n = 1 k + 1 F n
118 112 117 sstrid φ k E F k + 1 n = 1 k + 1 F n
119 df-ss E F k + 1 n = 1 k + 1 F n E F k + 1 n = 1 k + 1 F n = E F k + 1
120 118 119 sylib φ k E F k + 1 n = 1 k + 1 F n = E F k + 1
121 111 120 syl5eq φ k E n = 1 k + 1 F n F k + 1 = E F k + 1
122 121 fveq2d φ k vol * E n = 1 k + 1 F n F k + 1 = vol * E F k + 1
123 indif2 E n = 1 k + 1 F n F k + 1 = E n = 1 k + 1 F n F k + 1
124 uncom n = 1 k F n F k + 1 = F k + 1 n = 1 k F n
125 101 124 eqtr2di φ k F k + 1 n = 1 k F n = n = 1 k + 1 F n
126 2 ad2antrr φ k n 1 k Disj i F i
127 113 adantr φ k n 1 k k + 1
128 16 adantl φ k n 1 k n
129 128 nnred φ k n 1 k n
130 elfzle2 n 1 k n k
131 130 adantl φ k n 1 k n k
132 89 adantr φ k n 1 k k
133 nnleltp1 n k n k n < k + 1
134 128 132 133 syl2anc φ k n 1 k n k n < k + 1
135 131 134 mpbid φ k n 1 k n < k + 1
136 129 135 gtned φ k n 1 k k + 1 n
137 fveq2 i = k + 1 F i = F k + 1
138 fveq2 i = n F i = F n
139 137 138 disji2 Disj i F i k + 1 n k + 1 n F k + 1 F n =
140 126 127 128 136 139 syl121anc φ k n 1 k F k + 1 F n =
141 140 iuneq2dv φ k n = 1 k F k + 1 F n = n = 1 k
142 iunin2 n = 1 k F k + 1 F n = F k + 1 n = 1 k F n
143 iun0 n = 1 k =
144 141 142 143 3eqtr3g φ k F k + 1 n = 1 k F n =
145 uneqdifeq F k + 1 n = 1 k + 1 F n F k + 1 n = 1 k F n = F k + 1 n = 1 k F n = n = 1 k + 1 F n n = 1 k + 1 F n F k + 1 = n = 1 k F n
146 117 144 145 syl2anc φ k F k + 1 n = 1 k F n = n = 1 k + 1 F n n = 1 k + 1 F n F k + 1 = n = 1 k F n
147 125 146 mpbid φ k n = 1 k + 1 F n F k + 1 = n = 1 k F n
148 147 ineq2d φ k E n = 1 k + 1 F n F k + 1 = E n = 1 k F n
149 123 148 eqtr3id φ k E n = 1 k + 1 F n F k + 1 = E n = 1 k F n
150 149 fveq2d φ k vol * E n = 1 k + 1 F n F k + 1 = vol * E n = 1 k F n
151 122 150 oveq12d φ k vol * E n = 1 k + 1 F n F k + 1 + vol * E n = 1 k + 1 F n F k + 1 = vol * E F k + 1 + vol * E n = 1 k F n
152 inss1 E F k + 1 E
153 ovolsscl E F k + 1 E E vol * E vol * E F k + 1
154 152 4 7 153 mp3an2ani φ k vol * E F k + 1
155 154 recnd φ k vol * E F k + 1
156 15 recnd φ k vol * E n = 1 k F n
157 155 156 addcomd φ k vol * E F k + 1 + vol * E n = 1 k F n = vol * E n = 1 k F n + vol * E F k + 1
158 110 151 157 3eqtrd φ k vol * E n = 1 k + 1 F n = vol * E n = 1 k F n + vol * E F k + 1
159 seqp1 k 1 seq 1 + H k + 1 = seq 1 + H k + H k + 1
160 91 159 syl φ k seq 1 + H k + 1 = seq 1 + H k + H k + 1
161 97 ineq2d n = k + 1 E F n = E F k + 1
162 161 fveq2d n = k + 1 vol * E F n = vol * E F k + 1
163 fvex vol * E F k + 1 V
164 162 3 163 fvmpt k + 1 H k + 1 = vol * E F k + 1
165 113 164 syl φ k H k + 1 = vol * E F k + 1
166 165 oveq2d φ k seq 1 + H k + H k + 1 = seq 1 + H k + vol * E F k + 1
167 160 166 eqtrd φ k seq 1 + H k + 1 = seq 1 + H k + vol * E F k + 1
168 158 167 eqeq12d φ k vol * E n = 1 k + 1 F n = seq 1 + H k + 1 vol * E n = 1 k F n + vol * E F k + 1 = seq 1 + H k + vol * E F k + 1
169 104 168 syl5ibr φ k vol * E n = 1 k F n = seq 1 + H k vol * E n = 1 k + 1 F n = seq 1 + H k + 1
170 103 169 anim12d φ k n = 1 k F n dom vol vol * E n = 1 k F n = seq 1 + H k n = 1 k + 1 F n dom vol vol * E n = 1 k + 1 F n = seq 1 + H k + 1
171 170 expcom k φ n = 1 k F n dom vol vol * E n = 1 k F n = seq 1 + H k n = 1 k + 1 F n dom vol vol * E n = 1 k + 1 F n = seq 1 + H k + 1
172 171 a2d k φ n = 1 k F n dom vol vol * E n = 1 k F n = seq 1 + H k φ n = 1 k + 1 F n dom vol vol * E n = 1 k + 1 F n = seq 1 + H k + 1
173 41 50 59 50 82 172 nnind k φ n = 1 k F n dom vol vol * E n = 1 k F n = seq 1 + H k
174 173 impcom φ k n = 1 k F n dom vol vol * E n = 1 k F n = seq 1 + H k
175 174 simprd φ k vol * E n = 1 k F n = seq 1 + H k
176 175 eqcomd φ k seq 1 + H k = vol * E n = 1 k F n
177 176 oveq1d φ k seq 1 + H k + vol * E ran F = vol * E n = 1 k F n + vol * E ran F
178 174 simpld φ k n = 1 k F n dom vol
179 mblsplit n = 1 k F n dom vol E vol * E vol * E = vol * E n = 1 k F n + vol * E n = 1 k F n
180 178 28 7 179 syl3anc φ k vol * E = vol * E n = 1 k F n + vol * E n = 1 k F n
181 32 177 180 3brtr4d φ k seq 1 + H k + vol * E ran F vol * E