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 \to B = D$
	sge0fodjrnlem.c	$⊢ φ \to C \in V$
	sge0fodjrnlem.f	$⊢ φ \to F : C \underset{onto}{⟶} A$
	sge0fodjrnlem.dj	$⊢ φ \to \underset{n \in C}{Disj} F (n)$
	sge0fodjrnlem.fng	$⊢ (φ \land n \in C) \to F (n) = G$
	sge0fodjrnlem.b	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
	sge0fodjrnlem.b0	$⊢ (φ \land k = \emptyset) \to B = 0$
	sge0fodjrnlem.z	$⊢ Z = F^{-1} [\{\emptyset\}]$
Assertion	sge0fodjrnlem	$⊢ φ \to sum^((k \in A ⟼ B)) = sum^((n \in C ⟼ D))$

Proof

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

Metamath Proof Explorer

Theorem sge0fodjrnlem

Proof