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

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