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

Metamath Proof Explorer

Theorem sge0f1o

Proof