Theorem sge0fodjrnlem 46407

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 7891	. . . . 5 ⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V))
5	2, 3, 4	sylc 65	. . . 4 ⊢ (𝜑 → 𝐴 ∈ V)
6		difssd 4088	. . . 4 ⊢ (𝜑 → (𝐴 ∖ {∅}) ⊆ 𝐴)
7		simpl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝜑)
8	6	sselda 3935	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝑘 ∈ 𝐴)
9		sge0fodjrnlem.b	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
10	7, 8, 9	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝐵 ∈ (0[,]+∞))
11		simpl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝜑)
12		dfin4 4229	. . . . . . . . . 10 ⊢ (𝐴 ∩ {∅}) = (𝐴 ∖ (𝐴 ∖ {∅}))
13	12	eqcomi 2738	. . . . . . . . 9 ⊢ (𝐴 ∖ (𝐴 ∖ {∅})) = (𝐴 ∩ {∅})
14		inss2 4189	. . . . . . . . 9 ⊢ (𝐴 ∩ {∅}) ⊆ {∅}
15	13, 14	eqsstri 3982	. . . . . . . 8 ⊢ (𝐴 ∖ (𝐴 ∖ {∅})) ⊆ {∅}
16		id 22	. . . . . . . 8 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})))
17	15, 16	sselid 3933	. . . . . . 7 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ {∅})
18		elsni 4594	. . . . . . 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 46403	. . 3 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) = (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)))
24	23	eqcomd 2735	. 2 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)))
25		sge0fodjrnlem.n	. . 3 ⊢ Ⅎ𝑛𝜑
26		sge0fodjrnlem.bd	. . 3 ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
27	2	difexd 5270	. . 3 ⊢ (𝜑 → (𝐶 ∖ 𝑍) ∈ V)
28		eqid 2729	. . . . 5 ⊢ (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
29		fof 6736	. . . . . . 7 ⊢ (𝐹:𝐶–onto→𝐴 → 𝐹:𝐶⟶𝐴)
30	3, 29	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐶⟶𝐴)
31	30	ffvelcdmda 7018	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴)
32		sge0fodjrnlem.dj	. . . . 5 ⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 (𝐹‘𝑛))
33		fveq2 6822	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
34	33	neeq1d 2984	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ≠ ∅ ↔ (𝐹‘𝑛) ≠ ∅))
35	34	cbvrabv 3405	. . . . 5 ⊢ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} = {𝑛 ∈ 𝐶 ∣ (𝐹‘𝑛) ≠ ∅}
36	33	cbvmptv 5196	. . . . . . 7 ⊢ (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
37	36	rneqi 5879	. . . . . 6 ⊢ ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
38	37	difeq1i 4073	. . . . 5 ⊢ (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}) = (ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ∖ {∅})
39	25, 28, 31, 32, 35, 38	disjf1o 45179	. . . 4 ⊢ (𝜑 → ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))
40	30	feqmptd 6891	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)))
41		difssd 4088	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 ∖ 𝑍) ⊆ 𝐶)
42	41	sselda 3935	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶)
43		eldifi 4082	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ 𝐶)
44	43	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝐶)
45		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) = ∅)
46		fvex 6835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑛) ∈ V
47	46	elsn 4592	. . . . . . . . . . . . . . . . . . . 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 6653	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 Fn 𝐶)
53		elpreima 6992	. . . . . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝑍)
59		eldifn 4083	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ¬ 𝑛 ∈ 𝑍)
60	59	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → ¬ 𝑛 ∈ 𝑍)
61	58, 60	pm2.65da 816	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ¬ (𝐹‘𝑛) = ∅)
62	61	neqned 2932	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) ≠ ∅)
63	42, 62	jca 511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅))
64	34	elrab 3648	. . . . . . . . . . 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 2820	. . . . . . . . . . . . . . . . . . . . 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 4594	. . . . . . . . . . . . . . . . 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 2930	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → ¬ (𝐹‘𝑛) = ∅)
81	77, 80	pm2.65da 816	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → ¬ 𝑛 ∈ 𝑍)
82	68, 81	eldifd 3914	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ (𝐶 ∖ 𝑍))
83	82	ex 412	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍)))
84	25, 83	ralrimi 3227	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍))
85		dfss3 3924	. . . . . . . . . . 11 ⊢ ({𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍) ↔ ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍))
86	84, 85	sylibr 234	. . . . . . . . . 10 ⊢ (𝜑 → {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍))
87	86	sseld 3934	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍)))
88	66, 87	impbid 212	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
89	25, 88	alrimi 2214	. . . . . . 7 ⊢ (𝜑 → ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
90		dfcleq 2722	. . . . . . 7 ⊢ ((𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
91	89, 90	sylibr 234	. . . . . 6 ⊢ (𝜑 → (𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})
92	40, 91	reseq12d 5931	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)) = ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
93	40, 36	eqtr4di 2782	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)))
94	93	eqcomd 2735	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = 𝐹)
95	94	rneqd 5880	. . . . . . 7 ⊢ (𝜑 → ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran 𝐹)
96		forn 6739	. . . . . . . 8 ⊢ (𝐹:𝐶–onto→𝐴 → ran 𝐹 = 𝐴)
97	3, 96	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 = 𝐴)
98	95, 97	eqtr2d 2765	. . . . . 6 ⊢ (𝜑 → 𝐴 = ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)))
99	98	difeq1d 4076	. . . . 5 ⊢ (𝜑 → (𝐴 ∖ {∅}) = (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))
100	92, 91, 99	f1oeq123d 6758	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}) ↔ ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅})))
101	39, 100	mpbird 257	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}))
102		fvres 6841	. . . . 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 2764	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = 𝐺)
108	1, 25, 26, 27, 101, 107, 10	sge0f1o 46373	. 2 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) = (Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)))
109	105	eqcomd 2735	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 = (𝐹‘𝑛))
110	109, 31	eqeltrd 2828	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 ∈ 𝐴)
111	104, 42, 110	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐺 ∈ 𝐴)
112	111	ex 412	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝐺 ∈ 𝐴))
113	112	imdistani 568	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝜑 ∧ 𝐺 ∈ 𝐴))
114		nfcv 2891	. . . . 5 ⊢ Ⅎ𝑘𝐺
115		nfv 1914	. . . . . . 7 ⊢ Ⅎ𝑘 𝐺 ∈ 𝐴
116	1, 115	nfan 1899	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝐺 ∈ 𝐴)
117		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑘 𝐷 ∈ (0[,]+∞)
118	116, 117	nfim 1896	. . . . 5 ⊢ Ⅎ𝑘((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))
119		eleq1 2816	. . . . . . 7 ⊢ (𝑘 = 𝐺 → (𝑘 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴))
120	119	anbi2d 630	. . . . . 6 ⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝐺 ∈ 𝐴)))
121	26	eleq1d 2813	. . . . . 6 ⊢ (𝑘 = 𝐺 → (𝐵 ∈ (0[,]+∞) ↔ 𝐷 ∈ (0[,]+∞)))
122	120, 121	imbi12d 344	. . . . 5 ⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))))
123	114, 118, 122, 9	vtoclgf 3524	. . . 4 ⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞)))
124	111, 113, 123	sylc 65	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐷 ∈ (0[,]+∞))
125		simpl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝜑)
126		eldifi 4082	. . . . . 6 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶)
127	126	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝐶)
128	125, 127, 110	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 ∈ 𝐴)
129		dfin4 4229	. . . . . . . . 9 ⊢ (𝑍 ∩ 𝐶) = (𝑍 ∖ (𝑍 ∖ 𝐶))
130		difss 4087	. . . . . . . . 9 ⊢ (𝑍 ∖ (𝑍 ∖ 𝐶)) ⊆ 𝑍
131	129, 130	eqsstri 3982	. . . . . . . 8 ⊢ (𝑍 ∩ 𝐶) ⊆ 𝑍
132		inss2 4189	. . . . . . . . . 10 ⊢ (𝐶 ∩ 𝑍) ⊆ 𝑍
133		id 22	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)))
134		dfin4 4229	. . . . . . . . . . . 12 ⊢ (𝐶 ∩ 𝑍) = (𝐶 ∖ (𝐶 ∖ 𝑍))
135	134	eqcomi 2738	. . . . . . . . . . 11 ⊢ (𝐶 ∖ (𝐶 ∖ 𝑍)) = (𝐶 ∩ 𝑍)
136	133, 135	eleqtrdi 2838	. . . . . . . . . 10 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∩ 𝑍))
137	132, 136	sselid 3933	. . . . . . . . 9 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍)
138	137, 126	elind 4151	. . . . . . . 8 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝑍 ∩ 𝐶))
139	131, 138	sselid 3933	. . . . . . 7 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍)
140	139	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝑍)
141	76	eqcomd 2735	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∅ = (𝐹‘𝑛))
142		simpl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝜑)
143	73	simpld 494	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝐶)
144	142, 143, 105	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = 𝐺)
145	141, 144	eqtr2d 2765	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐺 = ∅)
146	125, 140, 145	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 = ∅)
147	125, 146	jca 511	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → (𝜑 ∧ 𝐺 = ∅))
148		nfv 1914	. . . . . . 7 ⊢ Ⅎ𝑘 𝐺 = ∅
149	1, 148	nfan 1899	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝐺 = ∅)
150		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑘 𝐷 = 0
151	149, 150	nfim 1896	. . . . 5 ⊢ Ⅎ𝑘((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0)
152		eqeq1 2733	. . . . . . 7 ⊢ (𝑘 = 𝐺 → (𝑘 = ∅ ↔ 𝐺 = ∅))
153	152	anbi2d 630	. . . . . 6 ⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 = ∅) ↔ (𝜑 ∧ 𝐺 = ∅)))
154	26	eqeq1d 2731	. . . . . 6 ⊢ (𝑘 = 𝐺 → (𝐵 = 0 ↔ 𝐷 = 0))
155	153, 154	imbi12d 344	. . . . 5 ⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) ↔ ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0)))
156	114, 151, 155, 21	vtoclgf 3524	. . . 4 ⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0))
157	128, 147, 156	sylc 65	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐷 = 0)
158	25, 2, 41, 124, 157	sge0ss 46403	. 2 ⊢ (𝜑 → (Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
159	24, 108, 158	3eqtrd 2768	1 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  Ⅎwnf 1783   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  {crab 3394  Vcvv 3436   ∖ cdif 3900   ∩ cin 3902   ⊆ wss 3903  ∅c0 4284  {csn 4577  Disj wdisj 5059   ↦ cmpt 5173  ^◡ccnv 5618  ran crn 5620   ↾ cres 5621   “ cima 5622   Fn wfn 6477  ⟶wf 6478  –onto→wfo 6480  –1-1-onto→wf1o 6481  ‘cfv 6482  (class class class)co 7349  0cc0 11009  +∞cpnf 11146  [,]cicc 13251  Σ^{^}csumge0 46353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-inf2 9537  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-int 4897  df-iun 4943  df-disj 5060  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-isom 6491  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-sup 9332  df-oi 9402  df-card 9835  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-div 11778  df-nn 12129  df-2 12191  df-3 12192  df-n0 12385  df-z 12472  df-uz 12736  df-rp 12894  df-xadd 13015  df-ico 13254  df-icc 13255  df-fz 13411  df-fzo 13558  df-seq 13909  df-exp 13969  df-hash 14238  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-clim 15395  df-sum 15594  df-sumge0 46354

This theorem is referenced by:  sge0fodjrn  46408