gsumwspan - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > gsumwspan		Structured version Visualization version GIF version

Theorem gsumwspan 18724

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

**Hypotheses**
Ref	Expression
gsumwspan.b	⊢ 𝐵 = (Base‘𝑀)
gsumwspan.k	⊢ 𝐾 = (mrCls‘(SubMnd‘𝑀))

**Assertion**
Ref	Expression
gsumwspan	⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) = ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))

Distinct variable groups: 𝑤,𝐺 𝑤,𝐵 𝑤,𝑀 𝑤,𝐾

Proof of Theorem gsumwspan Dummy variables 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumwspan.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝑀)
2	1	submacs 18705	. . . . 5 ⊢ (𝑀 ∈ Mnd → (SubMnd‘𝑀) ∈ (ACS‘𝐵))
3	2	acsmred 17597	. . . 4 ⊢ (𝑀 ∈ Mnd → (SubMnd‘𝑀) ∈ (Moore‘𝐵))
4	3	adantr 482	. . 3 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (SubMnd‘𝑀) ∈ (Moore‘𝐵))
5		simpr 486	. . . . . . . 8 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐺)
6	5	s1cld 14550	. . . . . . 7 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → ⟨“𝑥”⟩ ∈ Word 𝐺)
7		ssel2 3977	. . . . . . . . . 10 ⊢ ((𝐺 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐵)
8	7	adantll 713	. . . . . . . . 9 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐵)
9	1	gsumws1 18716	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐵 → (𝑀 Σ_g ⟨“𝑥”⟩) = 𝑥)
10	8, 9	syl 17	. . . . . . . 8 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → (𝑀 Σ_g ⟨“𝑥”⟩) = 𝑥)
11	10	eqcomd 2739	. . . . . . 7 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 = (𝑀 Σ_g ⟨“𝑥”⟩))
12		oveq2 7414	. . . . . . . 8 ⊢ (𝑤 = ⟨“𝑥”⟩ → (𝑀 Σ_g 𝑤) = (𝑀 Σ_g ⟨“𝑥”⟩))
13	12	rspceeqv 3633	. . . . . . 7 ⊢ ((⟨“𝑥”⟩ ∈ Word 𝐺 ∧ 𝑥 = (𝑀 Σ_g ⟨“𝑥”⟩)) → ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σ_g 𝑤))
14	6, 11, 13	syl2anc 585	. . . . . 6 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σ_g 𝑤))
15		eqid 2733	. . . . . . . 8 ⊢ (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) = (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))
16	15	elrnmpt 5954	. . . . . . 7 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σ_g 𝑤)))
17	16	elv 3481	. . . . . 6 ⊢ (𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σ_g 𝑤))
18	14, 17	sylibr 233	. . . . 5 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
19	18	ex 414	. . . 4 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝑥 ∈ 𝐺 → 𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))))
20	19	ssrdv 3988	. . 3 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
21		gsumwspan.k	. . . . . . . . . 10 ⊢ 𝐾 = (mrCls‘(SubMnd‘𝑀))
22	21	mrccl 17552	. . . . . . . . 9 ⊢ (((SubMnd‘𝑀) ∈ (Moore‘𝐵) ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ∈ (SubMnd‘𝑀))
23	3, 22	sylan 581	. . . . . . . 8 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ∈ (SubMnd‘𝑀))
24	21	mrcssid 17558	. . . . . . . . . . 11 ⊢ (((SubMnd‘𝑀) ∈ (Moore‘𝐵) ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺))
25	3, 24	sylan 581	. . . . . . . . . 10 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺))
26		sswrd 14469	. . . . . . . . . 10 ⊢ (𝐺 ⊆ (𝐾‘𝐺) → Word 𝐺 ⊆ Word (𝐾‘𝐺))
27	25, 26	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → Word 𝐺 ⊆ Word (𝐾‘𝐺))
28	27	sselda 3982	. . . . . . . 8 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑤 ∈ Word 𝐺) → 𝑤 ∈ Word (𝐾‘𝐺))
29		gsumwsubmcl 18715	. . . . . . . 8 ⊢ (((𝐾‘𝐺) ∈ (SubMnd‘𝑀) ∧ 𝑤 ∈ Word (𝐾‘𝐺)) → (𝑀 Σ_g 𝑤) ∈ (𝐾‘𝐺))
30	23, 28, 29	syl2an2r 684	. . . . . . 7 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑤 ∈ Word 𝐺) → (𝑀 Σ_g 𝑤) ∈ (𝐾‘𝐺))
31	30	fmpttd 7112	. . . . . 6 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)):Word 𝐺⟶(𝐾‘𝐺))
32	31	frnd 6723	. . . . 5 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ⊆ (𝐾‘𝐺))
33	3, 21	mrcssvd 17564	. . . . . 6 ⊢ (𝑀 ∈ Mnd → (𝐾‘𝐺) ⊆ 𝐵)
34	33	adantr 482	. . . . 5 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ⊆ 𝐵)
35	32, 34	sstrd 3992	. . . 4 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ⊆ 𝐵)
36		wrd0 14486	. . . . . 6 ⊢ ∅ ∈ Word 𝐺
37		eqid 2733	. . . . . . . . 9 ⊢ (0_g‘𝑀) = (0_g‘𝑀)
38	37	gsum0 18600	. . . . . . . 8 ⊢ (𝑀 Σ_g ∅) = (0_g‘𝑀)
39	38	eqcomi 2742	. . . . . . 7 ⊢ (0_g‘𝑀) = (𝑀 Σ_g ∅)
40	39	a1i 11	. . . . . 6 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (0_g‘𝑀) = (𝑀 Σ_g ∅))
41		oveq2 7414	. . . . . . 7 ⊢ (𝑤 = ∅ → (𝑀 Σ_g 𝑤) = (𝑀 Σ_g ∅))
42	41	rspceeqv 3633	. . . . . 6 ⊢ ((∅ ∈ Word 𝐺 ∧ (0_g‘𝑀) = (𝑀 Σ_g ∅)) → ∃𝑤 ∈ Word 𝐺(0_g‘𝑀) = (𝑀 Σ_g 𝑤))
43	36, 40, 42	sylancr 588	. . . . 5 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ∃𝑤 ∈ Word 𝐺(0_g‘𝑀) = (𝑀 Σ_g 𝑤))
44		fvex 6902	. . . . . 6 ⊢ (0_g‘𝑀) ∈ V
45	15	elrnmpt 5954	. . . . . 6 ⊢ ((0_g‘𝑀) ∈ V → ((0_g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺(0_g‘𝑀) = (𝑀 Σ_g 𝑤)))
46	44, 45	ax-mp 5	. . . . 5 ⊢ ((0_g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺(0_g‘𝑀) = (𝑀 Σ_g 𝑤))
47	43, 46	sylibr 233	. . . 4 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (0_g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
48		ccatcl 14521	. . . . . . . 8 ⊢ ((𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺) → (𝑧 ++ 𝑣) ∈ Word 𝐺)
49		simpll 766	. . . . . . . . . 10 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑀 ∈ Mnd)
50		sswrd 14469	. . . . . . . . . . . 12 ⊢ (𝐺 ⊆ 𝐵 → Word 𝐺 ⊆ Word 𝐵)
51	50	ad2antlr 726	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → Word 𝐺 ⊆ Word 𝐵)
52		simprl 770	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑧 ∈ Word 𝐺)
53	51, 52	sseldd 3983	. . . . . . . . . 10 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑧 ∈ Word 𝐵)
54		simprr 772	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑣 ∈ Word 𝐺)
55	51, 54	sseldd 3983	. . . . . . . . . 10 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑣 ∈ Word 𝐵)
56		eqid 2733	. . . . . . . . . . 11 ⊢ (+_g‘𝑀) = (+_g‘𝑀)
57	1, 56	gsumccat 18719	. . . . . . . . . 10 ⊢ ((𝑀 ∈ Mnd ∧ 𝑧 ∈ Word 𝐵 ∧ 𝑣 ∈ Word 𝐵) → (𝑀 Σ_g (𝑧 ++ 𝑣)) = ((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)))
58	49, 53, 55, 57	syl3anc 1372	. . . . . . . . 9 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → (𝑀 Σ_g (𝑧 ++ 𝑣)) = ((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)))
59	58	eqcomd 2739	. . . . . . . 8 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → ((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) = (𝑀 Σ_g (𝑧 ++ 𝑣)))
60		oveq2 7414	. . . . . . . . 9 ⊢ (𝑤 = (𝑧 ++ 𝑣) → (𝑀 Σ_g 𝑤) = (𝑀 Σ_g (𝑧 ++ 𝑣)))
61	60	rspceeqv 3633	. . . . . . . 8 ⊢ (((𝑧 ++ 𝑣) ∈ Word 𝐺 ∧ ((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) = (𝑀 Σ_g (𝑧 ++ 𝑣))) → ∃𝑤 ∈ Word 𝐺((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) = (𝑀 Σ_g 𝑤))
62	48, 59, 61	syl2an2 685	. . . . . . 7 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → ∃𝑤 ∈ Word 𝐺((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) = (𝑀 Σ_g 𝑤))
63		ovex 7439	. . . . . . . 8 ⊢ ((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ V
64	15	elrnmpt 5954	. . . . . . . 8 ⊢ (((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ V → (((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) = (𝑀 Σ_g 𝑤)))
65	63, 64	ax-mp 5	. . . . . . 7 ⊢ (((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) = (𝑀 Σ_g 𝑤))
66	62, 65	sylibr 233	. . . . . 6 ⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → ((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
67	66	ralrimivva 3201	. . . . 5 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
68		oveq2 7414	. . . . . . . . 9 ⊢ (𝑤 = 𝑧 → (𝑀 Σ_g 𝑤) = (𝑀 Σ_g 𝑧))
69	68	cbvmptv 5261	. . . . . . . 8 ⊢ (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) = (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑧))
70	69	rneqi 5935	. . . . . . 7 ⊢ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) = ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑧))
71	70	raleqi 3324	. . . . . 6 ⊢ (∀𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))(𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑧))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))(𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
72		oveq2 7414	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑣 → (𝑀 Σ_g 𝑤) = (𝑀 Σ_g 𝑣))
73	72	cbvmptv 5261	. . . . . . . . . 10 ⊢ (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) = (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑣))
74	73	rneqi 5935	. . . . . . . . 9 ⊢ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) = ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑣))
75	74	raleqi 3324	. . . . . . . 8 ⊢ (∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))(𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∀𝑦 ∈ ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑣))(𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
76		eqid 2733	. . . . . . . . . 10 ⊢ (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑣)) = (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑣))
77		oveq2 7414	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑀 Σ_g 𝑣) → (𝑥(+_g‘𝑀)𝑦) = (𝑥(+_g‘𝑀)(𝑀 Σ_g 𝑣)))
78	77	eleq1d 2819	. . . . . . . . . 10 ⊢ (𝑦 = (𝑀 Σ_g 𝑣) → ((𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ (𝑥(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))))
79	76, 78	ralrnmptw 7093	. . . . . . . . 9 ⊢ (∀𝑣 ∈ Word 𝐺(𝑀 Σ_g 𝑣) ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑣))(𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺(𝑥(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))))
80		ovexd 7441	. . . . . . . . 9 ⊢ (𝑣 ∈ Word 𝐺 → (𝑀 Σ_g 𝑣) ∈ V)
81	79, 80	mprg 3068	. . . . . . . 8 ⊢ (∀𝑦 ∈ ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑣))(𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺(𝑥(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
82	75, 81	bitri 275	. . . . . . 7 ⊢ (∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))(𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺(𝑥(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
83	82	ralbii 3094	. . . . . 6 ⊢ (∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑧))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))(𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑧))∀𝑣 ∈ Word 𝐺(𝑥(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
84		eqid 2733	. . . . . . . 8 ⊢ (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑧)) = (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑧))
85		oveq1 7413	. . . . . . . . . 10 ⊢ (𝑥 = (𝑀 Σ_g 𝑧) → (𝑥(+_g‘𝑀)(𝑀 Σ_g 𝑣)) = ((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)))
86	85	eleq1d 2819	. . . . . . . . 9 ⊢ (𝑥 = (𝑀 Σ_g 𝑧) → ((𝑥(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))))
87	86	ralbidv 3178	. . . . . . . 8 ⊢ (𝑥 = (𝑀 Σ_g 𝑧) → (∀𝑣 ∈ Word 𝐺(𝑥(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))))
88	84, 87	ralrnmptw 7093	. . . . . . 7 ⊢ (∀𝑧 ∈ Word 𝐺(𝑀 Σ_g 𝑧) ∈ V → (∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑧))∀𝑣 ∈ Word 𝐺(𝑥(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))))
89		ovexd 7441	. . . . . . 7 ⊢ (𝑧 ∈ Word 𝐺 → (𝑀 Σ_g 𝑧) ∈ V)
90	88, 89	mprg 3068	. . . . . 6 ⊢ (∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑧))∀𝑣 ∈ Word 𝐺(𝑥(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
91	71, 83, 90	3bitri 297	. . . . 5 ⊢ (∀𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))(𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ↔ ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σ_g 𝑧)(+_g‘𝑀)(𝑀 Σ_g 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
92	67, 91	sylibr 233	. . . 4 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ∀𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))(𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
93	1, 37, 56	issubm 18681	. . . . 5 ⊢ (𝑀 ∈ Mnd → (ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ∈ (SubMnd‘𝑀) ↔ (ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ⊆ 𝐵 ∧ (0_g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ∧ ∀𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))(𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))))
94	93	adantr 482	. . . 4 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ∈ (SubMnd‘𝑀) ↔ (ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ⊆ 𝐵 ∧ (0_g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ∧ ∀𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤))(𝑥(+_g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))))
95	35, 47, 92, 94	mpbir3and 1343	. . 3 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ∈ (SubMnd‘𝑀))
96	21	mrcsscl 17561	. . 3 ⊢ (((SubMnd‘𝑀) ∈ (Moore‘𝐵) ∧ 𝐺 ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ∧ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)) ∈ (SubMnd‘𝑀)) → (𝐾‘𝐺) ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
97	4, 20, 95, 96	syl3anc 1372	. 2 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))
98	97, 32	eqssd 3999	1 ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) = ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σ_g 𝑤)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ∃wrex 3071 Vcvv 3475 ⊆ wss 3948 ∅c0 4322 ↦ cmpt 5231 ran crn 5677 ‘cfv 6541 (class class class)co 7406 Word cword 14461 ++ cconcat 14517 ⟨“cs1 14542 Basecbs 17141 +_gcplusg 17194 0_gc0g 17382 Σ_g cgsu 17383 Moorecmre 17523 mrClscmrc 17524 Mndcmnd 18622 SubMndcsubmnd 18667

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-om 7853 df-1st 7972 df-2nd 7973 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-er 8700 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-nn 12210 df-2 12272 df-n0 12470 df-z 12556 df-uz 12820 df-fz 13482 df-fzo 13625 df-seq 13964 df-hash 14288 df-word 14462 df-concat 14518 df-s1 14543 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-0g 17384 df-gsum 17385 df-mre 17527 df-mrc 17528 df-acs 17530 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-submnd 18669

This theorem is referenced by: psgneldm2 19367 psgnfitr 19380

W3C validator