Metamath Proof Explorer

Theorem esumpr

Description: Extended sum over a pair. (Contributed by Thierry Arnoux, 2-Jan-2017)

Ref Expression
Hypotheses esumpr.1 
|- ( ( ph /\ k = A ) -> C = D )
esumpr.2 
|- ( ( ph /\ k = B ) -> C = E )
esumpr.3 
|- ( ph -> A e. V )
esumpr.4 
|- ( ph -> B e. W )
esumpr.5 
|- ( ph -> D e. ( 0 [,] +oo ) )
esumpr.6 
|- ( ph -> E e. ( 0 [,] +oo ) )
esumpr.7 
|- ( ph -> A =/= B )
Assertion esumpr 
|- ( ph -> sum* k e. { A , B } C = ( D +e E ) )

Proof

Step Hyp Ref Expression
1 esumpr.1 
 |-  ( ( ph /\ k = A ) -> C = D )
2 esumpr.2 
 |-  ( ( ph /\ k = B ) -> C = E )
3 esumpr.3 
 |-  ( ph -> A e. V )
4 esumpr.4 
 |-  ( ph -> B e. W )
5 esumpr.5 
 |-  ( ph -> D e. ( 0 [,] +oo ) )
6 esumpr.6 
 |-  ( ph -> E e. ( 0 [,] +oo ) )
7 esumpr.7 
 |-  ( ph -> A =/= B )
8 df-pr 
 |-  { A , B } = ( { A } u. { B } )
9 esumeq1 
 |-  ( { A , B } = ( { A } u. { B } ) -> sum* k e. { A , B } C = sum* k e. ( { A } u. { B } ) C )
10 8 9 mp1i 
 |-  ( ph -> sum* k e. { A , B } C = sum* k e. ( { A } u. { B } ) C )
11 nfv 
 |-  F/ k ph
12 nfcv 
 |-  F/_ k { A }
13 nfcv 
 |-  F/_ k { B }
14 snex 
 |-  { A } e. _V
15 14 a1i 
 |-  ( ph -> { A } e. _V )
16 snex 
 |-  { B } e. _V
17 16 a1i 
 |-  ( ph -> { B } e. _V )
18 disjsn2 
 |-  ( A =/= B -> ( { A } i^i { B } ) = (/) )
19 7 18 syl 
 |-  ( ph -> ( { A } i^i { B } ) = (/) )
20 elsni 
 |-  ( k e. { A } -> k = A )
21 20 1 sylan2 
 |-  ( ( ph /\ k e. { A } ) -> C = D )
22 5 adantr 
 |-  ( ( ph /\ k e. { A } ) -> D e. ( 0 [,] +oo ) )
23 21 22 eqeltrd 
 |-  ( ( ph /\ k e. { A } ) -> C e. ( 0 [,] +oo ) )
24 elsni 
 |-  ( k e. { B } -> k = B )
25 24 2 sylan2 
 |-  ( ( ph /\ k e. { B } ) -> C = E )
26 6 adantr 
 |-  ( ( ph /\ k e. { B } ) -> E e. ( 0 [,] +oo ) )
27 25 26 eqeltrd 
 |-  ( ( ph /\ k e. { B } ) -> C e. ( 0 [,] +oo ) )
28 11 12 13 15 17 19 23 27 esumsplit 
 |-  ( ph -> sum* k e. ( { A } u. { B } ) C = ( sum* k e. { A } C +e sum* k e. { B } C ) )
29 1 3 5 esumsn 
 |-  ( ph -> sum* k e. { A } C = D )
30 2 4 6 esumsn 
 |-  ( ph -> sum* k e. { B } C = E )
31 29 30 oveq12d 
 |-  ( ph -> ( sum* k e. { A } C +e sum* k e. { B } C ) = ( D +e E ) )
32 10 28 31 3eqtrd 
 |-  ( ph -> sum* k e. { A , B } C = ( D +e E ) )