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 𝐵 = ( Base ‘ 𝑀 )
gsumwspan.k 𝐾 = ( mrCls ‘ ( SubMnd ‘ 𝑀 ) )
Assertion gsumwspan ( ( 𝑀 ∈ Mnd ∧ 𝐺𝐵 ) → ( 𝐾𝐺 ) = ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) )

Proof

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