Theorem sge0splitsn

Description: Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	sge0splitsn.ph	|- F/ k ph
	sge0splitsn.a	|- ( ph -> A e. V )
	sge0splitsn.b	|- ( ph -> B e. W )
	sge0splitsn.n	|- ( ph -> -. B e. A )
	sge0splitsn.c	|- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
	sge0splitsn.d	|- ( k = B -> C = D )
	sge0splitsn.e	|- ( ph -> D e. ( 0 [,] +oo ) )
Assertion	sge0splitsn	|- ( ph -> ( sum^ ` ( k e. ( A u. { B } ) |-> C ) ) = ( ( sum^ ` ( k e. A |-> C ) ) +e D ) )

Proof

Step	Hyp	Ref	Expression
1		sge0splitsn.ph	|- F/ k ph
2		sge0splitsn.a	|- ( ph -> A e. V )
3		sge0splitsn.b	|- ( ph -> B e. W )
4		sge0splitsn.n	|- ( ph -> -. B e. A )
5		sge0splitsn.c	|- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
6		sge0splitsn.d	|- ( k = B -> C = D )
7		sge0splitsn.e	|- ( ph -> D e. ( 0 [,] +oo ) )
8		snfi	|- { B } e. Fin
9	8	a1i	|- ( ph -> { B } e. Fin )
10	9	elexd	|- ( ph -> { B } e. _V )
11		disjsn	|- ( ( A i^i { B } ) = (/) <-> -. B e. A )
12	4 11	sylibr	|- ( ph -> ( A i^i { B } ) = (/) )
13		elsni	|- ( k e. { B } -> k = B )
14	6	adantl	|- ( ( ph /\ k = B ) -> C = D )
15	13 14	sylan2	|- ( ( ph /\ k e. { B } ) -> C = D )
16	7	adantr	|- ( ( ph /\ k e. { B } ) -> D e. ( 0 [,] +oo ) )
17	15 16	eqeltrd	|- ( ( ph /\ k e. { B } ) -> C e. ( 0 [,] +oo ) )
18	1 2 10 12 5 17	sge0splitmpt	|- ( ph -> ( sum^ ` ( k e. ( A u. { B } ) |-> C ) ) = ( ( sum^ ` ( k e. A |-> C ) ) +e ( sum^ ` ( k e. { B } |-> C ) ) ) )
19	1 3 7 6	sge0snmptf	|- ( ph -> ( sum^ ` ( k e. { B } |-> C ) ) = D )
20	19	oveq2d	|- ( ph -> ( ( sum^ ` ( k e. A |-> C ) ) +e ( sum^ ` ( k e. { B } |-> C ) ) ) = ( ( sum^ ` ( k e. A |-> C ) ) +e D ) )
21	18 20	eqtrd	|- ( ph -> ( sum^ ` ( k e. ( A u. { B } ) |-> C ) ) = ( ( sum^ ` ( k e. A |-> C ) ) +e D ) )