Theorem gsumncl

Description: Closure of a group sum in a non-commutative monoid. (Contributed by Thierry Arnoux, 8-Oct-2018)

	Ref	Expression
Hypotheses	gsumncl.k	⊢ 𝐾 = ( Base ‘ 𝑀 )
	gsumncl.w	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
	gsumncl.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ 𝑁 ) )
	gsumncl.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑁 ... 𝑃 ) ) → 𝐵 ∈ 𝐾 )
Assertion	gsumncl	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		gsumncl.k	⊢ 𝐾 = ( Base ‘ 𝑀 )
2		gsumncl.w	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3		gsumncl.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ 𝑁 ) )
4		gsumncl.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑁 ... 𝑃 ) ) → 𝐵 ∈ 𝐾 )
5		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
6	4	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) : ( 𝑁 ... 𝑃 ) ⟶ 𝐾 )
7	1 5 2 3 6	gsumval2	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) = ( seq 𝑁 ( ( +g ‘ 𝑀 ) , ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) ‘ 𝑃 ) )
8	6	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ... 𝑃 ) ) → ( ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ‘ 𝑥 ) ∈ 𝐾 )
9	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑀 ∈ Mnd )
10		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑥 ∈ 𝐾 )
11		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑦 ∈ 𝐾 )
12	1 5	mndcl	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐾 )
13	9 10 11 12	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐾 )
14	3 8 13	seqcl	⊢ ( 𝜑 → ( seq 𝑁 ( ( +g ‘ 𝑀 ) , ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) ‘ 𝑃 ) ∈ 𝐾 )
15	7 14	eqeltrd	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) ∈ 𝐾 )