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		focdmex	|- ( 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	ffvelcdmda	|- ( ( 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		fvex	|- ( F ` n ) e. _V
48	47	elsn	|- ( ( F ` n ) e. { (/) } <-> ( F ` n ) = (/) )
49	48	bilanri	|- ( ( n e. ( C \ Z ) /\ ( F ` n ) = (/) ) -> ( F ` n ) e. { (/) } )
50	46 49	jca	|- ( ( n e. ( C \ Z ) /\ ( F ` n ) = (/) ) -> ( n e. C /\ ( F ` n ) e. { (/) } ) )
51	50	adantll	|- ( ( ( ph /\ n e. ( C \ Z ) ) /\ ( F ` n ) = (/) ) -> ( n e. C /\ ( F ` n ) e. { (/) } ) )
52	33	ffnd	|- ( ph -> F Fn C )
53		elpreima	|- ( F Fn C -> ( n e. ( `' F " { (/) } ) <-> ( n e. C /\ ( F ` n ) e. { (/) } ) ) )
54	52 53	syl	|- ( ph -> ( n e. ( `' F " { (/) } ) <-> ( n e. C /\ ( F ` n ) e. { (/) } ) ) )
55	54	ad2antrr	|- ( ( ( ph /\ n e. ( C \ Z ) ) /\ ( F ` n ) = (/) ) -> ( n e. ( `' F " { (/) } ) <-> ( n e. C /\ ( F ` n ) e. { (/) } ) ) )
56	51 55	mpbird	|- ( ( ( ph /\ n e. ( C \ Z ) ) /\ ( F ` n ) = (/) ) -> n e. ( `' F " { (/) } ) )
57	56 10	eleqtrrdi	|- ( ( ( ph /\ n e. ( C \ Z ) ) /\ ( F ` n ) = (/) ) -> n e. Z )
58		eldifn	|- ( n e. ( C \ Z ) -> -. n e. Z )
59	58	ad2antlr	|- ( ( ( ph /\ n e. ( C \ Z ) ) /\ ( F ` n ) = (/) ) -> -. n e. Z )
60	57 59	pm2.65da	|- ( ( ph /\ n e. ( C \ Z ) ) -> -. ( F ` n ) = (/) )
61	60	neqned	|- ( ( ph /\ n e. ( C \ Z ) ) -> ( F ` n ) =/= (/) )
62	44 61	jca	|- ( ( ph /\ n e. ( C \ Z ) ) -> ( n e. C /\ ( F ` n ) =/= (/) ) )
63	36	elrab	|- ( n e. { m e. C | ( F ` m ) =/= (/) } <-> ( n e. C /\ ( F ` n ) =/= (/) ) )
64	62 63	sylibr	|- ( ( ph /\ n e. ( C \ Z ) ) -> n e. { m e. C | ( F ` m ) =/= (/) } )
65	64	ex	|- ( ph -> ( n e. ( C \ Z ) -> n e. { m e. C | ( F ` m ) =/= (/) } ) )
66	63	simplbi	|- ( n e. { m e. C | ( F ` m ) =/= (/) } -> n e. C )
67	66	adantl	|- ( ( ph /\ n e. { m e. C | ( F ` m ) =/= (/) } ) -> n e. C )
68	10	eleq2i	|- ( n e. Z <-> n e. ( `' F " { (/) } ) )
69	68	bilani	|- ( ( ph /\ n e. Z ) -> n e. ( `' F " { (/) } ) )
70	54	adantr	|- ( ( ph /\ n e. Z ) -> ( n e. ( `' F " { (/) } ) <-> ( n e. C /\ ( F ` n ) e. { (/) } ) ) )
71	69 70	mpbid	|- ( ( ph /\ n e. Z ) -> ( n e. C /\ ( F ` n ) e. { (/) } ) )
72	71	simprd	|- ( ( ph /\ n e. Z ) -> ( F ` n ) e. { (/) } )
73		elsni	|- ( ( F ` n ) e. { (/) } -> ( F ` n ) = (/) )
74	72 73	syl	|- ( ( ph /\ n e. Z ) -> ( F ` n ) = (/) )
75	74	adantlr	|- ( ( ( ph /\ n e. { m e. C | ( F ` m ) =/= (/) } ) /\ n e. Z ) -> ( F ` n ) = (/) )
76	63	simprbi	|- ( n e. { m e. C | ( F ` m ) =/= (/) } -> ( F ` n ) =/= (/) )
77	76	ad2antlr	|- ( ( ( ph /\ n e. { m e. C | ( F ` m ) =/= (/) } ) /\ n e. Z ) -> ( F ` n ) =/= (/) )
78	77	neneqd	|- ( ( ( ph /\ n e. { m e. C | ( F ` m ) =/= (/) } ) /\ n e. Z ) -> -. ( F ` n ) = (/) )
79	75 78	pm2.65da	|- ( ( ph /\ n e. { m e. C | ( F ` m ) =/= (/) } ) -> -. n e. Z )
80	67 79	eldifd	|- ( ( ph /\ n e. { m e. C | ( F ` m ) =/= (/) } ) -> n e. ( C \ Z ) )
81	80	ex	|- ( ph -> ( n e. { m e. C | ( F ` m ) =/= (/) } -> n e. ( C \ Z ) ) )
82	2 81	ralrimi	|- ( ph -> A. n e. { m e. C | ( F ` m ) =/= (/) } n e. ( C \ Z ) )
83		dfss3	|- ( { m e. C | ( F ` m ) =/= (/) } C_ ( C \ Z ) <-> A. n e. { m e. C | ( F ` m ) =/= (/) } n e. ( C \ Z ) )
84	82 83	sylibr	|- ( ph -> { m e. C | ( F ` m ) =/= (/) } C_ ( C \ Z ) )
85	84	sseld	|- ( ph -> ( n e. { m e. C | ( F ` m ) =/= (/) } -> n e. ( C \ Z ) ) )
86	65 85	impbid	|- ( ph -> ( n e. ( C \ Z ) <-> n e. { m e. C | ( F ` m ) =/= (/) } ) )
87	2 86	alrimi	|- ( ph -> A. n ( n e. ( C \ Z ) <-> n e. { m e. C | ( F ` m ) =/= (/) } ) )
88		dfcleq	|- ( ( C \ Z ) = { m e. C | ( F ` m ) =/= (/) } <-> A. n ( n e. ( C \ Z ) <-> n e. { m e. C | ( F ` m ) =/= (/) } ) )
89	87 88	sylibr	|- ( ph -> ( C \ Z ) = { m e. C | ( F ` m ) =/= (/) } )
90	42 89	reseq12d	|- ( ph -> ( F |` ( C \ Z ) ) = ( ( n e. C |-> ( F ` n ) ) |` { m e. C | ( F ` m ) =/= (/) } ) )
91	42 38	eqtr4di	|- ( ph -> F = ( m e. C |-> ( F ` m ) ) )
92	91	eqcomd	|- ( ph -> ( m e. C |-> ( F ` m ) ) = F )
93	92	rneqd	|- ( ph -> ran ( m e. C |-> ( F ` m ) ) = ran F )
94		forn	|- ( F : C -onto-> A -> ran F = A )
95	5 94	syl	|- ( ph -> ran F = A )
96	93 95	eqtr2d	|- ( ph -> A = ran ( m e. C |-> ( F ` m ) ) )
97	96	difeq1d	|- ( ph -> ( A \ { (/) } ) = ( ran ( m e. C |-> ( F ` m ) ) \ { (/) } ) )
98	90 89 97	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 ) ) \ { (/) } ) ) )
99	41 98	mpbird	|- ( ph -> ( F |` ( C \ Z ) ) : ( C \ Z ) -1-1-onto-> ( A \ { (/) } ) )
100		fvres	|- ( n e. ( C \ Z ) -> ( ( F |` ( C \ Z ) ) ` n ) = ( F ` n ) )
101	100	adantl	|- ( ( ph /\ n e. ( C \ Z ) ) -> ( ( F |` ( C \ Z ) ) ` n ) = ( F ` n ) )
102		simpl	|- ( ( ph /\ n e. ( C \ Z ) ) -> ph )
103	102 44 7	syl2anc	|- ( ( ph /\ n e. ( C \ Z ) ) -> ( F ` n ) = G )
104	101 103	eqtrd	|- ( ( ph /\ n e. ( C \ Z ) ) -> ( ( F |` ( C \ Z ) ) ` n ) = G )
105	1 2 3 30 99 104 16	sge0f1o	|- ( ph -> ( sum^ ` ( k e. ( A \ { (/) } ) |-> B ) ) = ( sum^ ` ( n e. ( C \ Z ) |-> D ) ) )
106	7	eqcomd	|- ( ( ph /\ n e. C ) -> G = ( F ` n ) )
107	106 34	eqeltrd	|- ( ( ph /\ n e. C ) -> G e. A )
108	102 44 107	syl2anc	|- ( ( ph /\ n e. ( C \ Z ) ) -> G e. A )
109	108	ex	|- ( ph -> ( n e. ( C \ Z ) -> G e. A ) )
110	109	imdistani	|- ( ( ph /\ n e. ( C \ Z ) ) -> ( ph /\ G e. A ) )
111		nfcv	|- F/_ k G
112		nfv	|- F/ k G e. A
113	1 112	nfan	|- F/ k ( ph /\ G e. A )
114		nfv	|- F/ k D e. ( 0 [,] +oo )
115	113 114	nfim	|- F/ k ( ( ph /\ G e. A ) -> D e. ( 0 [,] +oo ) )
116		eleq1	|- ( k = G -> ( k e. A <-> G e. A ) )
117	116	anbi2d	|- ( k = G -> ( ( ph /\ k e. A ) <-> ( ph /\ G e. A ) ) )
118	3	eleq1d	|- ( k = G -> ( B e. ( 0 [,] +oo ) <-> D e. ( 0 [,] +oo ) ) )
119	117 118	imbi12d	|- ( k = G -> ( ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) ) <-> ( ( ph /\ G e. A ) -> D e. ( 0 [,] +oo ) ) ) )
120	111 115 119 8	vtoclgf	|- ( G e. A -> ( ( ph /\ G e. A ) -> D e. ( 0 [,] +oo ) ) )
121	108 110 120	sylc	|- ( ( ph /\ n e. ( C \ Z ) ) -> D e. ( 0 [,] +oo ) )
122		simpl	|- ( ( ph /\ n e. ( C \ ( C \ Z ) ) ) -> ph )
123		eldifi	|- ( n e. ( C \ ( C \ Z ) ) -> n e. C )
124	123	adantl	|- ( ( ph /\ n e. ( C \ ( C \ Z ) ) ) -> n e. C )
125	122 124 107	syl2anc	|- ( ( ph /\ n e. ( C \ ( C \ Z ) ) ) -> G e. A )
126		dfin4	|- ( Z i^i C ) = ( Z \ ( Z \ C ) )
127		difss	|- ( Z \ ( Z \ C ) ) C_ Z
128	126 127	eqsstri	|- ( Z i^i C ) C_ Z
129		inss2	|- ( C i^i Z ) C_ Z
130		id	|- ( n e. ( C \ ( C \ Z ) ) -> n e. ( C \ ( C \ Z ) ) )
131		dfin4	|- ( C i^i Z ) = ( C \ ( C \ Z ) )
132	131	eqcomi	|- ( C \ ( C \ Z ) ) = ( C i^i Z )
133	130 132	eleqtrdi	|- ( n e. ( C \ ( C \ Z ) ) -> n e. ( C i^i Z ) )
134	129 133	sselid	|- ( n e. ( C \ ( C \ Z ) ) -> n e. Z )
135	134 123	elind	|- ( n e. ( C \ ( C \ Z ) ) -> n e. ( Z i^i C ) )
136	128 135	sselid	|- ( n e. ( C \ ( C \ Z ) ) -> n e. Z )
137	136	adantl	|- ( ( ph /\ n e. ( C \ ( C \ Z ) ) ) -> n e. Z )
138	74	eqcomd	|- ( ( ph /\ n e. Z ) -> (/) = ( F ` n ) )
139		simpl	|- ( ( ph /\ n e. Z ) -> ph )
140	71	simpld	|- ( ( ph /\ n e. Z ) -> n e. C )
141	139 140 7	syl2anc	|- ( ( ph /\ n e. Z ) -> ( F ` n ) = G )
142	138 141	eqtr2d	|- ( ( ph /\ n e. Z ) -> G = (/) )
143	122 137 142	syl2anc	|- ( ( ph /\ n e. ( C \ ( C \ Z ) ) ) -> G = (/) )
144	122 143	jca	|- ( ( ph /\ n e. ( C \ ( C \ Z ) ) ) -> ( ph /\ G = (/) ) )
145		nfv	|- F/ k G = (/)
146	1 145	nfan	|- F/ k ( ph /\ G = (/) )
147		nfv	|- F/ k D = 0
148	146 147	nfim	|- F/ k ( ( ph /\ G = (/) ) -> D = 0 )
149		eqeq1	|- ( k = G -> ( k = (/) <-> G = (/) ) )
150	149	anbi2d	|- ( k = G -> ( ( ph /\ k = (/) ) <-> ( ph /\ G = (/) ) ) )
151	3	eqeq1d	|- ( k = G -> ( B = 0 <-> D = 0 ) )
152	150 151	imbi12d	|- ( k = G -> ( ( ( ph /\ k = (/) ) -> B = 0 ) <-> ( ( ph /\ G = (/) ) -> D = 0 ) ) )
153	111 148 152 9	vtoclgf	|- ( G e. A -> ( ( ph /\ G = (/) ) -> D = 0 ) )
154	125 144 153	sylc	|- ( ( ph /\ n e. ( C \ ( C \ Z ) ) ) -> D = 0 )
155	2 4 43 121 154	sge0ss	|- ( ph -> ( sum^ ` ( n e. ( C \ Z ) |-> D ) ) = ( sum^ ` ( n e. C |-> D ) ) )
156	29 105 155	3eqtrd	|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) = ( sum^ ` ( n e. C |-> D ) ) )