Metamath Proof Explorer

Theorem seqcaopr

Description: The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 30-May-2014)

Ref Expression
Hypotheses seqcaopr.1 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
seqcaopr.2 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( y .+ x ) )
seqcaopr.3 
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
seqcaopr.4 
|- ( ph -> N e. ( ZZ>= ` M ) )
seqcaopr.5 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. S )
seqcaopr.6 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. S )
seqcaopr.7 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) .+ ( G ` k ) ) )
Assertion seqcaopr 
|- ( ph -> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) .+ ( seq M ( .+ , G ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 seqcaopr.1 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
2 seqcaopr.2 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( y .+ x ) )
3 seqcaopr.3 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
4 seqcaopr.4 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 seqcaopr.5 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. S )
6 seqcaopr.6 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. S )
7 seqcaopr.7 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) .+ ( G ` k ) ) )
8 1 caovclg 
 |-  ( ( ph /\ ( a e. S /\ b e. S ) ) -> ( a .+ b ) e. S )
9 simpl 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> ph )
10 simprrl 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> c e. S )
11 simprlr 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> b e. S )
12 2 caovcomg 
 |-  ( ( ph /\ ( c e. S /\ b e. S ) ) -> ( c .+ b ) = ( b .+ c ) )
13 9 10 11 12 syl12anc 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> ( c .+ b ) = ( b .+ c ) )
14 13 oveq1d 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> ( ( c .+ b ) .+ d ) = ( ( b .+ c ) .+ d ) )
15 simprrr 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> d e. S )
16 3 caovassg 
 |-  ( ( ph /\ ( c e. S /\ b e. S /\ d e. S ) ) -> ( ( c .+ b ) .+ d ) = ( c .+ ( b .+ d ) ) )
17 9 10 11 15 16 syl13anc 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> ( ( c .+ b ) .+ d ) = ( c .+ ( b .+ d ) ) )
18 3 caovassg 
 |-  ( ( ph /\ ( b e. S /\ c e. S /\ d e. S ) ) -> ( ( b .+ c ) .+ d ) = ( b .+ ( c .+ d ) ) )
19 9 11 10 15 18 syl13anc 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> ( ( b .+ c ) .+ d ) = ( b .+ ( c .+ d ) ) )
20 14 17 19 3eqtr3d 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> ( c .+ ( b .+ d ) ) = ( b .+ ( c .+ d ) ) )
21 20 oveq2d 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> ( a .+ ( c .+ ( b .+ d ) ) ) = ( a .+ ( b .+ ( c .+ d ) ) ) )
22 simprll 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> a e. S )
23 1 caovclg 
 |-  ( ( ph /\ ( b e. S /\ d e. S ) ) -> ( b .+ d ) e. S )
24 9 11 15 23 syl12anc 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> ( b .+ d ) e. S )
25 3 caovassg 
 |-  ( ( ph /\ ( a e. S /\ c e. S /\ ( b .+ d ) e. S ) ) -> ( ( a .+ c ) .+ ( b .+ d ) ) = ( a .+ ( c .+ ( b .+ d ) ) ) )
26 9 22 10 24 25 syl13anc 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> ( ( a .+ c ) .+ ( b .+ d ) ) = ( a .+ ( c .+ ( b .+ d ) ) ) )
27 1 caovclg 
 |-  ( ( ph /\ ( c e. S /\ d e. S ) ) -> ( c .+ d ) e. S )
28 27 adantrl 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> ( c .+ d ) e. S )
29 3 caovassg 
 |-  ( ( ph /\ ( a e. S /\ b e. S /\ ( c .+ d ) e. S ) ) -> ( ( a .+ b ) .+ ( c .+ d ) ) = ( a .+ ( b .+ ( c .+ d ) ) ) )
30 9 22 11 28 29 syl13anc 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> ( ( a .+ b ) .+ ( c .+ d ) ) = ( a .+ ( b .+ ( c .+ d ) ) ) )
31 21 26 30 3eqtr4d 
 |-  ( ( ph /\ ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) ) -> ( ( a .+ c ) .+ ( b .+ d ) ) = ( ( a .+ b ) .+ ( c .+ d ) ) )
32 8 8 31 4 5 6 7 seqcaopr2 
 |-  ( ph -> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) .+ ( seq M ( .+ , G ) ` N ) ) )