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 
|- F/ k ph
sge0fodjrnlem.n 
|- F/ n ph
sge0fodjrnlem.bd 
|- ( k = G -> B = D )
sge0fodjrnlem.c 
|- ( ph -> C e. V )
sge0fodjrnlem.f 
|- ( ph -> F : C -onto-> A )
sge0fodjrnlem.dj 
|- ( ph -> Disj_ n e. C ( F ` n ) )
sge0fodjrnlem.fng 
|- ( ( ph /\ n e. C ) -> ( F ` n ) = G )
sge0fodjrnlem.b 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
sge0fodjrnlem.b0 
|- ( ( ph /\ k = (/) ) -> B = 0 )
sge0fodjrnlem.z 
|- Z = ( `' F " { (/) } )
Assertion sge0fodjrnlem 
|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) = ( sum^ ` ( n e. C |-> D ) ) )

Proof

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