Theorem isummulc2

Description: An infinite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005) (Revised by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	isumcl.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	isumcl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	isumcl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	isumcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
	isumcl.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
	summulc.6	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion	isummulc2	⊢ ( 𝜑 → ( 𝐵 · Σ 𝑘 ∈ 𝑍 𝐴 ) = Σ 𝑘 ∈ 𝑍 ( 𝐵 · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		isumcl.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		isumcl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		isumcl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4		isumcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
5		isumcl.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6		summulc.6	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
7		sumfc	⊢ Σ 𝑚 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝑍 ( 𝐵 · 𝐴 )
8		eqidd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) )
9	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
10	9 4	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐵 · 𝐴 ) ∈ ℂ )
11	10	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) : 𝑍 ⟶ ℂ )
12	11	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) ∈ ℂ )
13	1 2 3 4 5	isumclim2	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ Σ 𝑘 ∈ 𝑍 𝐴 )
14	3 4	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
15	14	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
16		fveq2	⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
17	16	eleq1d	⊢ ( 𝑘 = 𝑚 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑚 ) ∈ ℂ ) )
18	17	rspccva	⊢ ( ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
19	15 18	sylan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
21		ovex	⊢ ( 𝐵 · 𝐴 ) ∈ V
22		eqid	⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) )
23	22	fvmpt2	⊢ ( ( 𝑘 ∈ 𝑍 ∧ ( 𝐵 · 𝐴 ) ∈ V ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( 𝐵 · 𝐴 ) )
24	20 21 23	sylancl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( 𝐵 · 𝐴 ) )
25	3	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐵 · ( 𝐹 ‘ 𝑘 ) ) = ( 𝐵 · 𝐴 ) )
26	24 25	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( 𝐵 · ( 𝐹 ‘ 𝑘 ) ) )
27	26	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( 𝐵 · ( 𝐹 ‘ 𝑘 ) ) )
28		nffvmpt1	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 )
29	28	nfeq1	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = ( 𝐵 · ( 𝐹 ‘ 𝑚 ) )
30		fveq2	⊢ ( 𝑘 = 𝑚 → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) )
31	16	oveq2d	⊢ ( 𝑘 = 𝑚 → ( 𝐵 · ( 𝐹 ‘ 𝑘 ) ) = ( 𝐵 · ( 𝐹 ‘ 𝑚 ) ) )
32	30 31	eqeq12d	⊢ ( 𝑘 = 𝑚 → ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( 𝐵 · ( 𝐹 ‘ 𝑘 ) ) ↔ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = ( 𝐵 · ( 𝐹 ‘ 𝑚 ) ) ) )
33	29 32	rspc	⊢ ( 𝑚 ∈ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( 𝐵 · ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = ( 𝐵 · ( 𝐹 ‘ 𝑚 ) ) ) )
34	27 33	mpan9	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = ( 𝐵 · ( 𝐹 ‘ 𝑚 ) ) )
35	1 2 6 13 19 34	isermulc2	⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ) ⇝ ( 𝐵 · Σ 𝑘 ∈ 𝑍 𝐴 ) )
36	1 2 8 12 35	isumclim	⊢ ( 𝜑 → Σ 𝑚 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = ( 𝐵 · Σ 𝑘 ∈ 𝑍 𝐴 ) )
37	7 36	syl5reqr	⊢ ( 𝜑 → ( 𝐵 · Σ 𝑘 ∈ 𝑍 𝐴 ) = Σ 𝑘 ∈ 𝑍 ( 𝐵 · 𝐴 ) )