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

Metamath Proof Explorer

Theorem sge0fodjrnlem

Proof