Metamath Proof Explorer

Theorem gsumwspan

Description: The submonoid generated by a set of elements is precisely the set of elements which can be expressed as finite products of the generator. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses gsumwspan.b 
|- B = ( Base ` M )
gsumwspan.k 
|- K = ( mrCls ` ( SubMnd ` M ) )
Assertion gsumwspan 
|- ( ( M e. Mnd /\ G C_ B ) -> ( K ` G ) = ran ( w e. Word G |-> ( M gsum w ) ) )

Proof

Step Hyp Ref Expression
1 gsumwspan.b 
 |-  B = ( Base ` M )
2 gsumwspan.k 
 |-  K = ( mrCls ` ( SubMnd ` M ) )
3 1 submacs 
 |-  ( M e. Mnd -> ( SubMnd ` M ) e. ( ACS ` B ) )
4 3 acsmred 
 |-  ( M e. Mnd -> ( SubMnd ` M ) e. ( Moore ` B ) )
5 4 adantr 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ( SubMnd ` M ) e. ( Moore ` B ) )
6 simpr 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ x e. G ) -> x e. G )
7 6 s1cld 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ x e. G ) -> <" x "> e. Word G )
8 ssel2 
 |-  ( ( G C_ B /\ x e. G ) -> x e. B )
9 8 adantll 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ x e. G ) -> x e. B )
10 1 gsumws1 
 |-  ( x e. B -> ( M gsum <" x "> ) = x )
11 9 10 syl 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ x e. G ) -> ( M gsum <" x "> ) = x )
12 11 eqcomd 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ x e. G ) -> x = ( M gsum <" x "> ) )
13 oveq2 
 |-  ( w = <" x "> -> ( M gsum w ) = ( M gsum <" x "> ) )
14 13 rspceeqv 
 |-  ( ( <" x "> e. Word G /\ x = ( M gsum <" x "> ) ) -> E. w e. Word G x = ( M gsum w ) )
15 7 12 14 syl2anc 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ x e. G ) -> E. w e. Word G x = ( M gsum w ) )
16 eqid 
 |-  ( w e. Word G |-> ( M gsum w ) ) = ( w e. Word G |-> ( M gsum w ) )
17 16 elrnmpt 
 |-  ( x e. _V -> ( x e. ran ( w e. Word G |-> ( M gsum w ) ) <-> E. w e. Word G x = ( M gsum w ) ) )
18 17 elv 
 |-  ( x e. ran ( w e. Word G |-> ( M gsum w ) ) <-> E. w e. Word G x = ( M gsum w ) )
19 15 18 sylibr 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ x e. G ) -> x e. ran ( w e. Word G |-> ( M gsum w ) ) )
20 19 ex 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ( x e. G -> x e. ran ( w e. Word G |-> ( M gsum w ) ) ) )
21 20 ssrdv 
 |-  ( ( M e. Mnd /\ G C_ B ) -> G C_ ran ( w e. Word G |-> ( M gsum w ) ) )
22 2 mrccl 
 |-  ( ( ( SubMnd ` M ) e. ( Moore ` B ) /\ G C_ B ) -> ( K ` G ) e. ( SubMnd ` M ) )
23 4 22 sylan 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ( K ` G ) e. ( SubMnd ` M ) )
24 2 mrcssid 
 |-  ( ( ( SubMnd ` M ) e. ( Moore ` B ) /\ G C_ B ) -> G C_ ( K ` G ) )
25 4 24 sylan 
 |-  ( ( M e. Mnd /\ G C_ B ) -> G C_ ( K ` G ) )
26 sswrd 
 |-  ( G C_ ( K ` G ) -> Word G C_ Word ( K ` G ) )
27 25 26 syl 
 |-  ( ( M e. Mnd /\ G C_ B ) -> Word G C_ Word ( K ` G ) )
28 27 sselda 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ w e. Word G ) -> w e. Word ( K ` G ) )
29 gsumwsubmcl 
 |-  ( ( ( K ` G ) e. ( SubMnd ` M ) /\ w e. Word ( K ` G ) ) -> ( M gsum w ) e. ( K ` G ) )
30 23 28 29 syl2an2r 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ w e. Word G ) -> ( M gsum w ) e. ( K ` G ) )
31 30 fmpttd 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ( w e. Word G |-> ( M gsum w ) ) : Word G --> ( K ` G ) )
32 31 frnd 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ran ( w e. Word G |-> ( M gsum w ) ) C_ ( K ` G ) )
33 4 2 mrcssvd 
 |-  ( M e. Mnd -> ( K ` G ) C_ B )
34 33 adantr 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ( K ` G ) C_ B )
35 32 34 sstrd 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ran ( w e. Word G |-> ( M gsum w ) ) C_ B )
36 wrd0 
 |-  (/) e. Word G
37 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
38 37 gsum0 
 |-  ( M gsum (/) ) = ( 0g ` M )
39 38 eqcomi 
 |-  ( 0g ` M ) = ( M gsum (/) )
40 39 a1i 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ( 0g ` M ) = ( M gsum (/) ) )
41 oveq2 
 |-  ( w = (/) -> ( M gsum w ) = ( M gsum (/) ) )
42 41 rspceeqv 
 |-  ( ( (/) e. Word G /\ ( 0g ` M ) = ( M gsum (/) ) ) -> E. w e. Word G ( 0g ` M ) = ( M gsum w ) )
43 36 40 42 sylancr 
 |-  ( ( M e. Mnd /\ G C_ B ) -> E. w e. Word G ( 0g ` M ) = ( M gsum w ) )
44 fvex 
 |-  ( 0g ` M ) e. _V
45 16 elrnmpt 
 |-  ( ( 0g ` M ) e. _V -> ( ( 0g ` M ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> E. w e. Word G ( 0g ` M ) = ( M gsum w ) ) )
46 44 45 ax-mp 
 |-  ( ( 0g ` M ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> E. w e. Word G ( 0g ` M ) = ( M gsum w ) )
47 43 46 sylibr 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ( 0g ` M ) e. ran ( w e. Word G |-> ( M gsum w ) ) )
48 ccatcl 
 |-  ( ( z e. Word G /\ v e. Word G ) -> ( z ++ v ) e. Word G )
49 simpll 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ ( z e. Word G /\ v e. Word G ) ) -> M e. Mnd )
50 sswrd 
 |-  ( G C_ B -> Word G C_ Word B )
51 50 ad2antlr 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ ( z e. Word G /\ v e. Word G ) ) -> Word G C_ Word B )
52 simprl 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ ( z e. Word G /\ v e. Word G ) ) -> z e. Word G )
53 51 52 sseldd 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ ( z e. Word G /\ v e. Word G ) ) -> z e. Word B )
54 simprr 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ ( z e. Word G /\ v e. Word G ) ) -> v e. Word G )
55 51 54 sseldd 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ ( z e. Word G /\ v e. Word G ) ) -> v e. Word B )
56 eqid 
 |-  ( +g ` M ) = ( +g ` M )
57 1 56 gsumccat 
 |-  ( ( M e. Mnd /\ z e. Word B /\ v e. Word B ) -> ( M gsum ( z ++ v ) ) = ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) )
58 49 53 55 57 syl3anc 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ ( z e. Word G /\ v e. Word G ) ) -> ( M gsum ( z ++ v ) ) = ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) )
59 58 eqcomd 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ ( z e. Word G /\ v e. Word G ) ) -> ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) = ( M gsum ( z ++ v ) ) )
60 oveq2 
 |-  ( w = ( z ++ v ) -> ( M gsum w ) = ( M gsum ( z ++ v ) ) )
61 60 rspceeqv 
 |-  ( ( ( z ++ v ) e. Word G /\ ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) = ( M gsum ( z ++ v ) ) ) -> E. w e. Word G ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) = ( M gsum w ) )
62 48 59 61 syl2an2 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ ( z e. Word G /\ v e. Word G ) ) -> E. w e. Word G ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) = ( M gsum w ) )
63 ovex 
 |-  ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) e. _V
64 16 elrnmpt 
 |-  ( ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) e. _V -> ( ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> E. w e. Word G ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) = ( M gsum w ) ) )
65 63 64 ax-mp 
 |-  ( ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> E. w e. Word G ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) = ( M gsum w ) )
66 62 65 sylibr 
 |-  ( ( ( M e. Mnd /\ G C_ B ) /\ ( z e. Word G /\ v e. Word G ) ) -> ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) )
67 66 ralrimivva 
 |-  ( ( M e. Mnd /\ G C_ B ) -> A. z e. Word G A. v e. Word G ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) )
68 oveq2 
 |-  ( w = z -> ( M gsum w ) = ( M gsum z ) )
69 68 cbvmptv 
 |-  ( w e. Word G |-> ( M gsum w ) ) = ( z e. Word G |-> ( M gsum z ) )
70 69 rneqi 
 |-  ran ( w e. Word G |-> ( M gsum w ) ) = ran ( z e. Word G |-> ( M gsum z ) )
71 70 raleqi 
 |-  ( A. x e. ran ( w e. Word G |-> ( M gsum w ) ) A. y e. ran ( w e. Word G |-> ( M gsum w ) ) ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> A. x e. ran ( z e. Word G |-> ( M gsum z ) ) A. y e. ran ( w e. Word G |-> ( M gsum w ) ) ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) )
72 oveq2 
 |-  ( w = v -> ( M gsum w ) = ( M gsum v ) )
73 72 cbvmptv 
 |-  ( w e. Word G |-> ( M gsum w ) ) = ( v e. Word G |-> ( M gsum v ) )
74 73 rneqi 
 |-  ran ( w e. Word G |-> ( M gsum w ) ) = ran ( v e. Word G |-> ( M gsum v ) )
75 74 raleqi 
 |-  ( A. y e. ran ( w e. Word G |-> ( M gsum w ) ) ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> A. y e. ran ( v e. Word G |-> ( M gsum v ) ) ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) )
76 eqid 
 |-  ( v e. Word G |-> ( M gsum v ) ) = ( v e. Word G |-> ( M gsum v ) )
77 oveq2 
 |-  ( y = ( M gsum v ) -> ( x ( +g ` M ) y ) = ( x ( +g ` M ) ( M gsum v ) ) )
78 77 eleq1d 
 |-  ( y = ( M gsum v ) -> ( ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> ( x ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) ) )
79 76 78 ralrnmptw 
 |-  ( A. v e. Word G ( M gsum v ) e. _V -> ( A. y e. ran ( v e. Word G |-> ( M gsum v ) ) ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> A. v e. Word G ( x ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) ) )
80 ovexd 
 |-  ( v e. Word G -> ( M gsum v ) e. _V )
81 79 80 mprg 
 |-  ( A. y e. ran ( v e. Word G |-> ( M gsum v ) ) ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> A. v e. Word G ( x ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) )
82 75 81 bitri 
 |-  ( A. y e. ran ( w e. Word G |-> ( M gsum w ) ) ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> A. v e. Word G ( x ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) )
83 82 ralbii 
 |-  ( A. x e. ran ( z e. Word G |-> ( M gsum z ) ) A. y e. ran ( w e. Word G |-> ( M gsum w ) ) ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> A. x e. ran ( z e. Word G |-> ( M gsum z ) ) A. v e. Word G ( x ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) )
84 eqid 
 |-  ( z e. Word G |-> ( M gsum z ) ) = ( z e. Word G |-> ( M gsum z ) )
85 oveq1 
 |-  ( x = ( M gsum z ) -> ( x ( +g ` M ) ( M gsum v ) ) = ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) )
