Theorem frmd0

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

	Ref	Expression
Hypothesis	frmdmnd.m	⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
Assertion	frmd0	⊢ ∅ = ( 0g ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		frmdmnd.m	⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
2		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
4		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
5		wrd0	⊢ ∅ ∈ Word 𝐼
6	1 2	frmdbas	⊢ ( 𝐼 ∈ V → ( Base ‘ 𝑀 ) = Word 𝐼 )
7	5 6	eleqtrrid	⊢ ( 𝐼 ∈ V → ∅ ∈ ( Base ‘ 𝑀 ) )
8	1 2 4	frmdadd	⊢ ( ( ∅ ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ( +g ‘ 𝑀 ) 𝑥 ) = ( ∅ ++ 𝑥 ) )
9	7 8	sylan	⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ( +g ‘ 𝑀 ) 𝑥 ) = ( ∅ ++ 𝑥 ) )
10	1 2	frmdelbas	⊢ ( 𝑥 ∈ ( Base ‘ 𝑀 ) → 𝑥 ∈ Word 𝐼 )
11	10	adantl	⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → 𝑥 ∈ Word 𝐼 )
12		ccatlid	⊢ ( 𝑥 ∈ Word 𝐼 → ( ∅ ++ 𝑥 ) = 𝑥 )
13	11 12	syl	⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ++ 𝑥 ) = 𝑥 )
14	9 13	eqtrd	⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ( +g ‘ 𝑀 ) 𝑥 ) = 𝑥 )
15	1 2 4	frmdadd	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ ∅ ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ∅ ) = ( 𝑥 ++ ∅ ) )
16	15	ancoms	⊢ ( ( ∅ ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ∅ ) = ( 𝑥 ++ ∅ ) )
17	7 16	sylan	⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ∅ ) = ( 𝑥 ++ ∅ ) )
18		ccatrid	⊢ ( 𝑥 ∈ Word 𝐼 → ( 𝑥 ++ ∅ ) = 𝑥 )
19	11 18	syl	⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ++ ∅ ) = 𝑥 )
20	17 19	eqtrd	⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ∅ ) = 𝑥 )
21	2 3 4 7 14 20	ismgmid2	⊢ ( 𝐼 ∈ V → ∅ = ( 0g ‘ 𝑀 ) )
22		0g0	⊢ ∅ = ( 0g ‘ ∅ )
23		fvprc	⊢ ( ¬ 𝐼 ∈ V → ( freeMnd ‘ 𝐼 ) = ∅ )
24	1 23	eqtrid	⊢ ( ¬ 𝐼 ∈ V → 𝑀 = ∅ )
25	24	fveq2d	⊢ ( ¬ 𝐼 ∈ V → ( 0g ‘ 𝑀 ) = ( 0g ‘ ∅ ) )
26	22 25	eqtr4id	⊢ ( ¬ 𝐼 ∈ V → ∅ = ( 0g ‘ 𝑀 ) )
27	21 26	pm2.61i	⊢ ∅ = ( 0g ‘ 𝑀 )