Metamath Proof Explorer


Theorem gsumsubm

Description: Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014)

Ref Expression
Hypotheses gsumsubm.a ( 𝜑𝐴𝑉 )
gsumsubm.s ( 𝜑𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
gsumsubm.f ( 𝜑𝐹 : 𝐴𝑆 )
gsumsubm.h 𝐻 = ( 𝐺s 𝑆 )
Assertion gsumsubm ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )

Proof

Step Hyp Ref Expression
1 gsumsubm.a ( 𝜑𝐴𝑉 )
2 gsumsubm.s ( 𝜑𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
3 gsumsubm.f ( 𝜑𝐹 : 𝐴𝑆 )
4 gsumsubm.h 𝐻 = ( 𝐺s 𝑆 )
5 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 eqid ( +g𝐺 ) = ( +g𝐺 )
7 submrcl ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝐺 ∈ Mnd )
8 2 7 syl ( 𝜑𝐺 ∈ Mnd )
9 5 submss ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
10 2 9 syl ( 𝜑𝑆 ⊆ ( Base ‘ 𝐺 ) )
11 eqid ( 0g𝐺 ) = ( 0g𝐺 )
12 11 subm0cl ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 0g𝐺 ) ∈ 𝑆 )
13 2 12 syl ( 𝜑 → ( 0g𝐺 ) ∈ 𝑆 )
14 5 6 11 mndlrid ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( 0g𝐺 ) ( +g𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐺 ) ( 0g𝐺 ) ) = 𝑥 ) )
15 8 14 sylan ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( 0g𝐺 ) ( +g𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐺 ) ( 0g𝐺 ) ) = 𝑥 ) )
16 5 6 4 8 1 10 3 13 15 gsumress ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )