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 sselid
 |-  ( 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 sselid
 |-  ( 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 sselid
 |-  ( 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 ) ) )