sge0f1o

Description: Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0f1o.1	$⊢ Ⅎ k φ$
	sge0f1o.2	$⊢ Ⅎ n φ$
	sge0f1o.3	$⊢ k = G \to B = D$
	sge0f1o.4	$⊢ φ \to C \in V$
	sge0f1o.5	$⊢ φ \to F : C \underset{1-1 onto}{⟶} A$
	sge0f1o.6	$⊢ (φ \land n \in C) \to F (n) = G$
	sge0f1o.7	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
Assertion	sge0f1o	$⊢ φ \to sum^((k \in A ⟼ B)) = sum^((n \in C ⟼ D))$

Proof

Step	Hyp	Ref	Expression
1		sge0f1o.1	$⊢ Ⅎ k φ$
2		sge0f1o.2	$⊢ Ⅎ n φ$
3		sge0f1o.3	$⊢ k = G \to B = D$
4		sge0f1o.4	$⊢ φ \to C \in V$
5		sge0f1o.5	$⊢ φ \to F : C \underset{1-1 onto}{⟶} A$
6		sge0f1o.6	$⊢ (φ \land n \in C) \to F (n) = G$
7		sge0f1o.7	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
8		f1ofo	$⊢ F : C \underset{1-1 onto}{⟶} A \to F : C \underset{onto}{⟶} A$
9	5 8	syl	$⊢ φ \to F : C \underset{onto}{⟶} A$
10		fornex	$⊢ C \in V \to (F : C \underset{onto}{⟶} A \to A \in V)$
11	4 9 10	sylc	$⊢ φ \to A \in V$
12	11	adantr	$⊢ (φ \land +∞ \in ran (n \in C ⟼ D)) \to A \in V$
13		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
14	1 7 13	fmptdf	$⊢ φ \to (k \in A ⟼ B) : A ⟶ [0, +∞]$
15	14	adantr	$⊢ (φ \land +∞ \in ran (n \in C ⟼ D)) \to (k \in A ⟼ B) : A ⟶ [0, +∞]$
16		pnfex	$⊢ +∞ \in V$
17		eqid	$⊢ (n \in C ⟼ D) = (n \in C ⟼ D)$
18	17	elrnmpt	$⊢ +∞ \in V \to (+∞ \in ran (n \in C ⟼ D) \leftrightarrow \exists n \in C +∞ = D)$
19	16 18	ax-mp	$⊢ +∞ \in ran (n \in C ⟼ D) \leftrightarrow \exists n \in C +∞ = D$
20	19	biimpi	$⊢ +∞ \in ran (n \in C ⟼ D) \to \exists n \in C +∞ = D$
21	20	adantl	$⊢ (φ \land +∞ \in ran (n \in C ⟼ D)) \to \exists n \in C +∞ = D$
22		nfv	$⊢ Ⅎ n +∞ \in ran (k \in A ⟼ B)$
23		simp3	$⊢ (φ \land n \in C \land +∞ = D) \to +∞ = D$
24		f1of	$⊢ F : C \underset{1-1 onto}{⟶} A \to F : C ⟶ A$
25	5 24	syl	$⊢ φ \to F : C ⟶ A$
26	25	ffvelrnda	$⊢ (φ \land n \in C) \to F (n) \in A$
27		nfcv	$⊢ \underline{Ⅎ} k F (n)$
28		nfv	$⊢ Ⅎ k F (n) = G$
29	27	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ F (n) / k ⦌ B$
30		nfcv	$⊢ \underline{Ⅎ} k D$
31	29 30	nfeq	$⊢ Ⅎ k ⦋ F (n) / k ⦌ B = D$
32	28 31	nfim	$⊢ Ⅎ k (F (n) = G \to ⦋ F (n) / k ⦌ B = D)$
33		eqeq1	$⊢ k = F (n) \to (k = G \leftrightarrow F (n) = G)$
34		csbeq1a	$⊢ k = F (n) \to B = ⦋ F (n) / k ⦌ B$
35	34	eqeq1d	$⊢ k = F (n) \to (B = D \leftrightarrow ⦋ F (n) / k ⦌ B = D)$
36	33 35	imbi12d	$⊢ k = F (n) \to ((k = G \to B = D) \leftrightarrow (F (n) = G \to ⦋ F (n) / k ⦌ B = D))$
37	27 32 36 3	vtoclgf	$⊢ F (n) \in A \to (F (n) = G \to ⦋ F (n) / k ⦌ B = D)$
38	26 6 37	sylc	$⊢ (φ \land n \in C) \to ⦋ F (n) / k ⦌ B = D$
39	38	eqcomd	$⊢ (φ \land n \in C) \to D = ⦋ F (n) / k ⦌ B$
40	39	3adant3	$⊢ (φ \land n \in C \land +∞ = D) \to D = ⦋ F (n) / k ⦌ B$
41	23 40	eqtrd	$⊢ (φ \land n \in C \land +∞ = D) \to +∞ = ⦋ F (n) / k ⦌ B$
42		simpl	$⊢ (φ \land n \in C) \to φ$
43	42 26	jca	$⊢ (φ \land n \in C) \to (φ \land F (n) \in A)$
44		nfv	$⊢ Ⅎ k F (n) \in A$
45	1 44	nfan	$⊢ Ⅎ k (φ \land F (n) \in A)$
46	29	nfel1	$⊢ Ⅎ k ⦋ F (n) / k ⦌ B \in [0, +∞]$
47	45 46	nfim	$⊢ Ⅎ k ((φ \land F (n) \in A) \to ⦋ F (n) / k ⦌ B \in [0, +∞])$
48		eleq1	$⊢ k = F (n) \to (k \in A \leftrightarrow F (n) \in A)$
49	48	anbi2d	$⊢ k = F (n) \to ((φ \land k \in A) \leftrightarrow (φ \land F (n) \in A))$
50	34	eleq1d	$⊢ k = F (n) \to (B \in [0, +∞] \leftrightarrow ⦋ F (n) / k ⦌ B \in [0, +∞])$
51	49 50	imbi12d	$⊢ k = F (n) \to (((φ \land k \in A) \to B \in [0, +∞]) \leftrightarrow ((φ \land F (n) \in A) \to ⦋ F (n) / k ⦌ B \in [0, +∞]))$
52	27 47 51 7	vtoclgf	$⊢ F (n) \in A \to ((φ \land F (n) \in A) \to ⦋ F (n) / k ⦌ B \in [0, +∞])$
53	26 43 52	sylc	$⊢ (φ \land n \in C) \to ⦋ F (n) / k ⦌ B \in [0, +∞]$
54	29 13 34	elrnmpt1sf	$⊢ (F (n) \in A \land ⦋ F (n) / k ⦌ B \in [0, +∞]) \to ⦋ F (n) / k ⦌ B \in ran (k \in A ⟼ B)$
55	26 53 54	syl2anc	$⊢ (φ \land n \in C) \to ⦋ F (n) / k ⦌ B \in ran (k \in A ⟼ B)$
56	55	3adant3	$⊢ (φ \land n \in C \land +∞ = D) \to ⦋ F (n) / k ⦌ B \in ran (k \in A ⟼ B)$
57	41 56	eqeltrd	$⊢ (φ \land n \in C \land +∞ = D) \to +∞ \in ran (k \in A ⟼ B)$
58	57	3exp	$⊢ φ \to (n \in C \to (+∞ = D \to +∞ \in ran (k \in A ⟼ B)))$
59	2 22 58	rexlimd	$⊢ φ \to (\exists n \in C +∞ = D \to +∞ \in ran (k \in A ⟼ B))$
60	59	adantr	$⊢ (φ \land +∞ \in ran (n \in C ⟼ D)) \to (\exists n \in C +∞ = D \to +∞ \in ran (k \in A ⟼ B))$
61	21 60	mpd	$⊢ (φ \land +∞ \in ran (n \in C ⟼ D)) \to +∞ \in ran (k \in A ⟼ B)$
62	12 15 61	sge0pnfval	$⊢ (φ \land +∞ \in ran (n \in C ⟼ D)) \to sum^((k \in A ⟼ B)) = +∞$
63	4	adantr	$⊢ (φ \land +∞ \in ran (n \in C ⟼ D)) \to C \in V$
64	39 53	eqeltrd	$⊢ (φ \land n \in C) \to D \in [0, +∞]$
65	2 64 17	fmptdf	$⊢ φ \to (n \in C ⟼ D) : C ⟶ [0, +∞]$
66	65	adantr	$⊢ (φ \land +∞ \in ran (n \in C ⟼ D)) \to (n \in C ⟼ D) : C ⟶ [0, +∞]$
67		simpr	$⊢ (φ \land +∞ \in ran (n \in C ⟼ D)) \to +∞ \in ran (n \in C ⟼ D)$
68	63 66 67	sge0pnfval	$⊢ (φ \land +∞ \in ran (n \in C ⟼ D)) \to sum^((n \in C ⟼ D)) = +∞$
69	62 68	eqtr4d	$⊢ (φ \land +∞ \in ran (n \in C ⟼ D)) \to sum^((k \in A ⟼ B)) = sum^((n \in C ⟼ D))$
70		sumex	$⊢ \sum_{k \in y} B \in V$
71	70	a1i	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \to \sum_{k \in y} B \in V$
72		cnvimass	$⊢ F^{-1} [y] \subseteq dom F$
73	72 25	fssdm	$⊢ φ \to F^{-1} [y] \subseteq C$
74	25 4	fexd	$⊢ φ \to F \in V$
75		cnvexg	$⊢ F \in V \to F^{-1} \in V$
76	74 75	syl	$⊢ φ \to F^{-1} \in V$
77		imaexg	$⊢ F^{-1} \in V \to F^{-1} [y] \in V$
78	76 77	syl	$⊢ φ \to F^{-1} [y] \in V$
79		elpwg	$⊢ F^{-1} [y] \in V \to (F^{-1} [y] \in 𝒫 C \leftrightarrow F^{-1} [y] \subseteq C)$
80	78 79	syl	$⊢ φ \to (F^{-1} [y] \in 𝒫 C \leftrightarrow F^{-1} [y] \subseteq C)$
81	73 80	mpbird	$⊢ φ \to F^{-1} [y] \in 𝒫 C$
82	81	adantr	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to F^{-1} [y] \in 𝒫 C$
83		f1ocnv	$⊢ F : C \underset{1-1 onto}{⟶} A \to F^{-1} : A \underset{1-1 onto}{⟶} C$
84	5 83	syl	$⊢ φ \to F^{-1} : A \underset{1-1 onto}{⟶} C$
85		f1ofun	$⊢ F^{-1} : A \underset{1-1 onto}{⟶} C \to Fun F^{-1}$
86	84 85	syl	$⊢ φ \to Fun F^{-1}$
87	86	adantr	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to Fun F^{-1}$
88		elinel2	$⊢ y \in (𝒫 A \cap Fin) \to y \in Fin$
89	88	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \in Fin$
90		imafi	$⊢ (Fun F^{-1} \land y \in Fin) \to F^{-1} [y] \in Fin$
91	87 89 90	syl2anc	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to F^{-1} [y] \in Fin$
92	82 91	elind	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to F^{-1} [y] \in (𝒫 C \cap Fin)$
93	92	adantlr	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \to F^{-1} [y] \in (𝒫 C \cap Fin)$
94		nfv	$⊢ Ⅎ k \neg +∞ \in ran (n \in C ⟼ D)$
95	1 94	nfan	$⊢ Ⅎ k (φ \land \neg +∞ \in ran (n \in C ⟼ D))$
96		nfv	$⊢ Ⅎ k y \in (𝒫 A \cap Fin)$
97	95 96	nfan	$⊢ Ⅎ k ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin))$
98		nfcv	$⊢ \underline{Ⅎ} n +∞$
99		nfmpt1	$⊢ \underline{Ⅎ} n (n \in C ⟼ D)$
100	99	nfrn	$⊢ \underline{Ⅎ} n ran (n \in C ⟼ D)$
101	98 100	nfel	$⊢ Ⅎ n +∞ \in ran (n \in C ⟼ D)$
102	101	nfn	$⊢ Ⅎ n \neg +∞ \in ran (n \in C ⟼ D)$
103	2 102	nfan	$⊢ Ⅎ n (φ \land \neg +∞ \in ran (n \in C ⟼ D))$
104		nfv	$⊢ Ⅎ n y \in (𝒫 A \cap Fin)$
105	103 104	nfan	$⊢ Ⅎ n ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin))$
106	91	adantlr	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \to F^{-1} [y] \in Fin$
107		f1of1	$⊢ F : C \underset{1-1 onto}{⟶} A \to F : C \underset{1-1}{⟶} A$
108	5 107	syl	$⊢ φ \to F : C \underset{1-1}{⟶} A$
109	108	adantr	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to F : C \underset{1-1}{⟶} A$
110	80	adantr	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to (F^{-1} [y] \in 𝒫 C \leftrightarrow F^{-1} [y] \subseteq C)$
111	82 110	mpbid	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to F^{-1} [y] \subseteq C$
112		f1ores	$⊢ (F : C \underset{1-1}{⟶} A \land F^{-1} [y] \subseteq C) \to ({F ↾}_{F^{-1} [y]}) : F^{-1} [y] \underset{1-1 onto}{⟶} F [F^{-1} [y]]$
113	109 111 112	syl2anc	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to ({F ↾}_{F^{-1} [y]}) : F^{-1} [y] \underset{1-1 onto}{⟶} F [F^{-1} [y]]$
114	9	adantr	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to F : C \underset{onto}{⟶} A$
115		elpwinss	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
116	115	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \subseteq A$
117		foimacnv	$⊢ (F : C \underset{onto}{⟶} A \land y \subseteq A) \to F [F^{-1} [y]] = y$
118	114 116 117	syl2anc	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to F [F^{-1} [y]] = y$
119	118	f1oeq3d	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to (({F ↾}_{F^{-1} [y]}) : F^{-1} [y] \underset{1-1 onto}{⟶} F [F^{-1} [y]] \leftrightarrow ({F ↾}_{F^{-1} [y]}) : F^{-1} [y] \underset{1-1 onto}{⟶} y)$
120	113 119	mpbid	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to ({F ↾}_{F^{-1} [y]}) : F^{-1} [y] \underset{1-1 onto}{⟶} y$
121	120	adantlr	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \to ({F ↾}_{F^{-1} [y]}) : F^{-1} [y] \underset{1-1 onto}{⟶} y$
122	78	ad2antrr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land n \in F^{-1} [y]) \to F^{-1} [y] \in V$
123		simpll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land n \in F^{-1} [y]) \to φ$
124	92	adantr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land n \in F^{-1} [y]) \to F^{-1} [y] \in (𝒫 C \cap Fin)$
125		simpr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land n \in F^{-1} [y]) \to n \in F^{-1} [y]$
126	123 124 125	jca31	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land n \in F^{-1} [y]) \to ((φ \land F^{-1} [y] \in (𝒫 C \cap Fin)) \land n \in F^{-1} [y])$
127		eleq1	$⊢ x = F^{-1} [y] \to (x \in (𝒫 C \cap Fin) \leftrightarrow F^{-1} [y] \in (𝒫 C \cap Fin))$
128	127	anbi2d	$⊢ x = F^{-1} [y] \to ((φ \land x \in (𝒫 C \cap Fin)) \leftrightarrow (φ \land F^{-1} [y] \in (𝒫 C \cap Fin)))$
129		eleq2	$⊢ x = F^{-1} [y] \to (n \in x \leftrightarrow n \in F^{-1} [y])$
130	128 129	anbi12d	$⊢ x = F^{-1} [y] \to (((φ \land x \in (𝒫 C \cap Fin)) \land n \in x) \leftrightarrow ((φ \land F^{-1} [y] \in (𝒫 C \cap Fin)) \land n \in F^{-1} [y]))$
131		reseq2	$⊢ x = F^{-1} [y] \to {F ↾}_{x} = {F ↾}_{F^{-1} [y]}$
132	131	fveq1d	$⊢ x = F^{-1} [y] \to ({F ↾}_{x}) (n) = ({F ↾}_{F^{-1} [y]}) (n)$
133	132	eqeq1d	$⊢ x = F^{-1} [y] \to (({F ↾}_{x}) (n) = G \leftrightarrow ({F ↾}_{F^{-1} [y]}) (n) = G)$
134	130 133	imbi12d	$⊢ x = F^{-1} [y] \to ((((φ \land x \in (𝒫 C \cap Fin)) \land n \in x) \to ({F ↾}_{x}) (n) = G) \leftrightarrow (((φ \land F^{-1} [y] \in (𝒫 C \cap Fin)) \land n \in F^{-1} [y]) \to ({F ↾}_{F^{-1} [y]}) (n) = G))$
135		fvres	$⊢ n \in x \to ({F ↾}_{x}) (n) = F (n)$
136	135	adantl	$⊢ ((φ \land x \in (𝒫 C \cap Fin)) \land n \in x) \to ({F ↾}_{x}) (n) = F (n)$
137		simpll	$⊢ ((φ \land x \in (𝒫 C \cap Fin)) \land n \in x) \to φ$
138		elpwinss	$⊢ x \in (𝒫 C \cap Fin) \to x \subseteq C$
139	138	adantl	$⊢ (φ \land x \in (𝒫 C \cap Fin)) \to x \subseteq C$
140	139	sselda	$⊢ ((φ \land x \in (𝒫 C \cap Fin)) \land n \in x) \to n \in C$
141	137 140 6	syl2anc	$⊢ ((φ \land x \in (𝒫 C \cap Fin)) \land n \in x) \to F (n) = G$
142	136 141	eqtrd	$⊢ ((φ \land x \in (𝒫 C \cap Fin)) \land n \in x) \to ({F ↾}_{x}) (n) = G$
143	134 142	vtoclg	$⊢ F^{-1} [y] \in V \to (((φ \land F^{-1} [y] \in (𝒫 C \cap Fin)) \land n \in F^{-1} [y]) \to ({F ↾}_{F^{-1} [y]}) (n) = G)$
144	122 126 143	sylc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land n \in F^{-1} [y]) \to ({F ↾}_{F^{-1} [y]}) (n) = G$
145	144	adantllr	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \land n \in F^{-1} [y]) \to ({F ↾}_{F^{-1} [y]}) (n) = G$
146	78	ad3antrrr	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \land k \in y) \to F^{-1} [y] \in V$
147		simpll	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \land k \in y) \to (φ \land \neg +∞ \in ran (n \in C ⟼ D))$
148	81	ad3antrrr	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \land k \in y) \to F^{-1} [y] \in 𝒫 C$
149	106	adantr	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \land k \in y) \to F^{-1} [y] \in Fin$
150	148 149	elind	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \land k \in y) \to F^{-1} [y] \in (𝒫 C \cap Fin)$
151		simpr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to k \in y$
152	118	eqcomd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y = F [F^{-1} [y]]$
153	152	adantr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to y = F [F^{-1} [y]]$
154	151 153	eleqtrd	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to k \in F [F^{-1} [y]]$
155	154	adantllr	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \land k \in y) \to k \in F [F^{-1} [y]]$
156	147 150 155	jca31	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \land k \in y) \to (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land F^{-1} [y] \in (𝒫 C \cap Fin)) \land k \in F [F^{-1} [y]])$
157	127	anbi2d	$⊢ x = F^{-1} [y] \to (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \leftrightarrow ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land F^{-1} [y] \in (𝒫 C \cap Fin)))$
158		imaeq2	$⊢ x = F^{-1} [y] \to F [x] = F [F^{-1} [y]]$
159	158	eleq2d	$⊢ x = F^{-1} [y] \to (k \in F [x] \leftrightarrow k \in F [F^{-1} [y]])$
160	157 159	anbi12d	$⊢ x = F^{-1} [y] \to ((((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \land k \in F [x]) \leftrightarrow (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land F^{-1} [y] \in (𝒫 C \cap Fin)) \land k \in F [F^{-1} [y]]))$
161	160	imbi1d	$⊢ x = F^{-1} [y] \to (((((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \land k \in F [x]) \to B \in ℂ) \leftrightarrow ((((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land F^{-1} [y] \in (𝒫 C \cap Fin)) \land k \in F [F^{-1} [y]]) \to B \in ℂ))$
162		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
163		ax-resscn	$⊢ ℝ \subseteq ℂ$
164	162 163	sstri	$⊢ [0, +∞) \subseteq ℂ$
165		simplll	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \land k \in F [x]) \to φ$
166		simpllr	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \land k \in F [x]) \to \neg +∞ \in ran (n \in C ⟼ D)$
167		fimass	$⊢ F : C ⟶ A \to F [x] \subseteq A$
168	25 167	syl	$⊢ φ \to F [x] \subseteq A$
169	168	ad2antrr	$⊢ ((φ \land x \in (𝒫 C \cap Fin)) \land k \in F [x]) \to F [x] \subseteq A$
170		simpr	$⊢ ((φ \land x \in (𝒫 C \cap Fin)) \land k \in F [x]) \to k \in F [x]$
171	169 170	sseldd	$⊢ ((φ \land x \in (𝒫 C \cap Fin)) \land k \in F [x]) \to k \in A$
172	171	adantllr	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \land k \in F [x]) \to k \in A$
173		foelrni	$⊢ (F : C \underset{onto}{⟶} A \land k \in A) \to \exists n \in C F (n) = k$
174	9 173	sylan	$⊢ (φ \land k \in A) \to \exists n \in C F (n) = k$
175	174	adantlr	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land k \in A) \to \exists n \in C F (n) = k$
176		nfv	$⊢ Ⅎ n k \in A$
177	103 176	nfan	$⊢ Ⅎ n ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land k \in A)$
178		nfv	$⊢ Ⅎ n B \in [0, +∞)$
179		csbid	$⊢ ⦋ k / k ⦌ B = B$
180	179	eqcomi	$⊢ B = ⦋ k / k ⦌ B$
181	180	a1i	$⊢ (φ \land n \in C \land F (n) = k) \to B = ⦋ k / k ⦌ B$
182		id	$⊢ F (n) = k \to F (n) = k$
183	182	eqcomd	$⊢ F (n) = k \to k = F (n)$
184	183	csbeq1d	$⊢ F (n) = k \to ⦋ k / k ⦌ B = ⦋ F (n) / k ⦌ B$
185	184	3ad2ant3	$⊢ (φ \land n \in C \land F (n) = k) \to ⦋ k / k ⦌ B = ⦋ F (n) / k ⦌ B$
186	38	idi	$⊢ (φ \land n \in C) \to ⦋ F (n) / k ⦌ B = D$
187	186	3adant3	$⊢ (φ \land n \in C \land F (n) = k) \to ⦋ F (n) / k ⦌ B = D$
188	181 185 187	3eqtrd	$⊢ (φ \land n \in C \land F (n) = k) \to B = D$
189	188	3adant1r	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land n \in C \land F (n) = k) \to B = D$
190		0xr	$⊢ 0 \in ℝ^{*}$
191	190	a1i	$⊢ ((φ \land n \in C) \land \neg D \in [0, +∞)) \to 0 \in ℝ^{*}$
192		pnfxr	$⊢ +∞ \in ℝ^{*}$
193	192	a1i	$⊢ ((φ \land n \in C) \land \neg D \in [0, +∞)) \to +∞ \in ℝ^{*}$
194	64	adantr	$⊢ ((φ \land n \in C) \land \neg D \in [0, +∞)) \to D \in [0, +∞]$
195		simpr	$⊢ ((φ \land n \in C) \land \neg D \in [0, +∞)) \to \neg D \in [0, +∞)$
196	191 193 194 195	eliccnelico	$⊢ ((φ \land n \in C) \land \neg D \in [0, +∞)) \to D = +∞$
197	196	eqcomd	$⊢ ((φ \land n \in C) \land \neg D \in [0, +∞)) \to +∞ = D$
198		simpr	$⊢ (φ \land n \in C) \to n \in C$
199	64	idi	$⊢ (φ \land n \in C) \to D \in [0, +∞]$
200	17	elrnmpt1	$⊢ (n \in C \land D \in [0, +∞]) \to D \in ran (n \in C ⟼ D)$
201	198 199 200	syl2anc	$⊢ (φ \land n \in C) \to D \in ran (n \in C ⟼ D)$
202	201	adantr	$⊢ ((φ \land n \in C) \land \neg D \in [0, +∞)) \to D \in ran (n \in C ⟼ D)$
203	197 202	eqeltrd	$⊢ ((φ \land n \in C) \land \neg D \in [0, +∞)) \to +∞ \in ran (n \in C ⟼ D)$
204	203	adantllr	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land n \in C) \land \neg D \in [0, +∞)) \to +∞ \in ran (n \in C ⟼ D)$
205		simpllr	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land n \in C) \land \neg D \in [0, +∞)) \to \neg +∞ \in ran (n \in C ⟼ D)$
206	204 205	condan	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land n \in C) \to D \in [0, +∞)$
207	206	3adant3	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land n \in C \land F (n) = k) \to D \in [0, +∞)$
208	189 207	eqeltrd	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land n \in C \land F (n) = k) \to B \in [0, +∞)$
209	208	3exp	$⊢ (φ \land \neg +∞ \in ran (n \in C ⟼ D)) \to (n \in C \to (F (n) = k \to B \in [0, +∞)))$
210	209	adantr	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land k \in A) \to (n \in C \to (F (n) = k \to B \in [0, +∞)))$
211	177 178 210	rexlimd	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land k \in A) \to (\exists n \in C F (n) = k \to B \in [0, +∞))$
212	175 211	mpd	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land k \in A) \to B \in [0, +∞)$
213	165 166 172 212	syl21anc	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \land k \in F [x]) \to B \in [0, +∞)$
214	164 213	sselid	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \land k \in F [x]) \to B \in ℂ$
215	214	idi	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \land k \in F [x]) \to B \in ℂ$
216	161 215	vtoclg	$⊢ F^{-1} [y] \in V \to ((((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land F^{-1} [y] \in (𝒫 C \cap Fin)) \land k \in F [F^{-1} [y]]) \to B \in ℂ)$
217	146 156 216	sylc	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \land k \in y) \to B \in ℂ$
218	97 105 3 106 121 145 217	fsumf1of	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \to \sum_{k \in y} B = \sum_{n \in F^{-1} [y]} D$
219		sumeq1	$⊢ x = F^{-1} [y] \to \sum_{n \in x} D = \sum_{n \in F^{-1} [y]} D$
220	219	rspceeqv	$⊢ (F^{-1} [y] \in (𝒫 C \cap Fin) \land \sum_{k \in y} B = \sum_{n \in F^{-1} [y]} D) \to \exists x \in (𝒫 C \cap Fin) \sum_{k \in y} B = \sum_{n \in x} D$
221	93 218 220	syl2anc	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land y \in (𝒫 A \cap Fin)) \to \exists x \in (𝒫 C \cap Fin) \sum_{k \in y} B = \sum_{n \in x} D$
222	71 221	rnmptssrn	$⊢ (φ \land \neg +∞ \in ran (n \in C ⟼ D)) \to ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) \subseteq ran (x \in (𝒫 C \cap Fin) ⟼ \sum_{n \in x} D)$
223		sumex	$⊢ \sum_{n \in x} D \in V$
224	223	a1i	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \to \sum_{n \in x} D \in V$
225	11 168	ssexd	$⊢ φ \to F [x] \in V$
226		elpwg	$⊢ F [x] \in V \to (F [x] \in 𝒫 A \leftrightarrow F [x] \subseteq A)$
227	225 226	syl	$⊢ φ \to (F [x] \in 𝒫 A \leftrightarrow F [x] \subseteq A)$
228	168 227	mpbird	$⊢ φ \to F [x] \in 𝒫 A$
229	228	adantr	$⊢ (φ \land x \in (𝒫 C \cap Fin)) \to F [x] \in 𝒫 A$
230	25	ffund	$⊢ φ \to Fun F$
231	230	adantr	$⊢ (φ \land x \in (𝒫 C \cap Fin)) \to Fun F$
232		elinel2	$⊢ x \in (𝒫 C \cap Fin) \to x \in Fin$
233	232	adantl	$⊢ (φ \land x \in (𝒫 C \cap Fin)) \to x \in Fin$
234		imafi	$⊢ (Fun F \land x \in Fin) \to F [x] \in Fin$
235	231 233 234	syl2anc	$⊢ (φ \land x \in (𝒫 C \cap Fin)) \to F [x] \in Fin$
236	229 235	elind	$⊢ (φ \land x \in (𝒫 C \cap Fin)) \to F [x] \in (𝒫 A \cap Fin)$
237	236	adantlr	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \to F [x] \in (𝒫 A \cap Fin)$
238		nfv	$⊢ Ⅎ k x \in (𝒫 C \cap Fin)$
239	95 238	nfan	$⊢ Ⅎ k ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin))$
240		nfv	$⊢ Ⅎ n x \in (𝒫 C \cap Fin)$
241	103 240	nfan	$⊢ Ⅎ n ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin))$
242	232	adantl	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \to x \in Fin$
243	108	adantr	$⊢ (φ \land x \in (𝒫 C \cap Fin)) \to F : C \underset{1-1}{⟶} A$
244		f1ores	$⊢ (F : C \underset{1-1}{⟶} A \land x \subseteq C) \to ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} F [x]$
245	243 139 244	syl2anc	$⊢ (φ \land x \in (𝒫 C \cap Fin)) \to ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} F [x]$
246	245	adantlr	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \to ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} F [x]$
247	142	adantllr	$⊢ (((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \land n \in x) \to ({F ↾}_{x}) (n) = G$
248	239 241 3 242 246 247 214	fsumf1of	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \to \sum_{k \in F [x]} B = \sum_{n \in x} D$
249	248	eqcomd	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \to \sum_{n \in x} D = \sum_{k \in F [x]} B$
250		sumeq1	$⊢ y = F [x] \to \sum_{k \in y} B = \sum_{k \in F [x]} B$
251	250	rspceeqv	$⊢ (F [x] \in (𝒫 A \cap Fin) \land \sum_{n \in x} D = \sum_{k \in F [x]} B) \to \exists y \in (𝒫 A \cap Fin) \sum_{n \in x} D = \sum_{k \in y} B$
252	237 249 251	syl2anc	$⊢ ((φ \land \neg +∞ \in ran (n \in C ⟼ D)) \land x \in (𝒫 C \cap Fin)) \to \exists y \in (𝒫 A \cap Fin) \sum_{n \in x} D = \sum_{k \in y} B$
253	224 252	rnmptssrn	$⊢ (φ \land \neg +∞ \in ran (n \in C ⟼ D)) \to ran (x \in (𝒫 C \cap Fin) ⟼ \sum_{n \in x} D) \subseteq ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B)$
254	222 253	eqssd	$⊢ (φ \land \neg +∞ \in ran (n \in C ⟼ D)) \to ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) = ran (x \in (𝒫 C \cap Fin) ⟼ \sum_{n \in x} D)$
255	254	supeq1d	$⊢ (φ \land \neg +∞ \in ran (n \in C ⟼ D)) \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) = sup (ran (x \in (𝒫 C \cap Fin) ⟼ \sum_{n \in x} D) ℝ^{} <)$
256	11	adantr	$⊢ (φ \land \neg +∞ \in ran (n \in C ⟼ D)) \to A \in V$
257	95 256 212	sge0revalmpt	$⊢ (φ \land \neg +∞ \in ran (n \in C ⟼ D)) \to sum^((k \in A ⟼ B)) = sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{*} <)$
258	4	adantr	$⊢ (φ \land \neg +∞ \in ran (n \in C ⟼ D)) \to C \in V$
259	103 258 206	sge0revalmpt	$⊢ (φ \land \neg +∞ \in ran (n \in C ⟼ D)) \to sum^((n \in C ⟼ D)) = sup (ran (x \in (𝒫 C \cap Fin) ⟼ \sum_{n \in x} D) ℝ^{*} <)$
260	255 257 259	3eqtr4d	$⊢ (φ \land \neg +∞ \in ran (n \in C ⟼ D)) \to sum^((k \in A ⟼ B)) = sum^((n \in C ⟼ D))$
261	69 260	pm2.61dan	$⊢ φ \to sum^((k \in A ⟼ B)) = sum^((n \in C ⟼ D))$

Metamath Proof Explorer

Theorem sge0f1o

Proof