frmd0

Description: The identity of the free monoid is the empty word. (Contributed by Mario Carneiro, 27-Sep-2015)

		Ref	Expression
	Hypothesis	frmdmnd.m	$⊢ M = freeMnd (I)$
	Assertion	frmd0	$⊢ \emptyset = 0_{M}$

Proof

Step	Hyp	Ref	Expression
1		frmdmnd.m	$⊢ M = freeMnd (I)$
2		eqid	$⊢ {Base}_{M} = {Base}_{M}$
3		eqid	$⊢ 0_{M} = 0_{M}$
4		eqid	$⊢ +_{M} = +_{M}$
5		wrd0	$⊢ \emptyset \in Word I$
6	1 2	frmdbas	$⊢ I \in V \to {Base}_{M} = Word I$
7	5 6	eleqtrrid	$⊢ I \in V \to \emptyset \in {Base}_{M}$
8	1 2 4	frmdadd	$⊢ (\emptyset \in {Base}_{M} \land x \in {Base}_{M}) \to \emptyset +_{M} x = \emptyset ++ x$
9	7 8	sylan	$⊢ (I \in V \land x \in {Base}_{M}) \to \emptyset +_{M} x = \emptyset ++ x$
10	1 2	frmdelbas	$⊢ x \in {Base}_{M} \to x \in Word I$
11	10	adantl	$⊢ (I \in V \land x \in {Base}_{M}) \to x \in Word I$
12		ccatlid	$⊢ x \in Word I \to \emptyset ++ x = x$
13	11 12	syl	$⊢ (I \in V \land x \in {Base}_{M}) \to \emptyset ++ x = x$
14	9 13	eqtrd	$⊢ (I \in V \land x \in {Base}_{M}) \to \emptyset +_{M} x = x$
15	1 2 4	frmdadd	$⊢ (x \in {Base}_{M} \land \emptyset \in {Base}_{M}) \to x +_{M} \emptyset = x ++ \emptyset$
16	15	ancoms	$⊢ (\emptyset \in {Base}_{M} \land x \in {Base}_{M}) \to x +_{M} \emptyset = x ++ \emptyset$
17	7 16	sylan	$⊢ (I \in V \land x \in {Base}_{M}) \to x +_{M} \emptyset = x ++ \emptyset$
18		ccatrid	$⊢ x \in Word I \to x ++ \emptyset = x$
19	11 18	syl	$⊢ (I \in V \land x \in {Base}_{M}) \to x ++ \emptyset = x$
20	17 19	eqtrd	$⊢ (I \in V \land x \in {Base}_{M}) \to x +_{M} \emptyset = x$
21	2 3 4 7 14 20	ismgmid2	$⊢ I \in V \to \emptyset = 0_{M}$
22		0g0	$⊢ \emptyset = 0_{\emptyset}$
23		fvprc	$⊢ \neg I \in V \to freeMnd (I) = \emptyset$
24	1 23	eqtrid	$⊢ \neg I \in V \to M = \emptyset$
25	24	fveq2d	$⊢ \neg I \in V \to 0_{M} = 0_{\emptyset}$
26	22 25	eqtr4id	$⊢ \neg I \in V \to \emptyset = 0_{M}$
27	21 26	pm2.61i	$⊢ \emptyset = 0_{M}$

Metamath Proof Explorer

Theorem frmd0

Proof