Theorem sge0fodjrnlem 45132

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.)

Hypotheses

Ref	Expression
sge0fodjrnlem.k	⊢ Ⅎ𝑘𝜑
sge0fodjrnlem.n	⊢ Ⅎ𝑛𝜑
sge0fodjrnlem.bd	⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
sge0fodjrnlem.c	⊢ (𝜑 → 𝐶 ∈ 𝑉)
sge0fodjrnlem.f	⊢ (𝜑 → 𝐹:𝐶–onto→𝐴)
sge0fodjrnlem.dj	⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 (𝐹‘𝑛))
sge0fodjrnlem.fng	⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)
sge0fodjrnlem.b	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
sge0fodjrnlem.b0	⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0)
sge0fodjrnlem.z	⊢ 𝑍 = (◡𝐹 “ {∅})

Assertion

Ref	Expression
sge0fodjrnlem	⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Distinct variable groups:   𝐴,𝑘,𝑛   𝐵,𝑛   𝐶,𝑘,𝑛   𝐷,𝑘   𝑘,𝐹,𝑛   𝑘,𝐺   𝑘,𝑍,𝑛

Allowed substitution hints:   𝜑(𝑘,𝑛)   𝐵(𝑘)   𝐷(𝑛)   𝐺(𝑛)   𝑉(𝑘,𝑛)

