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 ( 𝑖 ∈ 𝑁 ↦ 𝑋 ) ) ∈ 𝐵 )