Theorem fsummulc2

Description: A finite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	fsummulc2.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsummulc2.2	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	fsummulc2.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion	fsummulc2	⊢ ( 𝜑 → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fsummulc2.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		fsummulc2.2	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
3		fsummulc2.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4	2	mul01d	⊢ ( 𝜑 → ( 𝐶 · 0 ) = 0 )
5		sumeq1	⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
6		sum0	⊢ Σ 𝑘 ∈ ∅ 𝐵 = 0
7	5 6	eqtrdi	⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 𝐵 = 0 )
8	7	oveq2d	⊢ ( 𝐴 = ∅ → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = ( 𝐶 · 0 ) )
9		sumeq1	⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) = Σ 𝑘 ∈ ∅ ( 𝐶 · 𝐵 ) )
10		sum0	⊢ Σ 𝑘 ∈ ∅ ( 𝐶 · 𝐵 ) = 0
11	9 10	eqtrdi	⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) = 0 )
12	8 11	eqeq12d	⊢ ( 𝐴 = ∅ → ( ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) ↔ ( 𝐶 · 0 ) = 0 ) )
13	4 12	syl5ibrcom	⊢ ( 𝜑 → ( 𝐴 = ∅ → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) ) )
14		addcl	⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 𝑛 + 𝑚 ) ∈ ℂ )
15	14	adantl	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( 𝑛 + 𝑚 ) ∈ ℂ )
16	2	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝐶 ∈ ℂ )
17		adddi	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 𝐶 · ( 𝑛 + 𝑚 ) ) = ( ( 𝐶 · 𝑛 ) + ( 𝐶 · 𝑚 ) ) )
18	17	3expb	⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( 𝐶 · ( 𝑛 + 𝑚 ) ) = ( ( 𝐶 · 𝑛 ) + ( 𝐶 · 𝑚 ) ) )
19	16 18	sylan	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( 𝐶 · ( 𝑛 + 𝑚 ) ) = ( ( 𝐶 · 𝑛 ) + ( 𝐶 · 𝑚 ) ) )
20		simprl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
21		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
22	20 21	eleqtrdi	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
23	3	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
24	23	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
25		simprr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
26	25	adantr	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
27		f1of	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
28	26 27	syl	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
29		fco	⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
30	24 28 29	syl2anc	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
31		simpr	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
32	30 31	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) ∈ ℂ )
33	28 31	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 )
34		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
35	2	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
36	35 3	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
37		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) )
38	37	fvmpt2	⊢ ( ( 𝑘 ∈ 𝐴 ∧ ( 𝐶 · 𝐵 ) ∈ ℂ ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · 𝐵 ) )
39	34 36 38	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · 𝐵 ) )
40		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
41	40	fvmpt2	⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
42	34 3 41	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
43	42	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( 𝐶 · 𝐵 ) )
44	39 43	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) )
45	44	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) )
46	45	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) )
47		nffvmpt1	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) )
48		nfcv	⊢ Ⅎ 𝑘 𝐶
49		nfcv	⊢ Ⅎ 𝑘 ·
50		nffvmpt1	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) )
51	48 49 50	nfov	⊢ Ⅎ 𝑘 ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
52	47 51	nfeq	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
53		fveq2	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
54		fveq2	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
55	54	oveq2d	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
56	53 55	eqeq12d	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) ↔ ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
57	52 56	rspc	⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
58	33 46 57	sylc	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
59	27	ad2antll	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
60		fvco3	⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
61	59 60	sylan	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
62		fvco3	⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
63	59 62	sylan	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
64	63	oveq2d	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐶 · ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
65	58 61 64	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∘ 𝑓 ) ‘ 𝑛 ) = ( 𝐶 · ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) ) )
66	15 19 22 32 65	seqdistr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐶 · ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) )
67		fveq2	⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
68	36	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) : 𝐴 ⟶ ℂ )
69	68	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) : 𝐴 ⟶ ℂ )
70	69	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑚 ) ∈ ℂ )
71	67 20 25 70 61	fsum	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
72		fveq2	⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
73	23	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
74	73	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ∈ ℂ )
75	72 20 25 74 63	fsum	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
76	75	oveq2d	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝐶 · Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ) = ( 𝐶 · ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) )
77	66 71 76	3eqtr4rd	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝐶 · Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ) = Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑚 ) )
78		sumfc	⊢ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝐴 𝐵
79	78	oveq2i	⊢ ( 𝐶 · Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ) = ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 )
80		sumfc	⊢ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 )
81	77 79 80	3eqtr3g	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) )
82	81	expr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) ) )
83	82	exlimdv	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) ) )
84	83	expimpd	⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) ) )
85		fz1f1o	⊢ ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
86	1 85	syl	⊢ ( 𝜑 → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
87	13 84 86	mpjaod	⊢ ( 𝜑 → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) )