Proof of Theorem sge0fodjrnlem

Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sge0fodjrnlem.k	. . . 4 ⊢ Ⅎ𝑘𝜑
2		sge0fodjrnlem.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
3		sge0fodjrnlem.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝐶–onto→𝐴)
4		focdmex 7942	. . . . 5 ⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V))
5	2, 3, 4	sylc 65	. . . 4 ⊢ (𝜑 → 𝐴 ∈ V)
6		difssd 4133	. . . 4 ⊢ (𝜑 → (𝐴 ∖ {∅}) ⊆ 𝐴)
7		simpl 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝜑)
8	6	sselda 3983	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝑘 ∈ 𝐴)
9		sge0fodjrnlem.b	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
10	7, 8, 9	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝐵 ∈ (0[,]+∞))
11		simpl 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝜑)
12		dfin4 4268	. . . . . . . . . 10 ⊢ (𝐴 ∩ {∅}) = (𝐴 ∖ (𝐴 ∖ {∅}))
13	12	eqcomi 2742	. . . . . . . . 9 ⊢ (𝐴 ∖ (𝐴 ∖ {∅})) = (𝐴 ∩ {∅})
14		inss2 4230	. . . . . . . . 9 ⊢ (𝐴 ∩ {∅}) ⊆ {∅}
15	13, 14	eqsstri 4017	. . . . . . . 8 ⊢ (𝐴 ∖ (𝐴 ∖ {∅})) ⊆ {∅}
16		id 22	. . . . . . . 8 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})))
17	15, 16	sselid 3981	. . . . . . 7 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ {∅})
18		elsni 4646	. . . . . . 7 ⊢ (𝑘 ∈ {∅} → 𝑘 = ∅)
19	17, 18	syl 17	. . . . . 6 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 = ∅)
20	19	adantl 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝑘 = ∅)
21		sge0fodjrnlem.b0	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0)
22	11, 20, 21	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝐵 = 0)
23	1, 5, 6, 10, 22	sge0ss 45128	. . 3 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) = (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)))
24	23	eqcomd 2739	. 2 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)))
25		sge0fodjrnlem.n	. . 3 ⊢ Ⅎ𝑛𝜑
26		sge0fodjrnlem.bd	. . 3 ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
27	2	difexd 5330	. . 3 ⊢ (𝜑 → (𝐶 ∖ 𝑍) ∈ V)
28		eqid 2733	. . . . 5 ⊢ (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
29		fof 6806	. . . . . . 7 ⊢ (𝐹:𝐶–onto→𝐴 → 𝐹:𝐶⟶𝐴)
30	3, 29	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐶⟶𝐴)
31	30	ffvelcdmda 7087	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴)
32		sge0fodjrnlem.dj	. . . . 5 ⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 (𝐹‘𝑛))
33		fveq2 6892	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
34	33	neeq1d 3001	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ≠ ∅ ↔ (𝐹‘𝑛) ≠ ∅))
35	34	cbvrabv 3443	. . . . 5 ⊢ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} = {𝑛 ∈ 𝐶 ∣ (𝐹‘𝑛) ≠ ∅}
36	33	cbvmptv 5262	. . . . . . 7 ⊢ (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
37	36	rneqi 5937	. . . . . 6 ⊢ ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
38	37	difeq1i 4119	. . . . 5 ⊢ (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}) = (ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ∖ {∅})
39	25, 28, 31, 32, 35, 38	disjf1o 43889	. . . 4 ⊢ (𝜑 → ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))
40	30	feqmptd 6961	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)))
41		difssd 4133	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 ∖ 𝑍) ⊆ 𝐶)
42	41	sselda 3983	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶)
43		eldifi 4127	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ 𝐶)
44	43	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝐶)
45		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) = ∅)
46		fvex 6905	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑛) ∈ V
47	46	elsn 4644	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑛) ∈ {∅} ↔ (𝐹‘𝑛) = ∅)
48	45, 47	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ∈ {∅})
49	48	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → (𝐹‘𝑛) ∈ {∅})
50	44, 49	jca 513	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))
51	50	adantll 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))
52	30	ffnd 6719	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 Fn 𝐶)
53		elpreima 7060	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn 𝐶 → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})))
54	52, 53	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})))
55	54	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})))
56	51, 55	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ (◡𝐹 “ {∅}))
57		sge0fodjrnlem.z	. . . . . . . . . . . . . . 15 ⊢ 𝑍 = (◡𝐹 “ {∅})
58	56, 57	eleqtrrdi 2845	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝑍)
59		eldifn 4128	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ¬ 𝑛 ∈ 𝑍)
60	59	ad2antlr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → ¬ 𝑛 ∈ 𝑍)
61	58, 60	pm2.65da 816	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ¬ (𝐹‘𝑛) = ∅)
62	61	neqned 2948	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) ≠ ∅)
63	42, 62	jca 513	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅))
64	34	elrab 3684	. . . . . . . . . . 11 ⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅))
65	63, 64	sylibr 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})
66	65	ex 414	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
67	64	simplbi 499	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ 𝐶)
68	67	adantl 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ 𝐶)
69	57	eleq2i 2826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (◡𝐹 “ {∅}))
70	69	biimpi 215	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (◡𝐹 “ {∅}))
71	70	adantl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (◡𝐹 “ {∅}))
72	54	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})))
73	71, 72	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))
74	73	simprd 497	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ {∅})
75		elsni 4646	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑛) ∈ {∅} → (𝐹‘𝑛) = ∅)
76	74, 75	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ∅)
77	76	adantlr 714	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ∅)
78	64	simprbi 498	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → (𝐹‘𝑛) ≠ ∅)
79	78	ad2antlr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ≠ ∅)
80	79	neneqd 2946	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → ¬ (𝐹‘𝑛) = ∅)
81	77, 80	pm2.65da 816	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → ¬ 𝑛 ∈ 𝑍)
82	68, 81	eldifd 3960	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ (𝐶 ∖ 𝑍))
83	82	ex 414	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍)))
84	25, 83	ralrimi 3255	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍))
85		dfss3 3971	. . . . . . . . . . 11 ⊢ ({𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍) ↔ ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍))
86	84, 85	sylibr 233	. . . . . . . . . 10 ⊢ (𝜑 → {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍))
87	86	sseld 3982	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍)))
88	66, 87	impbid 211	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
89	25, 88	alrimi 2207	. . . . . . 7 ⊢ (𝜑 → ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
90		dfcleq 2726	. . . . . . 7 ⊢ ((𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
91	89, 90	sylibr 233	. . . . . 6 ⊢ (𝜑 → (𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})
92	40, 91	reseq12d 5983	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)) = ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
93	40, 36	eqtr4di 2791	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)))
94	93	eqcomd 2739	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = 𝐹)
95	94	rneqd 5938	. . . . . . 7 ⊢ (𝜑 → ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran 𝐹)
96		forn 6809	. . . . . . . 8 ⊢ (𝐹:𝐶–onto→𝐴 → ran 𝐹 = 𝐴)
97	3, 96	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 = 𝐴)
98	95, 97	eqtr2d 2774	. . . . . 6 ⊢ (𝜑 → 𝐴 = ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)))
99	98	difeq1d 4122	. . . . 5 ⊢ (𝜑 → (𝐴 ∖ {∅}) = (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))
100	92, 91, 99	f1oeq123d 6828	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}) ↔ ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅})))
101	39, 100	mpbird 257	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}))
102		fvres 6911	. . . . 5 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = (𝐹‘𝑛))
103	102	adantl 483	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = (𝐹‘𝑛))
104		simpl 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝜑)
105		sge0fodjrnlem.fng	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)
106	104, 42, 105	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) = 𝐺)
107	103, 106	eqtrd 2773	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = 𝐺)
108	1, 25, 26, 27, 101, 107, 10	sge0f1o 45098	. 2 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) = (Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)))
109	105	eqcomd 2739	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 = (𝐹‘𝑛))
110	109, 31	eqeltrd 2834	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 ∈ 𝐴)
111	104, 42, 110	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐺 ∈ 𝐴)
112	111	ex 414	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝐺 ∈ 𝐴))
113	112	imdistani 570	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝜑 ∧ 𝐺 ∈ 𝐴))
114		nfcv 2904	. . . . 5 ⊢ Ⅎ𝑘𝐺
115		nfv 1918	. . . . . . 7 ⊢ Ⅎ𝑘 𝐺 ∈ 𝐴
116	1, 115	nfan 1903	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝐺 ∈ 𝐴)
117		nfv 1918	. . . . . 6 ⊢ Ⅎ𝑘 𝐷 ∈ (0[,]+∞)
118	116, 117	nfim 1900	. . . . 5 ⊢ Ⅎ𝑘((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))
119		eleq1 2822	. . . . . . 7 ⊢ (𝑘 = 𝐺 → (𝑘 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴))
120	119	anbi2d 630	. . . . . 6 ⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝐺 ∈ 𝐴)))
121	26	eleq1d 2819	. . . . . 6 ⊢ (𝑘 = 𝐺 → (𝐵 ∈ (0[,]+∞) ↔ 𝐷 ∈ (0[,]+∞)))
122	120, 121	imbi12d 345	. . . . 5 ⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))))
123	114, 118, 122, 9	vtoclgf 3555	. . . 4 ⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞)))
124	111, 113, 123	sylc 65	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐷 ∈ (0[,]+∞))
125		simpl 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝜑)
126		eldifi 4127	. . . . . 6 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶)
127	126	adantl 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝐶)
128	125, 127, 110	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 ∈ 𝐴)
129		dfin4 4268	. . . . . . . . 9 ⊢ (𝑍 ∩ 𝐶) = (𝑍 ∖ (𝑍 ∖ 𝐶))
130		difss 4132	. . . . . . . . 9 ⊢ (𝑍 ∖ (𝑍 ∖ 𝐶)) ⊆ 𝑍
131	129, 130	eqsstri 4017	. . . . . . . 8 ⊢ (𝑍 ∩ 𝐶) ⊆ 𝑍
132		inss2 4230	. . . . . . . . . 10 ⊢ (𝐶 ∩ 𝑍) ⊆ 𝑍
133		id 22	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)))
134		dfin4 4268	. . . . . . . . . . . 12 ⊢ (𝐶 ∩ 𝑍) = (𝐶 ∖ (𝐶 ∖ 𝑍))
135	134	eqcomi 2742	. . . . . . . . . . 11 ⊢ (𝐶 ∖ (𝐶 ∖ 𝑍)) = (𝐶 ∩ 𝑍)
136	133, 135	eleqtrdi 2844	. . . . . . . . . 10 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∩ 𝑍))
137	132, 136	sselid 3981	. . . . . . . . 9 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍)
138	137, 126	elind 4195	. . . . . . . 8 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝑍 ∩ 𝐶))
139	131, 138	sselid 3981	. . . . . . 7 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍)
140	139	adantl 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝑍)
141	76	eqcomd 2739	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∅ = (𝐹‘𝑛))
142		simpl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝜑)
143	73	simpld 496	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝐶)
144	142, 143, 105	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = 𝐺)
145	141, 144	eqtr2d 2774	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐺 = ∅)
146	125, 140, 145	syl2anc 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 = ∅)
147	125, 146	jca 513	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → (𝜑 ∧ 𝐺 = ∅))
148		nfv 1918	. . . . . . 7 ⊢ Ⅎ𝑘 𝐺 = ∅
149	1, 148	nfan 1903	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝐺 = ∅)
150		nfv 1918	. . . . . 6 ⊢ Ⅎ𝑘 𝐷 = 0
151	149, 150	nfim 1900	. . . . 5 ⊢ Ⅎ𝑘((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0)
152		eqeq1 2737	. . . . . . 7 ⊢ (𝑘 = 𝐺 → (𝑘 = ∅ ↔ 𝐺 = ∅))
153	152	anbi2d 630	. . . . . 6 ⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 = ∅) ↔ (𝜑 ∧ 𝐺 = ∅)))
154	26	eqeq1d 2735	. . . . . 6 ⊢ (𝑘 = 𝐺 → (𝐵 = 0 ↔ 𝐷 = 0))
155	153, 154	imbi12d 345	. . . . 5 ⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) ↔ ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0)))
156	114, 151, 155, 21	vtoclgf 3555	. . . 4 ⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0))
157	128, 147, 156	sylc 65	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐷 = 0)
158	25, 2, 41, 124, 157	sge0ss 45128	. 2 ⊢ (𝜑 → (Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
159	24, 108, 158	3eqtrd 2777	1 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540   = wceq 1542  Ⅎwnf 1786   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  {crab 3433  Vcvv 3475   ∖ cdif 3946   ∩ cin 3948   ⊆ wss 3949  ∅c0 4323  {csn 4629  Disj wdisj 5114   ↦ cmpt 5232  ^◡ccnv 5676  ran crn 5678   ↾ cres 5679   “ cima 5680   Fn wfn 6539  ⟶wf 6540  –onto→wfo 6542  –1-1-onto→wf1o 6543  ‘cfv 6544  (class class class)co 7409  0cc0 11110  +∞cpnf 11245  [,]cicc 13327  Σ^{^}csumge0 45078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-xadd 13093  df-ico 13330  df-icc 13331  df-fz 13485  df-fzo 13628  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-clim 15432  df-sum 15633  df-sumge0 45079

This theorem is referenced by:  sge0fodjrn  45133