Metamath Proof Explorer

Theorem esumeq12dvaf

Description: Equality deduction for extended sum. (Contributed by Thierry Arnoux, 26-Mar-2017)

Ref Expression
Hypotheses esumeq12dvaf.1 
|- F/ k ph
esumeq12dvaf.2 
|- ( ph -> A = B )
esumeq12dvaf.3 
|- ( ( ph /\ k e. A ) -> C = D )
Assertion esumeq12dvaf 
|- ( ph -> sum* k e. A C = sum* k e. B D )

Proof

Step Hyp Ref Expression
1 esumeq12dvaf.1 
 |-  F/ k ph
2 esumeq12dvaf.2 
 |-  ( ph -> A = B )
3 esumeq12dvaf.3 
 |-  ( ( ph /\ k e. A ) -> C = D )
4 1 2 alrimi 
 |-  ( ph -> A. k A = B )
5 3 ex 
 |-  ( ph -> ( k e. A -> C = D ) )
6 1 5 ralrimi 
 |-  ( ph -> A. k e. A C = D )
7 mpteq12f 
 |-  ( ( A. k A = B /\ A. k e. A C = D ) -> ( k e. A |-> C ) = ( k e. B |-> D ) )
8 4 6 7 syl2anc 
 |-  ( ph -> ( k e. A |-> C ) = ( k e. B |-> D ) )
9 8 oveq2d 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. B |-> D ) ) )
10 9 unieqd 
 |-  ( ph -> U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) ) = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. B |-> D ) ) )
11 df-esum 
 |-  sum* k e. A C = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) )
12 df-esum 
 |-  sum* k e. B D = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. B |-> D ) )
13 10 11 12 3eqtr4g 
 |-  ( ph -> sum* k e. A C = sum* k e. B D )