86 85 eleq1d 
 |-  ( x = ( M gsum z ) -> ( ( x ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) ) )
87 86 ralbidv 
 |-  ( x = ( M gsum z ) -> ( A. v e. Word G ( x ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> A. v e. Word G ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) ) )
88 84 87 ralrnmptw 
 |-  ( A. z e. Word G ( M gsum z ) e. _V -> ( A. x e. ran ( z e. Word G |-> ( M gsum z ) ) A. v e. Word G ( x ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> A. z e. Word G A. v e. Word G ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) ) )
89 ovexd 
 |-  ( z e. Word G -> ( M gsum z ) e. _V )
90 88 89 mprg 
 |-  ( A. x e. ran ( z e. Word G |-> ( M gsum z ) ) A. v e. Word G ( x ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> A. z e. Word G A. v e. Word G ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) )
91 71 83 90 3bitri 
 |-  ( A. x e. ran ( w e. Word G |-> ( M gsum w ) ) A. y e. ran ( w e. Word G |-> ( M gsum w ) ) ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) <-> A. z e. Word G A. v e. Word G ( ( M gsum z ) ( +g ` M ) ( M gsum v ) ) e. ran ( w e. Word G |-> ( M gsum w ) ) )
92 67 91 sylibr 
 |-  ( ( M e. Mnd /\ G C_ B ) -> A. x e. ran ( w e. Word G |-> ( M gsum w ) ) A. y e. ran ( w e. Word G |-> ( M gsum w ) ) ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) )
93 1 37 56 issubm 
 |-  ( M e. Mnd -> ( ran ( w e. Word G |-> ( M gsum w ) ) e. ( SubMnd ` M ) <-> ( ran ( w e. Word G |-> ( M gsum w ) ) C_ B /\ ( 0g ` M ) e. ran ( w e. Word G |-> ( M gsum w ) ) /\ A. x e. ran ( w e. Word G |-> ( M gsum w ) ) A. y e. ran ( w e. Word G |-> ( M gsum w ) ) ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) ) ) )
94 93 adantr 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ( ran ( w e. Word G |-> ( M gsum w ) ) e. ( SubMnd ` M ) <-> ( ran ( w e. Word G |-> ( M gsum w ) ) C_ B /\ ( 0g ` M ) e. ran ( w e. Word G |-> ( M gsum w ) ) /\ A. x e. ran ( w e. Word G |-> ( M gsum w ) ) A. y e. ran ( w e. Word G |-> ( M gsum w ) ) ( x ( +g ` M ) y ) e. ran ( w e. Word G |-> ( M gsum w ) ) ) ) )
95 35 47 92 94 mpbir3and 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ran ( w e. Word G |-> ( M gsum w ) ) e. ( SubMnd ` M ) )
96 2 mrcsscl 
 |-  ( ( ( SubMnd ` M ) e. ( Moore ` B ) /\ G C_ ran ( w e. Word G |-> ( M gsum w ) ) /\ ran ( w e. Word G |-> ( M gsum w ) ) e. ( SubMnd ` M ) ) -> ( K ` G ) C_ ran ( w e. Word G |-> ( M gsum w ) ) )
97 5 21 95 96 syl3anc 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ( K ` G ) C_ ran ( w e. Word G |-> ( M gsum w ) ) )
98 97 32 eqssd 
 |-  ( ( M e. Mnd /\ G C_ B ) -> ( K ` G ) = ran ( w e. Word G |-> ( M gsum w ) ) )