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

Metamath Proof Explorer

Theorem gsumzcl

Description: Closure of a finite group sum. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 1-Jun-2019)

Ref Expression
Hypotheses gsumzcl.b ⊢ B = Base G
gsumzcl.0 ⊢ 0 ˙ = 0 G
gsumzcl.z ⊢ Z = Cntz ⁡ G
gsumzcl.g ⊢ φ → G ∈ Mnd
gsumzcl.a ⊢ φ → A ∈ V
gsumzcl.f ⊢ φ → F : A ⟶ B
gsumzcl.c ⊢ φ → ran ⁡ F ⊆ Z ⁡ ran ⁡ F
gsumzcl.w ⊢ φ → finSupp 0 ˙⁡ F
Assertion gsumzcl ⊢ φ → ∑ G F ∈ B

Proof

Step Hyp Ref Expression
1 gsumzcl.b ⊢ B = Base G
2 gsumzcl.0 ⊢ 0 ˙ = 0 G
3 gsumzcl.z ⊢ Z = Cntz ⁡ G
4 gsumzcl.g ⊢ φ → G ∈ Mnd
5 gsumzcl.a ⊢ φ → A ∈ V
6 gsumzcl.f ⊢ φ → F : A ⟶ B
7 gsumzcl.c ⊢ φ → ran ⁡ F ⊆ Z ⁡ ran ⁡ F
8 gsumzcl.w ⊢ φ → finSupp 0 ˙⁡ F
9 8 fsuppimpd ⊢ φ → F supp 0 ˙ ∈ Fin
10 1 2 3 4 5 6 7 9 gsumzcl2 ⊢ φ → ∑ G F ∈ B