Metamath Proof Explorer

Theorem seqdistr

Description: The distributive property for series. (Contributed by Mario Carneiro, 28-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqdistr.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
seqdistr.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐶 𝑇 ( 𝑥 + 𝑦 ) ) = ( ( 𝐶 𝑇 𝑥 ) + ( 𝐶 𝑇 𝑦 ) ) )
seqdistr.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
seqdistr.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑆 )
seqdistr.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐶 𝑇 ( 𝐺 ‘ 𝑥 ) ) )
Assertion seqdistr ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐶 𝑇 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 seqdistr.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2 seqdistr.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐶 𝑇 ( 𝑥 + 𝑦 ) ) = ( ( 𝐶 𝑇 𝑥 ) + ( 𝐶 𝑇 𝑦 ) ) )
3 seqdistr.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
4 seqdistr.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑆 )
5 seqdistr.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐶 𝑇 ( 𝐺 ‘ 𝑥 ) ) )
6 oveq2 ⊢ ( 𝑧 = ( 𝑥 + 𝑦 ) → ( 𝐶 𝑇 𝑧 ) = ( 𝐶 𝑇 ( 𝑥 + 𝑦 ) ) )
7 eqid ⊢ ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) = ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) )
8 ovex ⊢ ( 𝐶 𝑇 ( 𝑥 + 𝑦 ) ) ∈ V
9 6 7 8 fvmpt ⊢ ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐶 𝑇 ( 𝑥 + 𝑦 ) ) )
10 1 9 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐶 𝑇 ( 𝑥 + 𝑦 ) ) )
11 oveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐶 𝑇 𝑧 ) = ( 𝐶 𝑇 𝑥 ) )
12 ovex ⊢ ( 𝐶 𝑇 𝑥 ) ∈ V
13 11 7 12 fvmpt ⊢ ( 𝑥 ∈ 𝑆 → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ 𝑥 ) = ( 𝐶 𝑇 𝑥 ) )
14 13 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ 𝑥 ) = ( 𝐶 𝑇 𝑥 ) )
15 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐶 𝑇 𝑧 ) = ( 𝐶 𝑇 𝑦 ) )
16 ovex ⊢ ( 𝐶 𝑇 𝑦 ) ∈ V
17 15 7 16 fvmpt ⊢ ( 𝑦 ∈ 𝑆 → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ 𝑦 ) = ( 𝐶 𝑇 𝑦 ) )
18 17 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ 𝑦 ) = ( 𝐶 𝑇 𝑦 ) )
19 14 18 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ 𝑥 ) + ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ 𝑦 ) ) = ( ( 𝐶 𝑇 𝑥 ) + ( 𝐶 𝑇 𝑦 ) ) )
20 2 10 19 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ 𝑥 ) + ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ 𝑦 ) ) )
21 oveq2 ⊢ ( 𝑧 = ( 𝐺 ‘ 𝑥 ) → ( 𝐶 𝑇 𝑧 ) = ( 𝐶 𝑇 ( 𝐺 ‘ 𝑥 ) ) )
22 ovex ⊢ ( 𝐶 𝑇 ( 𝐺 ‘ 𝑥 ) ) ∈ V
23 21 7 22 fvmpt ⊢ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑆 → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ ( 𝐺 ‘ 𝑥 ) ) = ( 𝐶 𝑇 ( 𝐺 ‘ 𝑥 ) ) )
24 4 23 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ ( 𝐺 ‘ 𝑥 ) ) = ( 𝐶 𝑇 ( 𝐺 ‘ 𝑥 ) ) )
25 24 5 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ ( 𝐺 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
26 1 4 3 20 25 seqhomo ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
27 3 4 1 seqcl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ∈ 𝑆 )
28 oveq2 ⊢ ( 𝑧 = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) → ( 𝐶 𝑇 𝑧 ) = ( 𝐶 𝑇 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )
29 ovex ⊢ ( 𝐶 𝑇 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) ∈ V
30 28 7 29 fvmpt ⊢ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ∈ 𝑆 → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) = ( 𝐶 𝑇 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )
31 27 30 syl ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝑆 ↦ ( 𝐶 𝑇 𝑧 ) ) ‘ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) = ( 𝐶 𝑇 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )
32 26 31 eqtr3d ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐶 𝑇 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )