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

Metamath Proof Explorer

Theorem sge0fodjrnlem

Proof