Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Monoids (extension)
Group sum operation (extension 1)
gsumfsupp
Metamath Proof Explorer
Description: A group sum of a family can be restricted to the support of that family
without changing its value, provided that that support is finite. This
corresponds to the definition of an (infinite) product in Lang p. 5,
last two formulas. (Contributed by AV , 27-Dec-2023)
Ref
Expression
Hypotheses
gsumfsupp.b
|- B = ( Base ` G )
gsumfsupp.z
|- .0. = ( 0g ` G )
gsumfsupp.s
|- I = ( F supp .0. )
gsumfsupp.g
|- ( ph -> G e. CMnd )
gsumfsupp.a
|- ( ph -> A e. V )
gsumfsupp.f
|- ( ph -> F : A --> B )
gsumfsupp.w
|- ( ph -> F finSupp .0. )
Assertion
gsumfsupp
|- ( ph -> ( G gsum ( F |` I ) ) = ( G gsum F ) )
Proof
Step
Hyp
Ref
Expression
1
gsumfsupp.b
|- B = ( Base ` G )
2
gsumfsupp.z
|- .0. = ( 0g ` G )
3
gsumfsupp.s
|- I = ( F supp .0. )
4
gsumfsupp.g
|- ( ph -> G e. CMnd )
5
gsumfsupp.a
|- ( ph -> A e. V )
6
gsumfsupp.f
|- ( ph -> F : A --> B )
7
gsumfsupp.w
|- ( ph -> F finSupp .0. )
8
3
eqimss2i
|- ( F supp .0. ) C_ I
9
8
a1i
|- ( ph -> ( F supp .0. ) C_ I )
10
1 2 4 5 6 9 7
gsumres
|- ( ph -> ( G gsum ( F |` I ) ) = ( G gsum F ) )