Metamath Proof Explorer


Theorem gsumsubgcl

Description: Closure of a group sum in a subgroup. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by AV, 3-Jun-2019)

Ref Expression
Hypotheses gsumsubgcl.z 0 = ( 0g𝐺 )
gsumsubgcl.g ( 𝜑𝐺 ∈ Abel )
gsumsubgcl.a ( 𝜑𝐴𝑉 )
gsumsubgcl.s ( 𝜑𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
gsumsubgcl.f ( 𝜑𝐹 : 𝐴𝑆 )
gsumsubgcl.w ( 𝜑𝐹 finSupp 0 )
Assertion gsumsubgcl ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 gsumsubgcl.z 0 = ( 0g𝐺 )
2 gsumsubgcl.g ( 𝜑𝐺 ∈ Abel )
3 gsumsubgcl.a ( 𝜑𝐴𝑉 )
4 gsumsubgcl.s ( 𝜑𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
5 gsumsubgcl.f ( 𝜑𝐹 : 𝐴𝑆 )
6 gsumsubgcl.w ( 𝜑𝐹 finSupp 0 )
7 ablcmn ( 𝐺 ∈ Abel → 𝐺 ∈ CMnd )
8 2 7 syl ( 𝜑𝐺 ∈ CMnd )
9 subgsubm ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
10 4 9 syl ( 𝜑𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
11 1 8 3 10 5 6 gsumsubmcl ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝑆 )