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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumzcl.0 ⊢ 0 = ( 0g ‘ 𝐺 )
gsumzcl.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
gsumzcl.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsumzcl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumzcl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumzcl.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
gsumzcl.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion gsumzcl ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 gsumzcl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumzcl.0 ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumzcl.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
4 gsumzcl.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
5 gsumzcl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 gsumzcl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 gsumzcl.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
8 gsumzcl.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
9 8 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
10 1 2 3 4 5 6 7 9 gsumzcl2 ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 )