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

Metamath Proof Explorer

Theorem gsummptcl

Description: Closure of a finite group sum over a finite set as map. (Contributed by AV, 29-Dec-2018)

Ref Expression
Hypotheses gsummptcl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptcl.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummptcl.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
gsummptcl.e ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐵 )
Assertion gsummptcl ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ 𝑁 ↦ 𝑋 ) ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 gsummptcl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptcl.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
3 gsummptcl.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
4 gsummptcl.e ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐵 )
5 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6 eqid ⊢ ( 𝑖 ∈ 𝑁 ↦ 𝑋 ) = ( 𝑖 ∈ 𝑁 ↦ 𝑋 )
7 6 fmpt ⊢ ( ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐵 ↔ ( 𝑖 ∈ 𝑁 ↦ 𝑋 ) : 𝑁 ⟶ 𝐵 )
8 4 7 sylib ⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 ↦ 𝑋 ) : 𝑁 ⟶ 𝐵 )
9 6 fnmpt ⊢ ( ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐵 → ( 𝑖 ∈ 𝑁 ↦ 𝑋 ) Fn 𝑁 )
10 4 9 syl ⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 ↦ 𝑋 ) Fn 𝑁 )
11 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ V )
12 10 3 11 fndmfifsupp ⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 ↦ 𝑋 ) finSupp ( 0g ‘ 𝐺 ) )
13 1 5 2 3 8 12 gsumcl ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ 𝑁 ↦ 𝑋 ) ) ∈ 𝐵 )