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

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