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 Mnd G B K G = ran w Word G M w

Proof

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