frmdsssubm

Description: The set of words taking values in a subset is a (free) submonoid of the free monoid. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

		Ref	Expression
	Hypothesis	frmdmnd.m	$⊢ M = freeMnd (I)$
	Assertion	frmdsssubm	$⊢ (I \in V \land J \subseteq I) \to Word J \in SubMnd (M)$

Proof

Step	Hyp	Ref	Expression
1		frmdmnd.m	$⊢ M = freeMnd (I)$
2		sswrd	$⊢ J \subseteq I \to Word J \subseteq Word I$
3	2	adantl	$⊢ (I \in V \land J \subseteq I) \to Word J \subseteq Word I$
4		eqid	$⊢ {Base}_{M} = {Base}_{M}$
5	1 4	frmdbas	$⊢ I \in V \to {Base}_{M} = Word I$
6	5	adantr	$⊢ (I \in V \land J \subseteq I) \to {Base}_{M} = Word I$
7	3 6	sseqtrrd	$⊢ (I \in V \land J \subseteq I) \to Word J \subseteq {Base}_{M}$
8		wrd0	$⊢ \emptyset \in Word J$
9	8	a1i	$⊢ (I \in V \land J \subseteq I) \to \emptyset \in Word J$
10	7	sselda	$⊢ ((I \in V \land J \subseteq I) \land x \in Word J) \to x \in {Base}_{M}$
11	7	sselda	$⊢ ((I \in V \land J \subseteq I) \land y \in Word J) \to y \in {Base}_{M}$
12	10 11	anim12dan	$⊢ ((I \in V \land J \subseteq I) \land (x \in Word J \land y \in Word J)) \to (x \in {Base}_{M} \land y \in {Base}_{M})$
13		eqid	$⊢ +_{M} = +_{M}$
14	1 4 13	frmdadd	$⊢ (x \in {Base}_{M} \land y \in {Base}_{M}) \to x +_{M} y = x ++ y$
15	12 14	syl	$⊢ ((I \in V \land J \subseteq I) \land (x \in Word J \land y \in Word J)) \to x +_{M} y = x ++ y$
16		ccatcl	$⊢ (x \in Word J \land y \in Word J) \to x ++ y \in Word J$
17	16	adantl	$⊢ ((I \in V \land J \subseteq I) \land (x \in Word J \land y \in Word J)) \to x ++ y \in Word J$
18	15 17	eqeltrd	$⊢ ((I \in V \land J \subseteq I) \land (x \in Word J \land y \in Word J)) \to x +_{M} y \in Word J$
19	18	ralrimivva	$⊢ (I \in V \land J \subseteq I) \to \forall x \in Word J \forall y \in Word J x +_{M} y \in Word J$
20	1	frmdmnd	$⊢ I \in V \to M \in Mnd$
21	20	adantr	$⊢ (I \in V \land J \subseteq I) \to M \in Mnd$
22	1	frmd0	$⊢ \emptyset = 0_{M}$
23	4 22 13	issubm	$⊢ M \in Mnd \to (Word J \in SubMnd (M) \leftrightarrow (Word J \subseteq {Base}_{M} \land \emptyset \in Word J \land \forall x \in Word J \forall y \in Word J x +_{M} y \in Word J))$
24	21 23	syl	$⊢ (I \in V \land J \subseteq I) \to (Word J \in SubMnd (M) \leftrightarrow (Word J \subseteq {Base}_{M} \land \emptyset \in Word J \land \forall x \in Word J \forall y \in Word J x +_{M} y \in Word J))$
25	7 9 19 24	mpbir3and	$⊢ (I \in V \land J \subseteq I) \to Word J \in SubMnd (M)$

Metamath Proof Explorer

Theorem frmdsssubm

Proof