Theorem regsumfsum

Description: Relate a group sum on ` ( CCfld |``s RR ) ` to a finite sum on the reals. Cf. gsumfsum . (Contributed by Thierry Arnoux, 7-Sep-2018)

	Ref	Expression
Hypotheses	regsumfsum.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	regsumfsum.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
Assertion	regsumfsum	⊢ ( 𝜑 → ( ( ℂfld ↾s ℝ ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		regsumfsum.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		regsumfsum.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
4		cnfldadd	⊢ + = ( +g ‘ ℂfld )
5		eqid	⊢ ( ℂfld ↾s ℝ ) = ( ℂfld ↾s ℝ )
6		cnfldex	⊢ ℂfld ∈ V
7	6	a1i	⊢ ( 𝜑 → ℂfld ∈ V )
8		ax-resscn	⊢ ℝ ⊆ ℂ
9	8	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
10	2	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )
11		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
13	12	addlidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 0 + 𝑥 ) = 𝑥 )
14	12	addridd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑥 + 0 ) = 𝑥 )
15	13 14	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) )
16	3 4 5 7 1 9 10 11 15	gsumress	⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ( ℂfld ↾s ℝ ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
17	2	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
18	1 17	gsumfsum	⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )
19	16 18	eqtr3d	⊢ ( 𝜑 → ( ( ℂfld ↾s ℝ ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )