frmdmnd

Description: A free monoid is a monoid. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

		Ref	Expression
	Hypothesis	frmdmnd.m	$⊢ M = freeMnd (I)$
	Assertion	frmdmnd	$⊢ I \in V \to M \in Mnd$

Proof

Step	Hyp	Ref	Expression
1		frmdmnd.m	$⊢ M = freeMnd (I)$
2		eqidd	$⊢ I \in V \to {Base}_{M} = {Base}_{M}$
3		eqidd	$⊢ I \in V \to +_{M} = +_{M}$
4		eqid	$⊢ {Base}_{M} = {Base}_{M}$
5		eqid	$⊢ +_{M} = +_{M}$
6	1 4 5	frmdadd	$⊢ (x \in {Base}_{M} \land y \in {Base}_{M}) \to x +_{M} y = x ++ y$
7	1 4	frmdelbas	$⊢ x \in {Base}_{M} \to x \in Word I$
8	1 4	frmdelbas	$⊢ y \in {Base}_{M} \to y \in Word I$
9		ccatcl	$⊢ (x \in Word I \land y \in Word I) \to x ++ y \in Word I$
10	7 8 9	syl2an	$⊢ (x \in {Base}_{M} \land y \in {Base}_{M}) \to x ++ y \in Word I$
11	6 10	eqeltrd	$⊢ (x \in {Base}_{M} \land y \in {Base}_{M}) \to x +_{M} y \in Word I$
12	11	3adant1	$⊢ (I \in V \land x \in {Base}_{M} \land y \in {Base}_{M}) \to x +_{M} y \in Word I$
13	1 4	frmdbas	$⊢ I \in V \to {Base}_{M} = Word I$
14	13	3ad2ant1	$⊢ (I \in V \land x \in {Base}_{M} \land y \in {Base}_{M}) \to {Base}_{M} = Word I$
15	12 14	eleqtrrd	$⊢ (I \in V \land x \in {Base}_{M} \land y \in {Base}_{M}) \to x +_{M} y \in {Base}_{M}$
16		simpr1	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to x \in {Base}_{M}$
17	16 7	syl	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to x \in Word I$
18		simpr2	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to y \in {Base}_{M}$
19	18 8	syl	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to y \in Word I$
20		simpr3	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to z \in {Base}_{M}$
21	1 4	frmdelbas	$⊢ z \in {Base}_{M} \to z \in Word I$
22	20 21	syl	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to z \in Word I$
23		ccatass	$⊢ (x \in Word I \land y \in Word I \land z \in Word I) \to (x ++ y) ++ z = x ++ (y ++ z)$
24	17 19 22 23	syl3anc	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to (x ++ y) ++ z = x ++ (y ++ z)$
25	16 18 10	syl2anc	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to x ++ y \in Word I$
26	13	adantr	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to {Base}_{M} = Word I$
27	25 26	eleqtrrd	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to x ++ y \in {Base}_{M}$
28	1 4 5	frmdadd	$⊢ (x ++ y \in {Base}_{M} \land z \in {Base}_{M}) \to (x ++ y) +_{M} z = (x ++ y) ++ z$
29	27 20 28	syl2anc	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to (x ++ y) +_{M} z = (x ++ y) ++ z$
30		ccatcl	$⊢ (y \in Word I \land z \in Word I) \to y ++ z \in Word I$
31	19 22 30	syl2anc	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to y ++ z \in Word I$
32	31 26	eleqtrrd	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to y ++ z \in {Base}_{M}$
33	1 4 5	frmdadd	$⊢ (x \in {Base}_{M} \land y ++ z \in {Base}_{M}) \to x +_{M} (y ++ z) = x ++ (y ++ z)$
34	16 32 33	syl2anc	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to x +_{M} (y ++ z) = x ++ (y ++ z)$
35	24 29 34	3eqtr4d	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to (x ++ y) +_{M} z = x +_{M} (y ++ z)$
36	16 18 6	syl2anc	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to x +_{M} y = x ++ y$
37	36	oveq1d	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to (x +_{M} y) +_{M} z = (x ++ y) +_{M} z$
38	1 4 5	frmdadd	$⊢ (y \in {Base}_{M} \land z \in {Base}_{M}) \to y +_{M} z = y ++ z$
39	18 20 38	syl2anc	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to y +_{M} z = y ++ z$
40	39	oveq2d	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to x +_{M} (y +_{M} z) = x +_{M} (y ++ z)$
41	35 37 40	3eqtr4d	$⊢ (I \in V \land (x \in {Base}_{M} \land y \in {Base}_{M} \land z \in {Base}_{M})) \to (x +_{M} y) +_{M} z = x +_{M} (y +_{M} z)$
42		wrd0	$⊢ \emptyset \in Word I$
43	42 13	eleqtrrid	$⊢ I \in V \to \emptyset \in {Base}_{M}$
44	1 4 5	frmdadd	$⊢ (\emptyset \in {Base}_{M} \land x \in {Base}_{M}) \to \emptyset +_{M} x = \emptyset ++ x$
45	43 44	sylan	$⊢ (I \in V \land x \in {Base}_{M}) \to \emptyset +_{M} x = \emptyset ++ x$
46	7	adantl	$⊢ (I \in V \land x \in {Base}_{M}) \to x \in Word I$
47		ccatlid	$⊢ x \in Word I \to \emptyset ++ x = x$
48	46 47	syl	$⊢ (I \in V \land x \in {Base}_{M}) \to \emptyset ++ x = x$
49	45 48	eqtrd	$⊢ (I \in V \land x \in {Base}_{M}) \to \emptyset +_{M} x = x$
50	1 4 5	frmdadd	$⊢ (x \in {Base}_{M} \land \emptyset \in {Base}_{M}) \to x +_{M} \emptyset = x ++ \emptyset$
51	50	ancoms	$⊢ (\emptyset \in {Base}_{M} \land x \in {Base}_{M}) \to x +_{M} \emptyset = x ++ \emptyset$
52	43 51	sylan	$⊢ (I \in V \land x \in {Base}_{M}) \to x +_{M} \emptyset = x ++ \emptyset$
53		ccatrid	$⊢ x \in Word I \to x ++ \emptyset = x$
54	46 53	syl	$⊢ (I \in V \land x \in {Base}_{M}) \to x ++ \emptyset = x$
55	52 54	eqtrd	$⊢ (I \in V \land x \in {Base}_{M}) \to x +_{M} \emptyset = x$
56	2 3 15 41 43 49 55	ismndd	$⊢ I \in V \to M \in Mnd$

Metamath Proof Explorer

Theorem frmdmnd

Proof