Metamath Proof Explorer

Theorem sge0ss

Description: Change the index set to a subset in a sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0ss.kph 
|- F/ k ph
sge0ss.b 
|- ( ph -> B e. V )
sge0ss.a 
|- ( ph -> A C_ B )
sge0ss.c 
|- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
sge0ss.c0 
|- ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )
Assertion sge0ss 
|- ( ph -> ( sum^ ` ( k e. A |-> C ) ) = ( sum^ ` ( k e. B |-> C ) ) )

Proof

Step Hyp Ref Expression
1 sge0ss.kph 
 |-  F/ k ph
2 sge0ss.b 
 |-  ( ph -> B e. V )
3 sge0ss.a 
 |-  ( ph -> A C_ B )
4 sge0ss.c 
 |-  ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
5 sge0ss.c0 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )
6 ssexg 
 |-  ( ( A C_ B /\ B e. V ) -> A e. _V )
7 3 2 6 syl2anc 
 |-  ( ph -> A e. _V )
8 2 difexd 
 |-  ( ph -> ( B \ A ) e. _V )
9 disjdif 
 |-  ( A i^i ( B \ A ) ) = (/)
10 9 a1i 
 |-  ( ph -> ( A i^i ( B \ A ) ) = (/) )
11 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
12 11 a1i 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> 0 e. ( 0 [,] +oo ) )
13 5 12 eqeltrd 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C e. ( 0 [,] +oo ) )
14 1 7 8 10 4 13 sge0splitmpt 
 |-  ( ph -> ( sum^ ` ( k e. ( A u. ( B \ A ) ) |-> C ) ) = ( ( sum^ ` ( k e. A |-> C ) ) +e ( sum^ ` ( k e. ( B \ A ) |-> C ) ) ) )
15 14 eqcomd 
 |-  ( ph -> ( ( sum^ ` ( k e. A |-> C ) ) +e ( sum^ ` ( k e. ( B \ A ) |-> C ) ) ) = ( sum^ ` ( k e. ( A u. ( B \ A ) ) |-> C ) ) )
16 1 5 mpteq2da 
 |-  ( ph -> ( k e. ( B \ A ) |-> C ) = ( k e. ( B \ A ) |-> 0 ) )
17 16 fveq2d 
 |-  ( ph -> ( sum^ ` ( k e. ( B \ A ) |-> C ) ) = ( sum^ ` ( k e. ( B \ A ) |-> 0 ) ) )
18 1 8 sge0z 
 |-  ( ph -> ( sum^ ` ( k e. ( B \ A ) |-> 0 ) ) = 0 )
19 17 18 eqtrd 
 |-  ( ph -> ( sum^ ` ( k e. ( B \ A ) |-> C ) ) = 0 )
20 19 oveq2d 
 |-  ( ph -> ( ( sum^ ` ( k e. A |-> C ) ) +e ( sum^ ` ( k e. ( B \ A ) |-> C ) ) ) = ( ( sum^ ` ( k e. A |-> C ) ) +e 0 ) )
21 eqid 
 |-  ( k e. A |-> C ) = ( k e. A |-> C )
22 1 4 21 fmptdf 
 |-  ( ph -> ( k e. A |-> C ) : A --> ( 0 [,] +oo ) )
23 7 22 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( k e. A |-> C ) ) e. RR* )
24 xaddid1 
 |-  ( ( sum^ ` ( k e. A |-> C ) ) e. RR* -> ( ( sum^ ` ( k e. A |-> C ) ) +e 0 ) = ( sum^ ` ( k e. A |-> C ) ) )
25 23 24 syl 
 |-  ( ph -> ( ( sum^ ` ( k e. A |-> C ) ) +e 0 ) = ( sum^ ` ( k e. A |-> C ) ) )
26 eqidd 
 |-  ( ph -> ( sum^ ` ( k e. A |-> C ) ) = ( sum^ ` ( k e. A |-> C ) ) )
27 20 25 26 3eqtrrd 
 |-  ( ph -> ( sum^ ` ( k e. A |-> C ) ) = ( ( sum^ ` ( k e. A |-> C ) ) +e ( sum^ ` ( k e. ( B \ A ) |-> C ) ) ) )
28 undif 
 |-  ( A C_ B <-> ( A u. ( B \ A ) ) = B )
29 3 28 sylib 
 |-  ( ph -> ( A u. ( B \ A ) ) = B )
30 29 eqcomd 
 |-  ( ph -> B = ( A u. ( B \ A ) ) )
31 30 mpteq1d 
 |-  ( ph -> ( k e. B |-> C ) = ( k e. ( A u. ( B \ A ) ) |-> C ) )
32 31 fveq2d 
 |-  ( ph -> ( sum^ ` ( k e. B |-> C ) ) = ( sum^ ` ( k e. ( A u. ( B \ A ) ) |-> C ) ) )
33 15 27 32 3eqtr4d 
 |-  ( ph -> ( sum^ ` ( k e. A |-> C ) ) = ( sum^ ` ( k e. B |-> C ) ) )