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 ⊢ M = freeMnd ⁡ I
Assertion frmd0 ⊢ ∅ = 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 ⊢ ∅ ∈ Word I
6 1 2 frmdbas ⊢ I ∈ V → Base M = Word I
7 5 6 eleqtrrid ⊢ I ∈ V → ∅ ∈ Base M
8 1 2 4 frmdadd ⊢ ∅ ∈ Base M ∧ x ∈ Base M → ∅ + M x = ∅ ++ x
9 7 8 sylan ⊢ I ∈ V ∧ x ∈ Base M → ∅ + M x = ∅ ++ x
10 1 2 frmdelbas ⊢ x ∈ Base M → x ∈ Word I
11 10 adantl ⊢ I ∈ V ∧ x ∈ Base M → x ∈ Word I
12 ccatlid ⊢ x ∈ Word I → ∅ ++ x = x
13 11 12 syl ⊢ I ∈ V ∧ x ∈ Base M → ∅ ++ x = x
14 9 13 eqtrd ⊢ I ∈ V ∧ x ∈ Base M → ∅ + M x = x
15 1 2 4 frmdadd ⊢ x ∈ Base M ∧ ∅ ∈ Base M → x + M ∅ = x ++ ∅
16 15 ancoms ⊢ ∅ ∈ Base M ∧ x ∈ Base M → x + M ∅ = x ++ ∅
17 7 16 sylan ⊢ I ∈ V ∧ x ∈ Base M → x + M ∅ = x ++ ∅
18 ccatrid ⊢ x ∈ Word I → x ++ ∅ = x
19 11 18 syl ⊢ I ∈ V ∧ x ∈ Base M → x ++ ∅ = x
20 17 19 eqtrd ⊢ I ∈ V ∧ x ∈ Base M → x + M ∅ = x
21 2 3 4 7 14 20 ismgmid2 ⊢ I ∈ V → ∅ = 0 M
22 0g0 ⊢ ∅ = 0 ∅
23 fvprc ⊢ ¬ I ∈ V → freeMnd ⁡ I = ∅
24 1 23 eqtrid ⊢ ¬ I ∈ V → M = ∅
25 24 fveq2d ⊢ ¬ I ∈ V → 0 M = 0 ∅
26 22 25 eqtr4id ⊢ ¬ I ∈ V → ∅ = 0 M
27 21 26 pm2.61i ⊢ ∅ = 0 M