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