This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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