Theorem sge0splitmpt

Description: Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0splitmpt.xph	|- F/ x ph
	sge0splitmpt.a	|- ( ph -> A e. V )
	sge0splitmpt.b	|- ( ph -> B e. W )
	sge0splitmpt.in	|- ( ph -> ( A i^i B ) = (/) )
	sge0splitmpt.ac	|- ( ( ph /\ x e. A ) -> C e. ( 0 [,] +oo ) )
	sge0splitmpt.bc	|- ( ( ph /\ x e. B ) -> C e. ( 0 [,] +oo ) )
Assertion	sge0splitmpt	|- ( ph -> ( sum^ ` ( x e. ( A u. B ) |-> C ) ) = ( ( sum^ ` ( x e. A |-> C ) ) +e ( sum^ ` ( x e. B |-> C ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0splitmpt.xph	|- F/ x ph
2		sge0splitmpt.a	|- ( ph -> A e. V )
3		sge0splitmpt.b	|- ( ph -> B e. W )
4		sge0splitmpt.in	|- ( ph -> ( A i^i B ) = (/) )
5		sge0splitmpt.ac	|- ( ( ph /\ x e. A ) -> C e. ( 0 [,] +oo ) )
6		sge0splitmpt.bc	|- ( ( ph /\ x e. B ) -> C e. ( 0 [,] +oo ) )
7		eqid	|- ( A u. B ) = ( A u. B )
8	5	adantlr	|- ( ( ( ph /\ x e. ( A u. B ) ) /\ x e. A ) -> C e. ( 0 [,] +oo ) )
9		simpll	|- ( ( ( ph /\ x e. ( A u. B ) ) /\ -. x e. A ) -> ph )
10		elunnel1	|- ( ( x e. ( A u. B ) /\ -. x e. A ) -> x e. B )
11	10	adantll	|- ( ( ( ph /\ x e. ( A u. B ) ) /\ -. x e. A ) -> x e. B )
12	9 11 6	syl2anc	|- ( ( ( ph /\ x e. ( A u. B ) ) /\ -. x e. A ) -> C e. ( 0 [,] +oo ) )
13	8 12	pm2.61dan	|- ( ( ph /\ x e. ( A u. B ) ) -> C e. ( 0 [,] +oo ) )
14		eqid	|- ( x e. ( A u. B ) |-> C ) = ( x e. ( A u. B ) |-> C )
15	1 13 14	fmptdf	|- ( ph -> ( x e. ( A u. B ) |-> C ) : ( A u. B ) --> ( 0 [,] +oo ) )
16	2 3 7 4 15	sge0split	|- ( ph -> ( sum^ ` ( x e. ( A u. B ) |-> C ) ) = ( ( sum^ ` ( ( x e. ( A u. B ) |-> C ) |` A ) ) +e ( sum^ ` ( ( x e. ( A u. B ) |-> C ) |` B ) ) ) )
17		ssun1	|- A C_ ( A u. B )
18	17	resmpti	|- ( ( x e. ( A u. B ) |-> C ) |` A ) = ( x e. A |-> C )
19	18	fveq2i	|- ( sum^ ` ( ( x e. ( A u. B ) |-> C ) |` A ) ) = ( sum^ ` ( x e. A |-> C ) )
20		ssun2	|- B C_ ( A u. B )
21	20	resmpti	|- ( ( x e. ( A u. B ) |-> C ) |` B ) = ( x e. B |-> C )
22	21	fveq2i	|- ( sum^ ` ( ( x e. ( A u. B ) |-> C ) |` B ) ) = ( sum^ ` ( x e. B |-> C ) )
23	19 22	oveq12i	|- ( ( sum^ ` ( ( x e. ( A u. B ) |-> C ) |` A ) ) +e ( sum^ ` ( ( x e. ( A u. B ) |-> C ) |` B ) ) ) = ( ( sum^ ` ( x e. A |-> C ) ) +e ( sum^ ` ( x e. B |-> C ) ) )
24	23	a1i	|- ( ph -> ( ( sum^ ` ( ( x e. ( A u. B ) |-> C ) |` A ) ) +e ( sum^ ` ( ( x e. ( A u. B ) |-> C ) |` B ) ) ) = ( ( sum^ ` ( x e. A |-> C ) ) +e ( sum^ ` ( x e. B |-> C ) ) ) )
25	16 24	eqtrd	|- ( ph -> ( sum^ ` ( x e. ( A u. B ) |-> C ) ) = ( ( sum^ ` ( x e. A |-> C ) ) +e ( sum^ ` ( x e. B |-> C ) ) ) )