Metamath Proof Explorer


Theorem sge0fodjrnlem

Description: Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned 0 in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0fodjrnlem.k kφ
sge0fodjrnlem.n nφ
sge0fodjrnlem.bd k=GB=D
sge0fodjrnlem.c φCV
sge0fodjrnlem.f φF:ContoA
sge0fodjrnlem.dj φDisjnCFn
sge0fodjrnlem.fng φnCFn=G
sge0fodjrnlem.b φkAB0+∞
sge0fodjrnlem.b0 φk=B=0
sge0fodjrnlem.z Z=F-1
Assertion sge0fodjrnlem φsum^kAB=sum^nCD

Proof

Step Hyp Ref Expression
1 sge0fodjrnlem.k kφ
2 sge0fodjrnlem.n nφ
3 sge0fodjrnlem.bd k=GB=D
4 sge0fodjrnlem.c φCV
5 sge0fodjrnlem.f φF:ContoA
6 sge0fodjrnlem.dj φDisjnCFn
7 sge0fodjrnlem.fng φnCFn=G
8 sge0fodjrnlem.b φkAB0+∞
9 sge0fodjrnlem.b0 φk=B=0
10 sge0fodjrnlem.z Z=F-1
11 fornex CVF:ContoAAV
12 4 5 11 sylc φAV
13 difssd φAA
14 simpl φkAφ
15 13 sselda φkAkA
16 14 15 8 syl2anc φkAB0+∞
17 simpl φkAAφ
18 dfin4 A=AA
19 18 eqcomi AA=A
20 inss2 A
21 19 20 eqsstri AA
22 id kAAkAA
23 21 22 sselid kAAk
24 elsni kk=
25 23 24 syl kAAk=
26 25 adantl φkAAk=
27 17 26 9 syl2anc φkAAB=0
28 1 12 13 16 27 sge0ss φsum^kAB=sum^kAB
29 28 eqcomd φsum^kAB=sum^kAB
30 4 difexd φCZV
31 eqid nCFn=nCFn
32 fof F:ContoAF:CA
33 5 32 syl φF:CA
34 33 ffvelrnda φnCFnA
35 fveq2 m=nFm=Fn
36 35 neeq1d m=nFmFn
37 36 cbvrabv mC|Fm=nC|Fn
38 35 cbvmptv mCFm=nCFn
39 38 rneqi ranmCFm=rannCFn
40 39 difeq1i ranmCFm=rannCFn
41 2 31 34 6 37 40 disjf1o φnCFnmC|Fm:mC|Fm1-1 ontoranmCFm
42 33 feqmptd φF=nCFn
43 difssd φCZC
44 43 sselda φnCZnC
45 eldifi nCZnC
46 45 adantr nCZFn=nC
47 id Fn=Fn=
48 fvex FnV
49 48 elsn FnFn=
50 47 49 sylibr Fn=Fn
51 50 adantl nCZFn=Fn
52 46 51 jca nCZFn=nCFn
53 52 adantll φnCZFn=nCFn
54 33 ffnd φFFnC
55 elpreima FFnCnF-1nCFn
56 54 55 syl φnF-1nCFn
57 56 ad2antrr φnCZFn=nF-1nCFn
58 53 57 mpbird φnCZFn=nF-1
59 58 10 eleqtrrdi φnCZFn=nZ
60 eldifn nCZ¬nZ
61 60 ad2antlr φnCZFn=¬nZ
62 59 61 pm2.65da φnCZ¬Fn=
63 62 neqned φnCZFn
64 44 63 jca φnCZnCFn
65 36 elrab nmC|FmnCFn
66 64 65 sylibr φnCZnmC|Fm
67 66 ex φnCZnmC|Fm
68 65 simplbi nmC|FmnC
69 68 adantl φnmC|FmnC
70 10 eleq2i nZnF-1
71 70 biimpi nZnF-1
72 71 adantl φnZnF-1
73 56 adantr φnZnF-1nCFn
74 72 73 mpbid φnZnCFn
75 74 simprd φnZFn
76 elsni FnFn=
77 75 76 syl φnZFn=
78 77 adantlr φnmC|FmnZFn=
79 65 simprbi nmC|FmFn
80 79 ad2antlr φnmC|FmnZFn
81 80 neneqd φnmC|FmnZ¬Fn=
82 78 81 pm2.65da φnmC|Fm¬nZ
83 69 82 eldifd φnmC|FmnCZ
84 83 ex φnmC|FmnCZ
85 2 84 ralrimi φnmC|FmnCZ
86 dfss3 mC|FmCZnmC|FmnCZ
87 85 86 sylibr φmC|FmCZ
88 87 sseld φnmC|FmnCZ
89 67 88 impbid φnCZnmC|Fm
90 2 89 alrimi φnnCZnmC|Fm
91 dfcleq CZ=mC|FmnnCZnmC|Fm
92 90 91 sylibr φCZ=mC|Fm
93 42 92 reseq12d φFCZ=nCFnmC|Fm
94 42 38 eqtr4di φF=mCFm
95 94 eqcomd φmCFm=F
96 95 rneqd φranmCFm=ranF
97 forn F:ContoAranF=A
98 5 97 syl φranF=A
99 96 98 eqtr2d φA=ranmCFm
100 99 difeq1d φA=ranmCFm
101 93 92 100 f1oeq123d φFCZ:CZ1-1 ontoAnCFnmC|Fm:mC|Fm1-1 ontoranmCFm
102 41 101 mpbird φFCZ:CZ1-1 ontoA
103 fvres nCZFCZn=Fn
104 103 adantl φnCZFCZn=Fn
105 simpl φnCZφ
106 105 44 7 syl2anc φnCZFn=G
107 104 106 eqtrd φnCZFCZn=G
108 1 2 3 30 102 107 16 sge0f1o φsum^kAB=sum^nCZD
109 7 eqcomd φnCG=Fn
110 109 34 eqeltrd φnCGA
111 105 44 110 syl2anc φnCZGA
112 111 ex φnCZGA
113 112 imdistani φnCZφGA
114 nfcv _kG
115 nfv kGA
116 1 115 nfan kφGA
117 nfv kD0+∞
118 116 117 nfim kφGAD0+∞
119 eleq1 k=GkAGA
120 119 anbi2d k=GφkAφGA
121 3 eleq1d k=GB0+∞D0+∞
122 120 121 imbi12d k=GφkAB0+∞φGAD0+∞
123 114 118 122 8 vtoclgf GAφGAD0+∞
124 111 113 123 sylc φnCZD0+∞
125 simpl φnCCZφ
126 eldifi nCCZnC
127 126 adantl φnCCZnC
128 125 127 110 syl2anc φnCCZGA
129 dfin4 ZC=ZZC
130 difss ZZCZ
131 129 130 eqsstri ZCZ
132 inss2 CZZ
133 id nCCZnCCZ
134 dfin4 CZ=CCZ
135 134 eqcomi CCZ=CZ
136 133 135 eleqtrdi nCCZnCZ
137 132 136 sselid nCCZnZ
138 137 126 elind nCCZnZC
139 131 138 sselid nCCZnZ
140 139 adantl φnCCZnZ
141 77 eqcomd φnZ=Fn
142 simpl φnZφ
143 74 simpld φnZnC
144 142 143 7 syl2anc φnZFn=G
145 141 144 eqtr2d φnZG=
146 125 140 145 syl2anc φnCCZG=
147 125 146 jca φnCCZφG=
148 nfv kG=
149 1 148 nfan kφG=
150 nfv kD=0
151 149 150 nfim kφG=D=0
152 eqeq1 k=Gk=G=
153 152 anbi2d k=Gφk=φG=
154 3 eqeq1d k=GB=0D=0
155 153 154 imbi12d k=Gφk=B=0φG=D=0
156 114 151 155 9 vtoclgf GAφG=D=0
157 128 147 156 sylc φnCCZD=0
158 2 4 43 124 157 sge0ss φsum^nCZD=sum^nCD
159 29 108 158 3eqtrd φsum^kAB=sum^nCD