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

Metamath Proof Explorer

Theorem frmdup3

Description: Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses frmdup3.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
frmdup3.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
frmdup3.u ⊢ 𝑈 = ( varFMnd ‘ 𝐼 )
Assertion frmdup3 ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ∃! 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 frmdup3.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
2 frmdup3.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 frmdup3.u ⊢ 𝑈 = ( varFMnd ‘ 𝐼 )
4 eqid ⊢ ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) )
5 simp1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → 𝐺 ∈ Mnd )
6 simp2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → 𝐼 ∈ 𝑉 )
7 simp3 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → 𝐴 : 𝐼 ⟶ 𝐵 )
8 1 2 4 5 6 7 frmdup1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∈ ( 𝑀 MndHom 𝐺 ) )
9 5 adantr ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝐺 ∈ Mnd )
10 6 adantr ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ 𝑉 )
11 7 adantr ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝐴 : 𝐼 ⟶ 𝐵 )
12 simpr ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
13 1 2 4 9 10 11 3 12 frmdup2 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ‘ ( 𝑈 ‘ 𝑦 ) ) = ( 𝐴 ‘ 𝑦 ) )
14 13 mpteq2dva ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ‘ ( 𝑈 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝐴 ‘ 𝑦 ) ) )
15 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
16 15 2 mhmf ⊢ ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∈ ( 𝑀 MndHom 𝐺 ) → ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) : ( Base ‘ 𝑀 ) ⟶ 𝐵 )
17 8 16 syl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) : ( Base ‘ 𝑀 ) ⟶ 𝐵 )
18 3 vrmdf ⊢ ( 𝐼 ∈ 𝑉 → 𝑈 : 𝐼 ⟶ Word 𝐼 )
19 18 3ad2ant2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → 𝑈 : 𝐼 ⟶ Word 𝐼 )
20 1 15 frmdbas ⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝑀 ) = Word 𝐼 )
21 20 3ad2ant2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( Base ‘ 𝑀 ) = Word 𝐼 )
22 21 feq3d ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝑈 : 𝐼 ⟶ ( Base ‘ 𝑀 ) ↔ 𝑈 : 𝐼 ⟶ Word 𝐼 ) )
23 19 22 mpbird ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → 𝑈 : 𝐼 ⟶ ( Base ‘ 𝑀 ) )
24 fcompt ⊢ ( ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) : ( Base ‘ 𝑀 ) ⟶ 𝐵 ∧ 𝑈 : 𝐼 ⟶ ( Base ‘ 𝑀 ) ) → ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∘ 𝑈 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ‘ ( 𝑈 ‘ 𝑦 ) ) ) )
25 17 23 24 syl2anc ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∘ 𝑈 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ‘ ( 𝑈 ‘ 𝑦 ) ) ) )
26 7 feqmptd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → 𝐴 = ( 𝑦 ∈ 𝐼 ↦ ( 𝐴 ‘ 𝑦 ) ) )
27 14 25 26 3eqtr4d ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∘ 𝑈 ) = 𝐴 )
28 1 2 3 frmdup3lem ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝑚 ∘ 𝑈 ) = 𝐴 ) ) → 𝑚 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) )
29 28 expr ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ) → ( ( 𝑚 ∘ 𝑈 ) = 𝐴 → 𝑚 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ) )
30 29 ralrimiva ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ∀ 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ( ( 𝑚 ∘ 𝑈 ) = 𝐴 → 𝑚 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ) )
31 coeq1 ⊢ ( 𝑚 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) → ( 𝑚 ∘ 𝑈 ) = ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∘ 𝑈 ) )
32 31 eqeq1d ⊢ ( 𝑚 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) → ( ( 𝑚 ∘ 𝑈 ) = 𝐴 ↔ ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∘ 𝑈 ) = 𝐴 ) )
33 32 eqreu ⊢ ( ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∘ 𝑈 ) = 𝐴 ∧ ∀ 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ( ( 𝑚 ∘ 𝑈 ) = 𝐴 → 𝑚 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ) ) → ∃! 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 )
34 8 27 30 33 syl3anc ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ∃! 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 )