This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )