This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐹 ) ∈ 𝑆 )