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

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 𝑤 ) ) )