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 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
seqcaopr.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
seqcaopr.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
seqcaopr.4 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
seqcaopr.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
seqcaopr.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑆 )
seqcaopr.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) )
Assertion seqcaopr ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 seqcaopr.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2 seqcaopr.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
3 seqcaopr.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
4 seqcaopr.4 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 seqcaopr.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
6 seqcaopr.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑆 )
7 seqcaopr.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) )
8 1 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝑆 )
9 simpl ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → 𝜑 )
10 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → 𝑐 ∈ 𝑆 )
11 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → 𝑏 ∈ 𝑆 )
12 2 caovcomg ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑐 + 𝑏 ) = ( 𝑏 + 𝑐 ) )
13 9 10 11 12 syl12anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ( 𝑐 + 𝑏 ) = ( 𝑏 + 𝑐 ) )
14 13 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ( ( 𝑐 + 𝑏 ) + 𝑑 ) = ( ( 𝑏 + 𝑐 ) + 𝑑 ) )
15 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → 𝑑 ∈ 𝑆 )
16 3 caovassg ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → ( ( 𝑐 + 𝑏 ) + 𝑑 ) = ( 𝑐 + ( 𝑏 + 𝑑 ) ) )
17 9 10 11 15 16 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ( ( 𝑐 + 𝑏 ) + 𝑑 ) = ( 𝑐 + ( 𝑏 + 𝑑 ) ) )
18 3 caovassg ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → ( ( 𝑏 + 𝑐 ) + 𝑑 ) = ( 𝑏 + ( 𝑐 + 𝑑 ) ) )
19 9 11 10 15 18 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ( ( 𝑏 + 𝑐 ) + 𝑑 ) = ( 𝑏 + ( 𝑐 + 𝑑 ) ) )
20 14 17 19 3eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ( 𝑐 + ( 𝑏 + 𝑑 ) ) = ( 𝑏 + ( 𝑐 + 𝑑 ) ) )
21 20 oveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ( 𝑎 + ( 𝑐 + ( 𝑏 + 𝑑 ) ) ) = ( 𝑎 + ( 𝑏 + ( 𝑐 + 𝑑 ) ) ) )
22 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → 𝑎 ∈ 𝑆 )
23 1 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → ( 𝑏 + 𝑑 ) ∈ 𝑆 )
24 9 11 15 23 syl12anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ( 𝑏 + 𝑑 ) ∈ 𝑆 )
25 3 caovassg ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ∧ ( 𝑏 + 𝑑 ) ∈ 𝑆 ) ) → ( ( 𝑎 + 𝑐 ) + ( 𝑏 + 𝑑 ) ) = ( 𝑎 + ( 𝑐 + ( 𝑏 + 𝑑 ) ) ) )
26 9 22 10 24 25 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ( ( 𝑎 + 𝑐 ) + ( 𝑏 + 𝑑 ) ) = ( 𝑎 + ( 𝑐 + ( 𝑏 + 𝑑 ) ) ) )
27 1 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → ( 𝑐 + 𝑑 ) ∈ 𝑆 )
28 27 adantrl ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ( 𝑐 + 𝑑 ) ∈ 𝑆 )
29 3 caovassg ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ ( 𝑐 + 𝑑 ) ∈ 𝑆 ) ) → ( ( 𝑎 + 𝑏 ) + ( 𝑐 + 𝑑 ) ) = ( 𝑎 + ( 𝑏 + ( 𝑐 + 𝑑 ) ) ) )
30 9 22 11 28 29 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ( ( 𝑎 + 𝑏 ) + ( 𝑐 + 𝑑 ) ) = ( 𝑎 + ( 𝑏 + ( 𝑐 + 𝑑 ) ) ) )
31 21 26 30 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) ) → ( ( 𝑎 + 𝑐 ) + ( 𝑏 + 𝑑 ) ) = ( ( 𝑎 + 𝑏 ) + ( 𝑐 + 𝑑 ) ) )
32 8 8 31 4 5 6 7 seqcaopr2 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )