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

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 ˙ = 0 G
gsumsubgcl.g ⊢ φ → G ∈ Abel
gsumsubgcl.a ⊢ φ → A ∈ V
gsumsubgcl.s ⊢ φ → S ∈ SubGrp ⁡ G
gsumsubgcl.f ⊢ φ → F : A ⟶ S
gsumsubgcl.w ⊢ φ → finSupp 0 ˙⁡ F
Assertion gsumsubgcl ⊢ φ → ∑ G F ∈ S

Proof

Step Hyp Ref Expression
1 gsumsubgcl.z ⊢ 0 ˙ = 0 G
2 gsumsubgcl.g ⊢ φ → G ∈ Abel
3 gsumsubgcl.a ⊢ φ → A ∈ V
4 gsumsubgcl.s ⊢ φ → S ∈ SubGrp ⁡ G
5 gsumsubgcl.f ⊢ φ → F : A ⟶ S
6 gsumsubgcl.w ⊢ φ → finSupp 0 ˙⁡ F
7 ablcmn ⊢ G ∈ Abel → G ∈ CMnd
8 2 7 syl ⊢ φ → G ∈ CMnd
9 subgsubm ⊢ S ∈ SubGrp ⁡ G → S ∈ SubMnd ⁡ G
10 4 9 syl ⊢ φ → S ∈ SubMnd ⁡ G
11 1 8 3 10 5 6 gsumsubmcl ⊢ φ → ∑ G F ∈ S