Metamath Proof Explorer


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 𝑊 ) ∈ 𝑆 )