Theorem sge0iun

Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0iun.a	$$⊢\phi \to A\in V$$
	sge0iun.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in W$$
	sge0iun.x	$$⊢X=\bigcup _{x\in A}B$$
	sge0iun.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
	sge0iun.dj	$$⊢\phi \to \underset{x\in A}{Disj}B$$
Assertion	sge0iun	$$⊢\phi \to \mathrm{sum^}\left(F\right)=\mathrm{sum^}\left(\left(x\in A⟼\mathrm{sum^}\left({F\upharpoonright }_B\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sge0iun.a	$$⊢\phi \to A\in V$$
2		sge0iun.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in W$$
3		sge0iun.x	$$⊢X=\bigcup _{x\in A}B$$
4		sge0iun.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
5		sge0iun.dj	$$⊢\phi \to \underset{x\in A}{Disj}B$$
6	4	adantr	$$⊢\left(\phi \wedge x\in A\right)\to F:X⟶\left[0,\mathrm{+\infty }\right]$$
7	6	3adant3	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to F:X⟶\left[0,\mathrm{+\infty }\right]$$
8		ssiun2	$$⊢x\in A\to B\subseteq \bigcup _{x\in A}B$$
9	8	adantl	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq \bigcup _{x\in A}B$$
10	3	eqcomi	$$⊢\bigcup _{x\in A}B=X$$
11	9 10	sseqtrdi	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq X$$
12	11	3adant3	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to B\subseteq X$$
13		simp3	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to y\in B$$
14	12 13	sseldd	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to y\in X$$
15	7 14	ffvelcdmd	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to F\left(y\right)\in \left[0,\mathrm{+\infty }\right]$$
16	1 2 5 15	sge0iunmpt	$$⊢\phi \to \mathrm{sum^}\left(\left(y\in \bigcup _{x\in A}B⟼F\left(y\right)\right)\right)=\mathrm{sum^}\left(\left(x\in A⟼\mathrm{sum^}\left(\left(y\in B⟼F\left(y\right)\right)\right)\right)\right)$$
17	3	feq2i	$$⊢F:X⟶\left[0,\mathrm{+\infty }\right]\leftrightarrow F:\bigcup _{x\in A}B⟶\left[0,\mathrm{+\infty }\right]$$
18	17	a1i	$$⊢\phi \to \left(F:X⟶\left[0,\mathrm{+\infty }\right]\leftrightarrow F:\bigcup _{x\in A}B⟶\left[0,\mathrm{+\infty }\right]\right)$$
19	4 18	mpbid	$$⊢\phi \to F:\bigcup _{x\in A}B⟶\left[0,\mathrm{+\infty }\right]$$
20	19	feqmptd	$$⊢\phi \to F=\left(y\in \bigcup _{x\in A}B⟼F\left(y\right)\right)$$
21	20	fveq2d	$$⊢\phi \to \mathrm{sum^}\left(F\right)=\mathrm{sum^}\left(\left(y\in \bigcup _{x\in A}B⟼F\left(y\right)\right)\right)$$
22	6 11	fssresd	$$⊢\left(\phi \wedge x\in A\right)\to \left({F\upharpoonright }_B\right):B⟶\left[0,\mathrm{+\infty }\right]$$
23	22	feqmptd	$$⊢\left(\phi \wedge x\in A\right)\to {F\upharpoonright }_B=\left(y\in B⟼\left({F\upharpoonright }_B\right)\left(y\right)\right)$$
24		fvres	$$⊢y\in B\to \left({F\upharpoonright }_B\right)\left(y\right)=F\left(y\right)$$
25	24	mpteq2ia	$$⊢\left(y\in B⟼\left({F\upharpoonright }_B\right)\left(y\right)\right)=\left(y\in B⟼F\left(y\right)\right)$$
26	25	a1i	$$⊢\left(\phi \wedge x\in A\right)\to \left(y\in B⟼\left({F\upharpoonright }_B\right)\left(y\right)\right)=\left(y\in B⟼F\left(y\right)\right)$$
27	23 26	eqtrd	$$⊢\left(\phi \wedge x\in A\right)\to {F\upharpoonright }_B=\left(y\in B⟼F\left(y\right)\right)$$
28	27	fveq2d	$$⊢\left(\phi \wedge x\in A\right)\to \mathrm{sum^}\left({F\upharpoonright }_B\right)=\mathrm{sum^}\left(\left(y\in B⟼F\left(y\right)\right)\right)$$
29	28	mpteq2dva	$$⊢\phi \to \left(x\in A⟼\mathrm{sum^}\left({F\upharpoonright }_B\right)\right)=\left(x\in A⟼\mathrm{sum^}\left(\left(y\in B⟼F\left(y\right)\right)\right)\right)$$
30	29	fveq2d	$$⊢\phi \to \mathrm{sum^}\left(\left(x\in A⟼\mathrm{sum^}\left({F\upharpoonright }_B\right)\right)\right)=\mathrm{sum^}\left(\left(x\in A⟼\mathrm{sum^}\left(\left(y\in B⟼F\left(y\right)\right)\right)\right)\right)$$
31	16 21 30	3eqtr4d	$$⊢\phi \to \mathrm{sum^}\left(F\right)=\mathrm{sum^}\left(\left(x\in A⟼\mathrm{sum^}\left({F\upharpoonright }_B\right)\right)\right)$$