Theorem sge0fodjrnlem 46602

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 7898	. . . . 5 ⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V))
5	2, 3, 4	sylc 65	. . . 4 ⊢ (𝜑 → 𝐴 ∈ V)
6		difssd 4087	. . . 4 ⊢ (𝜑 → (𝐴 ∖ {∅}) ⊆ 𝐴)
7		simpl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝜑)
8	6	sselda 3931	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝑘 ∈ 𝐴)
9		sge0fodjrnlem.b	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
10	7, 8, 9	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝐵 ∈ (0[,]+∞))
11		simpl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝜑)
12		dfin4 4228	. . . . . . . . . 10 ⊢ (𝐴 ∩ {∅}) = (𝐴 ∖ (𝐴 ∖ {∅}))
13	12	eqcomi 2743	. . . . . . . . 9 ⊢ (𝐴 ∖ (𝐴 ∖ {∅})) = (𝐴 ∩ {∅})
14		inss2 4188	. . . . . . . . 9 ⊢ (𝐴 ∩ {∅}) ⊆ {∅}
15	13, 14	eqsstri 3978	. . . . . . . 8 ⊢ (𝐴 ∖ (𝐴 ∖ {∅})) ⊆ {∅}
16		id 22	. . . . . . . 8 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})))
17	15, 16	sselid 3929	. . . . . . 7 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ {∅})
18		elsni 4595	. . . . . . 7 ⊢ (𝑘 ∈ {∅} → 𝑘 = ∅)
19	17, 18	syl 17	. . . . . 6 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 = ∅)
20	19	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝑘 = ∅)
21		sge0fodjrnlem.b0	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0)
22	11, 20, 21	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝐵 = 0)
23	1, 5, 6, 10, 22	sge0ss 46598	. . 3 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) = (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)))
24	23	eqcomd 2740	. 2 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)))
25		sge0fodjrnlem.n	. . 3 ⊢ Ⅎ𝑛𝜑
26		sge0fodjrnlem.bd	. . 3 ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
27	2	difexd 5274	. . 3 ⊢ (𝜑 → (𝐶 ∖ 𝑍) ∈ V)
28		eqid 2734	. . . . 5 ⊢ (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
29		fof 6744	. . . . . . 7 ⊢ (𝐹:𝐶–onto→𝐴 → 𝐹:𝐶⟶𝐴)
30	3, 29	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐶⟶𝐴)
31	30	ffvelcdmda 7027	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴)
32		sge0fodjrnlem.dj	. . . . 5 ⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 (𝐹‘𝑛))
33		fveq2 6832	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
34	33	neeq1d 2989	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ≠ ∅ ↔ (𝐹‘𝑛) ≠ ∅))
35	34	cbvrabv 3407	. . . . 5 ⊢ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} = {𝑛 ∈ 𝐶 ∣ (𝐹‘𝑛) ≠ ∅}
36	33	cbvmptv 5200	. . . . . . 7 ⊢ (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
37	36	rneqi 5884	. . . . . 6 ⊢ ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
38	37	difeq1i 4072	. . . . 5 ⊢ (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}) = (ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ∖ {∅})
39	25, 28, 31, 32, 35, 38	disjf1o 45377	. . . 4 ⊢ (𝜑 → ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))
40	30	feqmptd 6900	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)))
41		difssd 4087	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 ∖ 𝑍) ⊆ 𝐶)
42	41	sselda 3931	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶)
43		eldifi 4081	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ 𝐶)
44	43	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝐶)
45		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) = ∅)
46		fvex 6845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑛) ∈ V
47	46	elsn 4593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑛) ∈ {∅} ↔ (𝐹‘𝑛) = ∅)
48	45, 47	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ∈ {∅})
49	48	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → (𝐹‘𝑛) ∈ {∅})
50	44, 49	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))
51	50	adantll 714	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))
52	30	ffnd 6661	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 Fn 𝐶)
53		elpreima 7001	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn 𝐶 → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})))
54	52, 53	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})))
55	54	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})))
56	51, 55	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ (◡𝐹 “ {∅}))
57		sge0fodjrnlem.z	. . . . . . . . . . . . . . 15 ⊢ 𝑍 = (◡𝐹 “ {∅})
58	56, 57	eleqtrrdi 2845	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝑍)
59		eldifn 4082	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ¬ 𝑛 ∈ 𝑍)
60	59	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → ¬ 𝑛 ∈ 𝑍)
61	58, 60	pm2.65da 816	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ¬ (𝐹‘𝑛) = ∅)
62	61	neqned 2937	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) ≠ ∅)
63	42, 62	jca 511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅))
64	34	elrab 3644	. . . . . . . . . . 11 ⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅))
65	63, 64	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})
66	65	ex 412	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
67	64	simplbi 497	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ 𝐶)
68	67	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ 𝐶)
69	57	eleq2i 2826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (◡𝐹 “ {∅}))
70	69	biimpi 216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (◡𝐹 “ {∅}))
71	70	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (◡𝐹 “ {∅}))
72	54	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})))
73	71, 72	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))
74	73	simprd 495	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ {∅})
75		elsni 4595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑛) ∈ {∅} → (𝐹‘𝑛) = ∅)
76	74, 75	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ∅)
77	76	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ∅)
78	64	simprbi 496	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → (𝐹‘𝑛) ≠ ∅)
79	78	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ≠ ∅)
80	79	neneqd 2935	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → ¬ (𝐹‘𝑛) = ∅)
81	77, 80	pm2.65da 816	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → ¬ 𝑛 ∈ 𝑍)
82	68, 81	eldifd 3910	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ (𝐶 ∖ 𝑍))
83	82	ex 412	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍)))
84	25, 83	ralrimi 3232	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍))
85		dfss3 3920	. . . . . . . . . . 11 ⊢ ({𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍) ↔ ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍))
86	84, 85	sylibr 234	. . . . . . . . . 10 ⊢ (𝜑 → {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍))
87	86	sseld 3930	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍)))
88	66, 87	impbid 212	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
89	25, 88	alrimi 2218	. . . . . . 7 ⊢ (𝜑 → ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
90		dfcleq 2727	. . . . . . 7 ⊢ ((𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
91	89, 90	sylibr 234	. . . . . 6 ⊢ (𝜑 → (𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})
92	40, 91	reseq12d 5937	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)) = ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
93	40, 36	eqtr4di 2787	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)))
94	93	eqcomd 2740	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = 𝐹)
95	94	rneqd 5885	. . . . . . 7 ⊢ (𝜑 → ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran 𝐹)
96		forn 6747	. . . . . . . 8 ⊢ (𝐹:𝐶–onto→𝐴 → ran 𝐹 = 𝐴)
97	3, 96	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 = 𝐴)
98	95, 97	eqtr2d 2770	. . . . . 6 ⊢ (𝜑 → 𝐴 = ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)))
99	98	difeq1d 4075	. . . . 5 ⊢ (𝜑 → (𝐴 ∖ {∅}) = (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))
100	92, 91, 99	f1oeq123d 6766	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}) ↔ ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅})))
101	39, 100	mpbird 257	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}))
102		fvres 6851	. . . . 5 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = (𝐹‘𝑛))
103	102	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = (𝐹‘𝑛))
104		simpl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝜑)
105		sge0fodjrnlem.fng	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)
106	104, 42, 105	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) = 𝐺)
107	103, 106	eqtrd 2769	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = 𝐺)
108	1, 25, 26, 27, 101, 107, 10	sge0f1o 46568	. 2 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) = (Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)))
109	105	eqcomd 2740	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 = (𝐹‘𝑛))
110	109, 31	eqeltrd 2834	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 ∈ 𝐴)
111	104, 42, 110	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐺 ∈ 𝐴)
112	111	ex 412	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝐺 ∈ 𝐴))
113	112	imdistani 568	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝜑 ∧ 𝐺 ∈ 𝐴))
114		nfcv 2896	. . . . 5 ⊢ Ⅎ𝑘𝐺
115		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑘 𝐺 ∈ 𝐴
116	1, 115	nfan 1900	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝐺 ∈ 𝐴)
117		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑘 𝐷 ∈ (0[,]+∞)
118	116, 117	nfim 1897	. . . . 5 ⊢ Ⅎ𝑘((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))
119		eleq1 2822	. . . . . . 7 ⊢ (𝑘 = 𝐺 → (𝑘 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴))
120	119	anbi2d 630	. . . . . 6 ⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝐺 ∈ 𝐴)))
121	26	eleq1d 2819	. . . . . 6 ⊢ (𝑘 = 𝐺 → (𝐵 ∈ (0[,]+∞) ↔ 𝐷 ∈ (0[,]+∞)))
122	120, 121	imbi12d 344	. . . . 5 ⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))))
123	114, 118, 122, 9	vtoclgf 3523	. . . 4 ⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞)))
124	111, 113, 123	sylc 65	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐷 ∈ (0[,]+∞))
125		simpl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝜑)
126		eldifi 4081	. . . . . 6 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶)
127	126	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝐶)
128	125, 127, 110	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 ∈ 𝐴)
129		dfin4 4228	. . . . . . . . 9 ⊢ (𝑍 ∩ 𝐶) = (𝑍 ∖ (𝑍 ∖ 𝐶))
130		difss 4086	. . . . . . . . 9 ⊢ (𝑍 ∖ (𝑍 ∖ 𝐶)) ⊆ 𝑍
131	129, 130	eqsstri 3978	. . . . . . . 8 ⊢ (𝑍 ∩ 𝐶) ⊆ 𝑍
132		inss2 4188	. . . . . . . . . 10 ⊢ (𝐶 ∩ 𝑍) ⊆ 𝑍
133		id 22	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)))
134		dfin4 4228	. . . . . . . . . . . 12 ⊢ (𝐶 ∩ 𝑍) = (𝐶 ∖ (𝐶 ∖ 𝑍))
135	134	eqcomi 2743	. . . . . . . . . . 11 ⊢ (𝐶 ∖ (𝐶 ∖ 𝑍)) = (𝐶 ∩ 𝑍)
136	133, 135	eleqtrdi 2844	. . . . . . . . . 10 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∩ 𝑍))
137	132, 136	sselid 3929	. . . . . . . . 9 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍)
138	137, 126	elind 4150	. . . . . . . 8 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝑍 ∩ 𝐶))
139	131, 138	sselid 3929	. . . . . . 7 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍)
140	139	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝑍)
141	76	eqcomd 2740	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∅ = (𝐹‘𝑛))
142		simpl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝜑)
143	73	simpld 494	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝐶)
144	142, 143, 105	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = 𝐺)
145	141, 144	eqtr2d 2770	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐺 = ∅)
146	125, 140, 145	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 = ∅)
147	125, 146	jca 511	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → (𝜑 ∧ 𝐺 = ∅))
148		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑘 𝐺 = ∅
149	1, 148	nfan 1900	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝐺 = ∅)
150		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑘 𝐷 = 0
151	149, 150	nfim 1897	. . . . 5 ⊢ Ⅎ𝑘((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0)
152		eqeq1 2738	. . . . . . 7 ⊢ (𝑘 = 𝐺 → (𝑘 = ∅ ↔ 𝐺 = ∅))
153	152	anbi2d 630	. . . . . 6 ⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 = ∅) ↔ (𝜑 ∧ 𝐺 = ∅)))
154	26	eqeq1d 2736	. . . . . 6 ⊢ (𝑘 = 𝐺 → (𝐵 = 0 ↔ 𝐷 = 0))
155	153, 154	imbi12d 344	. . . . 5 ⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) ↔ ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0)))
156	114, 151, 155, 21	vtoclgf 3523	. . . 4 ⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0))
157	128, 147, 156	sylc 65	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐷 = 0)
158	25, 2, 41, 124, 157	sge0ss 46598	. 2 ⊢ (𝜑 → (Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
159	24, 108, 158	3eqtrd 2773	1 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  Ⅎwnf 1784   ∈ wcel 2113   ≠ wne 2930  ∀wral 3049  {crab 3397  Vcvv 3438   ∖ cdif 3896   ∩ cin 3898   ⊆ wss 3899  ∅c0 4283  {csn 4578  Disj wdisj 5063   ↦ cmpt 5177  ^◡ccnv 5621  ran crn 5623   ↾ cres 5624   “ cima 5625   Fn wfn 6485  ⟶wf 6486  –onto→wfo 6488  –1-1-onto→wf1o 6489  ‘cfv 6490  (class class class)co 7356  0cc0 11024  +∞cpnf 11161  [,]cicc 13262  Σ^{^}csumge0 46548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-inf2 9548  ax-cnex 11080  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101  ax-pre-sup 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-int 4901  df-iun 4946  df-disj 5064  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-se 5576  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-isom 6499  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-fin 8885  df-sup 9343  df-oi 9413  df-card 9849  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-div 11793  df-nn 12144  df-2 12206  df-3 12207  df-n0 12400  df-z 12487  df-uz 12750  df-rp 12904  df-xadd 13025  df-ico 13265  df-icc 13266  df-fz 13422  df-fzo 13569  df-seq 13923  df-exp 13983  df-hash 14252  df-cj 15020  df-re 15021  df-im 15022  df-sqrt 15156  df-abs 15157  df-clim 15409  df-sum 15608  df-sumge0 46549

This theorem is referenced by:  sge0fodjrn  46603