Metamath Proof Explorer

Theorem regsumsupp

Description: The group sum over the real numbers, expressed as a finite sum. (Contributed by Thierry Arnoux, 22-Jun-2019) (Proof shortened by AV, 19-Jul-2019)

Ref Expression
Assertion regsumsupp ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( ℝfld Σg 𝐹 ) = Σ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐹 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
2 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
3 cnring ⊢ ℂfld ∈ Ring
4 ringcmn ⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
5 3 4 mp1i ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ℂfld ∈ CMnd )
6 simp3 ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → 𝐼 ∈ 𝑉 )
7 simp1 ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → 𝐹 : 𝐼 ⟶ ℝ )
8 ax-resscn ⊢ ℝ ⊆ ℂ
9 fss ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : 𝐼 ⟶ ℂ )
10 7 8 9 sylancl ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → 𝐹 : 𝐼 ⟶ ℂ )
11 ssidd ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
12 simp2 ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → 𝐹 finSupp 0 )
13 1 2 5 6 10 11 12 gsumres ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( ℂfld Σg ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) = ( ℂfld Σg 𝐹 ) )
14 cnfldadd ⊢ + = ( +g ‘ ℂfld )
15 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
16 8 a1i ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ℝ ⊆ ℂ )
17 0red ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → 0 ∈ ℝ )
18 simpr ⊢ ( ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
19 18 addlidd ⊢ ( ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑥 ∈ ℂ ) → ( 0 + 𝑥 ) = 𝑥 )
20 18 addridd ⊢ ( ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑥 ∈ ℂ ) → ( 𝑥 + 0 ) = 𝑥 )
21 19 20 jca ⊢ ( ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑥 ∈ ℂ ) → ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) )
22 1 14 15 5 6 16 7 17 21 gsumress ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( ℂfld Σg 𝐹 ) = ( ℝfld Σg 𝐹 ) )
23 13 22 eqtr2d ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( ℝfld Σg 𝐹 ) = ( ℂfld Σg ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) )
24 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
25 24 7 fssdm ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( 𝐹 supp 0 ) ⊆ 𝐼 )
26 7 25 feqresmpt ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝑥 ∈ ( 𝐹 supp 0 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
27 26 oveq2d ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( ℂfld Σg ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) = ( ℂfld Σg ( 𝑥 ∈ ( 𝐹 supp 0 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
28 12 fsuppimpd ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( 𝐹 supp 0 ) ∈ Fin )
29 simpl1 ⊢ ( ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → 𝐹 : 𝐼 ⟶ ℝ )
30 25 sselda ⊢ ( ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → 𝑥 ∈ 𝐼 )
31 29 30 ffvelcdmd ⊢ ( ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
32 8 31 sselid ⊢ ( ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
33 28 32 gsumfsum ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( ℂfld Σg ( 𝑥 ∈ ( 𝐹 supp 0 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = Σ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐹 ‘ 𝑥 ) )
34 23 27 33 3eqtrd ⊢ ( ( 𝐹 : 𝐼 ⟶ ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( ℝfld Σg 𝐹 ) = Σ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐹 ‘ 𝑥 ) )