frmdss2

Description: A subset of generators is contained in a submonoid iff the set of words on the generators is in the submonoid. This can be viewed as an elementary way of saying "the monoidal closure of J is Word J ". (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	frmdmnd.m	$⊢ M = freeMnd (I)$
	frmdgsum.u	$⊢ U = {var}_{FMnd} (I)$
Assertion	frmdss2	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to (U [J] \subseteq A \leftrightarrow Word J \subseteq A)$

Proof

Step	Hyp	Ref	Expression
1		frmdmnd.m	$⊢ M = freeMnd (I)$
2		frmdgsum.u	$⊢ U = {var}_{FMnd} (I)$
3		simpl1	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to I \in V$
4		simpl2	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to J \subseteq I$
5		sswrd	$⊢ J \subseteq I \to Word J \subseteq Word I$
6	4 5	syl	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to Word J \subseteq Word I$
7		simprr	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to x \in Word J$
8	6 7	sseldd	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to x \in Word I$
9	1 2	frmdgsum	$⊢ (I \in V \land x \in Word I) \to \sum_{M} (U \circ x) = x$
10	3 8 9	syl2anc	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to \sum_{M} (U \circ x) = x$
11		simpl3	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to A \in SubMnd (M)$
12		wrdf	$⊢ x \in Word J \to x : (0 ..^\|x\|) ⟶ J$
13	12	ad2antll	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to x : (0 ..^\|x\|) ⟶ J$
14	13	frnd	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to ran x \subseteq J$
15		cores	$⊢ ran x \subseteq J \to ({U ↾}_{J}) \circ x = U \circ x$
16	14 15	syl	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to ({U ↾}_{J}) \circ x = U \circ x$
17	2	vrmdf	$⊢ I \in V \to U : I ⟶ Word I$
18	17	3ad2ant1	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to U : I ⟶ Word I$
19	18	ffnd	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to U Fn I$
20		fnssres	$⊢ (U Fn I \land J \subseteq I) \to ({U ↾}_{J}) Fn J$
21	19 4 20	syl2an2r	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to ({U ↾}_{J}) Fn J$
22		df-ima	$⊢ U [J] = ran ({U ↾}_{J})$
23		simprl	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to U [J] \subseteq A$
24	22 23	eqsstrrid	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to ran ({U ↾}_{J}) \subseteq A$
25		df-f	$⊢ ({U ↾}_{J}) : J ⟶ A \leftrightarrow (({U ↾}_{J}) Fn J \land ran ({U ↾}_{J}) \subseteq A)$
26	21 24 25	sylanbrc	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to ({U ↾}_{J}) : J ⟶ A$
27		wrdco	$⊢ (x \in Word J \land ({U ↾}_{J}) : J ⟶ A) \to ({U ↾}_{J}) \circ x \in Word A$
28	7 26 27	syl2anc	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to ({U ↾}_{J}) \circ x \in Word A$
29	16 28	eqeltrrd	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to U \circ x \in Word A$
30		gsumwsubmcl	$⊢ (A \in SubMnd (M) \land U \circ x \in Word A) \to \sum_{M} (U \circ x) \in A$
31	11 29 30	syl2anc	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to \sum_{M} (U \circ x) \in A$
32	10 31	eqeltrrd	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land (U [J] \subseteq A \land x \in Word J)) \to x \in A$
33	32	expr	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land U [J] \subseteq A) \to (x \in Word J \to x \in A)$
34	33	ssrdv	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land U [J] \subseteq A) \to Word J \subseteq A$
35	34	ex	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to (U [J] \subseteq A \to Word J \subseteq A)$
36		simpl1	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land x \in J) \to I \in V$
37		simp2	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to J \subseteq I$
38	37	sselda	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land x \in J) \to x \in I$
39	2	vrmdval	$⊢ (I \in V \land x \in I) \to U (x) = ⟨“ x ”⟩$
40	36 38 39	syl2anc	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land x \in J) \to U (x) = ⟨“ x ”⟩$
41		simpr	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land x \in J) \to x \in J$
42	41	s1cld	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land x \in J) \to ⟨“ x ”⟩ \in Word J$
43	40 42	eqeltrd	$⊢ ((I \in V \land J \subseteq I \land A \in SubMnd (M)) \land x \in J) \to U (x) \in Word J$
44	43	ralrimiva	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to \forall x \in J U (x) \in Word J$
45	18	ffund	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to Fun U$
46	18	fdmd	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to dom U = I$
47	37 46	sseqtrrd	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to J \subseteq dom U$
48		funimass4	$⊢ (Fun U \land J \subseteq dom U) \to (U [J] \subseteq Word J \leftrightarrow \forall x \in J U (x) \in Word J)$
49	45 47 48	syl2anc	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to (U [J] \subseteq Word J \leftrightarrow \forall x \in J U (x) \in Word J)$
50	44 49	mpbird	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to U [J] \subseteq Word J$
51		sstr2	$⊢ U [J] \subseteq Word J \to (Word J \subseteq A \to U [J] \subseteq A)$
52	50 51	syl	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to (Word J \subseteq A \to U [J] \subseteq A)$
53	35 52	impbid	$⊢ (I \in V \land J \subseteq I \land A \in SubMnd (M)) \to (U [J] \subseteq A \leftrightarrow Word J \subseteq A)$

Metamath Proof Explorer

Theorem frmdss2

Proof