Metamath Proof Explorer


Theorem gsumsubmcl

Description: Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 3-Jun-2019)

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

Proof

Step Hyp Ref Expression
1 gsumsubmcl.z 0 = ( 0g𝐺 )
2 gsumsubmcl.g ( 𝜑𝐺 ∈ CMnd )
3 gsumsubmcl.a ( 𝜑𝐴𝑉 )
4 gsumsubmcl.s ( 𝜑𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
5 gsumsubmcl.f ( 𝜑𝐹 : 𝐴𝑆 )
6 gsumsubmcl.w ( 𝜑𝐹 finSupp 0 )
7 eqid ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
8 cmnmnd ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
9 2 8 syl ( 𝜑𝐺 ∈ Mnd )
10 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
11 10 submss ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
12 4 11 syl ( 𝜑𝑆 ⊆ ( Base ‘ 𝐺 ) )
13 5 12 fssd ( 𝜑𝐹 : 𝐴 ⟶ ( Base ‘ 𝐺 ) )
14 10 7 2 13 cntzcmnf ( 𝜑 → ran 𝐹 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐹 ) )
15 1 7 9 3 4 5 14 6 gsumzsubmcl ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝑆 )