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 
|- ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) -> ( G gsum W ) e. S )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( W = (/) -> ( G gsum W ) = ( G gsum (/) ) )
2 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
3 2 gsum0 
 |-  ( G gsum (/) ) = ( 0g ` G )
4 1 3 eqtrdi 
 |-  ( W = (/) -> ( G gsum W ) = ( 0g ` G ) )
5 4 eleq1d 
 |-  ( W = (/) -> ( ( G gsum W ) e. S <-> ( 0g ` G ) e. S ) )
6 eqid 
 |-  ( Base ` G ) = ( Base ` G )
7 eqid 
 |-  ( +g ` G ) = ( +g ` G )
8 submrcl 
 |-  ( S e. ( SubMnd ` G ) -> G e. Mnd )
9 8 ad2antrr 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> G e. Mnd )
10 lennncl 
 |-  ( ( W e. Word S /\ W =/= (/) ) -> ( # ` W ) e. NN )
11 10 adantll 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> ( # ` W ) e. NN )
12 nnm1nn0 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. NN0 )
13 11 12 syl 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. NN0 )
14 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
15 13 14 eleqtrdi 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) )
16 wrdf 
 |-  ( W e. Word S -> W : ( 0 ..^ ( # ` W ) ) --> S )
17 16 ad2antlr 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> W : ( 0 ..^ ( # ` W ) ) --> S )
18 11 nnzd 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> ( # ` W ) e. ZZ )
19 fzoval 
 |-  ( ( # ` W ) e. ZZ -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
20 18 19 syl 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
21 20 feq2d 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> ( W : ( 0 ..^ ( # ` W ) ) --> S <-> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> S ) )
22 17 21 mpbid 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> S )
23 6 submss 
 |-  ( S e. ( SubMnd ` G ) -> S C_ ( Base ` G ) )
24 23 ad2antrr 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> S C_ ( Base ` G ) )
25 22 24 fssd 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> ( Base ` G ) )
26 6 7 9 15 25 gsumval2 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> ( G gsum W ) = ( seq 0 ( ( +g ` G ) , W ) ` ( ( # ` W ) - 1 ) ) )
27 22 ffvelcdmda 
 |-  ( ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> ( W ` x ) e. S )
28 7 submcl 
 |-  ( ( S e. ( SubMnd ` G ) /\ x e. S /\ y e. S ) -> ( x ( +g ` G ) y ) e. S )
29 28 3expb 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( x e. S /\ y e. S ) ) -> ( x ( +g ` G ) y ) e. S )
30 29 ad4ant14 
 |-  ( ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) /\ ( x e. S /\ y e. S ) ) -> ( x ( +g ` G ) y ) e. S )
31 15 27 30 seqcl 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> ( seq 0 ( ( +g ` G ) , W ) ` ( ( # ` W ) - 1 ) ) e. S )
32 26 31 eqeltrd 
 |-  ( ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) /\ W =/= (/) ) -> ( G gsum W ) e. S )
33 2 subm0cl 
 |-  ( S e. ( SubMnd ` G ) -> ( 0g ` G ) e. S )
34 33 adantr 
 |-  ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) -> ( 0g ` G ) e. S )
35 5 32 34 pm2.61ne 
 |-  ( ( S e. ( SubMnd ` G ) /\ W e. Word S ) -> ( G gsum W ) e. S )