Metamath Proof Explorer


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 syl5eq ( ¬ 𝐼 ∈ V → 𝑀 = ∅ )
25 24 fveq2d ( ¬ 𝐼 ∈ V → ( 0g𝑀 ) = ( 0g ‘ ∅ ) )
26 22 25 eqtr4id ( ¬ 𝐼 ∈ V → ∅ = ( 0g𝑀 ) )
27 21 26 pm2.61i ∅ = ( 0g𝑀 )