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 = G B = D
sge0fodjrnlem.c φ C V
sge0fodjrnlem.f φ F : C onto A
sge0fodjrnlem.dj φ Disj n C F n
sge0fodjrnlem.fng φ n C F n = G
sge0fodjrnlem.b φ k A B 0 +∞
sge0fodjrnlem.b0 φ k = B = 0
sge0fodjrnlem.z Z = F -1
Assertion sge0fodjrnlem φ sum^ k A B = sum^ n C D

Proof

Step Hyp Ref Expression
1 sge0fodjrnlem.k k φ
2 sge0fodjrnlem.n n φ
3 sge0fodjrnlem.bd k = G B = D
4 sge0fodjrnlem.c φ C V
5 sge0fodjrnlem.f φ F : C onto A
6 sge0fodjrnlem.dj φ Disj n C F n
7 sge0fodjrnlem.fng φ n C F n = G
8 sge0fodjrnlem.b φ k A B 0 +∞
9 sge0fodjrnlem.b0 φ k = B = 0
10 sge0fodjrnlem.z Z = F -1
11 fornex C V F : C onto A A V
12 4 5 11 sylc φ A V
13 difssd φ A A
14 simpl φ k A φ
15 13 sselda φ k A k A
16 14 15 8 syl2anc φ k A B 0 +∞
17 simpl φ k A A φ
18 dfin4 A = A A
19 18 eqcomi A A = A
20 inss2 A
21 19 20 eqsstri A A
22 id k A A k A A
23 21 22 sselid k A A k
24 elsni k k =
25 23 24 syl k A A k =
26 25 adantl φ k A A k =
27 17 26 9 syl2anc φ k A A B = 0
28 1 12 13 16 27 sge0ss φ sum^ k A B = sum^ k A B
29 28 eqcomd φ sum^ k A B = sum^ k A B
30 4 difexd φ C Z V
31 eqid n C F n = n C F n
32 fof F : C onto A F : C A
33 5 32 syl φ F : C A
34 33 ffvelrnda φ n C F n A
35 fveq2 m = n F m = F n
36 35 neeq1d m = n F m F n
37 36 cbvrabv m C | F m = n C | F n
38 35 cbvmptv m C F m = n C F n
39 38 rneqi ran m C F m = ran n C F n
40 39 difeq1i ran m C F m = ran n C F n
41 2 31 34 6 37 40 disjf1o φ n C F n m C | F m : m C | F m 1-1 onto ran m C F m
42 33 feqmptd φ F = n C F n
43 difssd φ C Z C
44 43 sselda φ n C Z n C
45 eldifi n C Z n C
46 45 adantr n C Z F n = n C
47 id F n = F n =
48 fvex F n V
49 48 elsn F n F n =
50 47 49 sylibr F n = F n
51 50 adantl n C Z F n = F n
52 46 51 jca n C Z F n = n C F n
53 52 adantll φ n C Z F n = n C F n
54 33 ffnd φ F Fn C
55 elpreima F Fn C n F -1 n C F n
56 54 55 syl φ n F -1 n C F n
57 56 ad2antrr φ n C Z F n = n F -1 n C F n
58 53 57 mpbird φ n C Z F n = n F -1
59 58 10 eleqtrrdi φ n C Z F n = n Z
60 eldifn n C Z ¬ n Z
61 60 ad2antlr φ n C Z F n = ¬ n Z
62 59 61 pm2.65da φ n C Z ¬ F n =
63 62 neqned φ n C Z F n
64 44 63 jca φ n C Z n C F n
65 36 elrab n m C | F m n C F n
66 64 65 sylibr φ n C Z n m C | F m
67 66 ex φ n C Z n m C | F m
68 65 simplbi n m C | F m n C
69 68 adantl φ n m C | F m n C
70 10 eleq2i n Z n F -1
71 70 biimpi n Z n F -1
72 71 adantl φ n Z n F -1
73 56 adantr φ n Z n F -1 n C F n
74 72 73 mpbid φ n Z n C F n
75 74 simprd φ n Z F n
76 elsni F n F n =
77 75 76 syl φ n Z F n =
78 77 adantlr φ n m C | F m n Z F n =
79 65 simprbi n m C | F m F n
80 79 ad2antlr φ n m C | F m n Z F n
81 80 neneqd φ n m C | F m n Z ¬ F n =
82 78 81 pm2.65da φ n m C | F m ¬ n Z
83 69 82 eldifd φ n m C | F m n C Z
84 83 ex φ n m C | F m n C Z
85 2 84 ralrimi φ n m C | F m n C Z
86 dfss3 m C | F m C Z n m C | F m n C Z
87 85 86 sylibr φ m C | F m C Z
88 87 sseld φ n m C | F m n C Z
89 67 88 impbid φ n C Z n m C | F m
90 2 89 alrimi φ n n C Z n m C | F m
91 dfcleq C Z = m C | F m n n C Z n m C | F m
92 90 91 sylibr φ C Z = m C | F m
93 42 92 reseq12d φ F C Z = n C F n m C | F m
94 42 38 eqtr4di φ F = m C F m
95 94 eqcomd φ m C F m = F
96 95 rneqd φ ran m C F m = ran F
97 forn F : C onto A ran F = A
98 5 97 syl φ ran F = A
99 96 98 eqtr2d φ A = ran m C F m
100 99 difeq1d φ A = ran m C F m
101 93 92 100 f1oeq123d φ F C Z : C Z 1-1 onto A n C F n m C | F m : m C | F m 1-1 onto ran m C F m
102 41 101 mpbird φ F C Z : C Z 1-1 onto A
103 fvres n C Z F C Z n = F n
104 103 adantl φ n C Z F C Z n = F n
105 simpl φ n C Z φ
106 105 44 7 syl2anc φ n C Z F n = G
107 104 106 eqtrd φ n C Z F C Z n = G
108 1 2 3 30 102 107 16 sge0f1o φ sum^ k A B = sum^ n C Z D
109 7 eqcomd φ n C G = F n
110 109 34 eqeltrd φ n C G A
111 105 44 110 syl2anc φ n C Z G A
112 111 ex φ n C Z G A
113 112 imdistani φ n C Z φ G A
114 nfcv _ k G
115 nfv k G A
116 1 115 nfan k φ G A
117 nfv k D 0 +∞
118 116 117 nfim k φ G A D 0 +∞
119 eleq1 k = G k A G A
120 119 anbi2d k = G φ k A φ G A
121 3 eleq1d k = G B 0 +∞ D 0 +∞
122 120 121 imbi12d k = G φ k A B 0 +∞ φ G A D 0 +∞
123 114 118 122 8 vtoclgf G A φ G A D 0 +∞
124 111 113 123 sylc φ n C Z D 0 +∞
125 simpl φ n C C Z φ
126 eldifi n C C Z n C
127 126 adantl φ n C C Z n C
128 125 127 110 syl2anc φ n C C Z G A
129 dfin4 Z C = Z Z C
130 difss Z Z C Z
131 129 130 eqsstri Z C Z
132 inss2 C Z Z
133 id n C C Z n C C Z
134 dfin4 C Z = C C Z
135 134 eqcomi C C Z = C Z
136 133 135 eleqtrdi n C C Z n C Z
137 132 136 sselid n C C Z n Z
138 137 126 elind n C C Z n Z C
139 131 138 sselid n C C Z n Z
140 139 adantl φ n C C Z n Z
141 77 eqcomd φ n Z = F n
142 simpl φ n Z φ
143 74 simpld φ n Z n C
144 142 143 7 syl2anc φ n Z F n = G
145 141 144 eqtr2d φ n Z G =
146 125 140 145 syl2anc φ n C C Z G =
147 125 146 jca φ n C C Z φ G =
148 nfv k G =
149 1 148 nfan k φ G =
150 nfv k D = 0
151 149 150 nfim k φ G = D = 0
152 eqeq1 k = G k = G =
153 152 anbi2d k = G φ k = φ G =
154 3 eqeq1d k = G B = 0 D = 0
155 153 154 imbi12d k = G φ k = B = 0 φ G = D = 0
156 114 151 155 9 vtoclgf G A φ G = D = 0
157 128 147 156 sylc φ n C C Z D = 0
158 2 4 43 124 157 sge0ss φ sum^ n C Z D = sum^ n C D
159 29 108 158 3eqtrd φ sum^ k A B = sum^ n C D