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 
|- ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> ( RRfld gsum F ) = sum_ x e. ( F supp 0 ) ( F ` x ) )

Proof

Step Hyp Ref Expression
1 cnfldbas 
 |-  CC = ( Base ` CCfld )
2 cnfld0 
 |-  0 = ( 0g ` CCfld )
3 cnring 
 |-  CCfld e. Ring
4 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
5 3 4 mp1i 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> CCfld e. CMnd )
6 simp3 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> I e. V )
7 simp1 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> F : I --> RR )
8 ax-resscn 
 |-  RR C_ CC
9 fss 
 |-  ( ( F : I --> RR /\ RR C_ CC ) -> F : I --> CC )
10 7 8 9 sylancl 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> F : I --> CC )
11 ssidd 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> ( F supp 0 ) C_ ( F supp 0 ) )
12 simp2 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> F finSupp 0 )
13 1 2 5 6 10 11 12 gsumres 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> ( CCfld gsum ( F |` ( F supp 0 ) ) ) = ( CCfld gsum F ) )
14 cnfldadd 
 |-  + = ( +g ` CCfld )
15 df-refld 
 |-  RRfld = ( CCfld |`s RR )
16 8 a1i 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> RR C_ CC )
17 0red 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> 0 e. RR )
18 simpr 
 |-  ( ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) /\ x e. CC ) -> x e. CC )
19 18 addid2d 
 |-  ( ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) /\ x e. CC ) -> ( 0 + x ) = x )
20 18 addid1d 
 |-  ( ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) /\ x e. CC ) -> ( x + 0 ) = x )
21 19 20 jca 
 |-  ( ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) /\ x e. CC ) -> ( ( 0 + x ) = x /\ ( x + 0 ) = x ) )
22 1 14 15 5 6 16 7 17 21 gsumress 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> ( CCfld gsum F ) = ( RRfld gsum F ) )
23 13 22 eqtr2d 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> ( RRfld gsum F ) = ( CCfld gsum ( F |` ( F supp 0 ) ) ) )
24 suppssdm 
 |-  ( F supp 0 ) C_ dom F
25 24 7 fssdm 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> ( F supp 0 ) C_ I )
26 7 25 feqresmpt 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> ( F |` ( F supp 0 ) ) = ( x e. ( F supp 0 ) |-> ( F ` x ) ) )
27 26 oveq2d 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> ( CCfld gsum ( F |` ( F supp 0 ) ) ) = ( CCfld gsum ( x e. ( F supp 0 ) |-> ( F ` x ) ) ) )
28 12 fsuppimpd 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> ( F supp 0 ) e. Fin )
29 simpl1 
 |-  ( ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) /\ x e. ( F supp 0 ) ) -> F : I --> RR )
30 25 sselda 
 |-  ( ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) /\ x e. ( F supp 0 ) ) -> x e. I )
31 29 30 ffvelrnd 
 |-  ( ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) /\ x e. ( F supp 0 ) ) -> ( F ` x ) e. RR )
32 8 31 sseldi 
 |-  ( ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) /\ x e. ( F supp 0 ) ) -> ( F ` x ) e. CC )
33 28 32 gsumfsum 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> ( CCfld gsum ( x e. ( F supp 0 ) |-> ( F ` x ) ) ) = sum_ x e. ( F supp 0 ) ( F ` x ) )
34 23 27 33 3eqtrd 
 |-  ( ( F : I --> RR /\ F finSupp 0 /\ I e. V ) -> ( RRfld gsum F ) = sum_ x e. ( F supp 0 ) ( F ` x ) )