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 \in Mnd \land G \subseteq B) \to K (G) = ran (w \in Word G ⟼ \sum_{M} w)$

Proof

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

Metamath Proof Explorer

Theorem gsumwspan

Proof