Metamath Proof Explorer

Theorem esumeq2

Description: Equality theorem for extended sum. (Contributed by Thierry Arnoux, 24-Dec-2016)

Ref Expression
Assertion esumeq2 
|- ( A. k e. A B = C -> sum* k e. A B = sum* k e. A C )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 mpteq12 
 |-  ( ( A = A /\ A. k e. A B = C ) -> ( k e. A |-> B ) = ( k e. A |-> C ) )
3 1 2 mpan 
 |-  ( A. k e. A B = C -> ( k e. A |-> B ) = ( k e. A |-> C ) )
4 3 oveq2d 
 |-  ( A. k e. A B = C -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) ) )
5 4 unieqd 
 |-  ( A. k e. A B = C -> U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) ) )
6 df-esum 
 |-  sum* k e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
7 df-esum 
 |-  sum* k e. A C = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) )
8 5 6 7 3eqtr4g 
 |-  ( A. k e. A B = C -> sum* k e. A B = sum* k e. A C )