Theorem gsumwsubmcl

Description: Closure of the composite in any submonoid. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 1-Oct-2015)

	Ref	Expression
Assertion	gsumwsubmcl	⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) → ( 𝐺 Σg 𝑊 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑊 = ∅ → ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg ∅ ) )
2		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
3	2	gsum0	⊢ ( 𝐺 Σg ∅ ) = ( 0g ‘ 𝐺 )
4	1 3	eqtrdi	⊢ ( 𝑊 = ∅ → ( 𝐺 Σg 𝑊 ) = ( 0g ‘ 𝐺 ) )
5	4	eleq1d	⊢ ( 𝑊 = ∅ → ( ( 𝐺 Σg 𝑊 ) ∈ 𝑆 ↔ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) )
6		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
8		submrcl	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝐺 ∈ Mnd )
9	8	ad2antrr	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → 𝐺 ∈ Mnd )
10		lennncl	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
11	10	adantll	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
12		nnm1nn0	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 )
13	11 12	syl	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 )
14		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
15	13 14	eleqtrdi	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
16		wrdf	⊢ ( 𝑊 ∈ Word 𝑆 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
17	16	ad2antlr	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
18	11	nnzd	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
19		fzoval	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
20	18 19	syl	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
21	20	feq2d	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 ↔ 𝑊 : ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ⟶ 𝑆 ) )
22	17 21	mpbid	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → 𝑊 : ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ⟶ 𝑆 )
23	6	submss	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
24	23	ad2antrr	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
25	22 24	fssd	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → 𝑊 : ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ⟶ ( Base ‘ 𝐺 ) )
26	6 7 9 15 25	gsumval2	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → ( 𝐺 Σg 𝑊 ) = ( seq 0 ( ( +g ‘ 𝐺 ) , 𝑊 ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
27	22	ffvelrnda	⊢ ( ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) ∧ 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 𝑊 ‘ 𝑥 ) ∈ 𝑆 )
28	7	submcl	⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
29	28	3expb	⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
30	29	ad4ant14	⊢ ( ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
31	15 27 30	seqcl	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → ( seq 0 ( ( +g ‘ 𝐺 ) , 𝑊 ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ 𝑆 )
32	26 31	eqeltrd	⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) ∧ 𝑊 ≠ ∅ ) → ( 𝐺 Σg 𝑊 ) ∈ 𝑆 )
33	2	subm0cl	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
34	33	adantr	⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
35	5 32 34	pm2.61ne	⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝑆 ) → ( 𝐺 Σg 𝑊 ) ∈ 𝑆 )