Metamath Proof Explorer

Theorem frmdup1

Description: Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses frmdup.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
frmdup.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
frmdup.e ⊢ 𝐸 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) )
frmdup.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
frmdup.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
frmdup.a ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐵 )
Assertion frmdup1 ( 𝜑 → 𝐸 ∈ ( 𝑀 MndHom 𝐺 ) )

Proof

Step Hyp Ref Expression
1 frmdup.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
2 frmdup.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 frmdup.e ⊢ 𝐸 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) )
4 frmdup.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
5 frmdup.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
6 frmdup.a ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐵 )
7 1 frmdmnd ⊢ ( 𝐼 ∈ 𝑋 → 𝑀 ∈ Mnd )
8 5 7 syl ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
9 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ Word 𝐼 ) → 𝐺 ∈ Mnd )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ Word 𝐼 ) → 𝑥 ∈ Word 𝐼 )
11 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ Word 𝐼 ) → 𝐴 : 𝐼 ⟶ 𝐵 )
12 wrdco ⊢ ( ( 𝑥 ∈ Word 𝐼 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝐴 ∘ 𝑥 ) ∈ Word 𝐵 )
13 10 11 12 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ Word 𝐼 ) → ( 𝐴 ∘ 𝑥 ) ∈ Word 𝐵 )
14 2 gsumwcl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝐴 ∘ 𝑥 ) ∈ Word 𝐵 ) → ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ∈ 𝐵 )
15 9 13 14 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ Word 𝐼 ) → ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ∈ 𝐵 )
16 15 3 fmptd ⊢ ( 𝜑 → 𝐸 : Word 𝐼 ⟶ 𝐵 )
17 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
18 1 17 frmdbas ⊢ ( 𝐼 ∈ 𝑋 → ( Base ‘ 𝑀 ) = Word 𝐼 )
19 5 18 syl ⊢ ( 𝜑 → ( Base ‘ 𝑀 ) = Word 𝐼 )
20 19 feq2d ⊢ ( 𝜑 → ( 𝐸 : ( Base ‘ 𝑀 ) ⟶ 𝐵 ↔ 𝐸 : Word 𝐼 ⟶ 𝐵 ) )
21 16 20 mpbird ⊢ ( 𝜑 → 𝐸 : ( Base ‘ 𝑀 ) ⟶ 𝐵 )
22 1 17 frmdelbas ⊢ ( 𝑦 ∈ ( Base ‘ 𝑀 ) → 𝑦 ∈ Word 𝐼 )
23 22 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑦 ∈ Word 𝐼 )
24 1 17 frmdelbas ⊢ ( 𝑧 ∈ ( Base ‘ 𝑀 ) → 𝑧 ∈ Word 𝐼 )
25 24 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑧 ∈ Word 𝐼 )
26 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐴 : 𝐼 ⟶ 𝐵 )
27 ccatco ⊢ ( ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ Word 𝐼 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝐴 ∘ ( 𝑦 ++ 𝑧 ) ) = ( ( 𝐴 ∘ 𝑦 ) ++ ( 𝐴 ∘ 𝑧 ) ) )
28 23 25 26 27 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐴 ∘ ( 𝑦 ++ 𝑧 ) ) = ( ( 𝐴 ∘ 𝑦 ) ++ ( 𝐴 ∘ 𝑧 ) ) )
29 28 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 Σg ( 𝐴 ∘ ( 𝑦 ++ 𝑧 ) ) ) = ( 𝐺 Σg ( ( 𝐴 ∘ 𝑦 ) ++ ( 𝐴 ∘ 𝑧 ) ) ) )
30 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐺 ∈ Mnd )
31 wrdco ⊢ ( ( 𝑦 ∈ Word 𝐼 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝐴 ∘ 𝑦 ) ∈ Word 𝐵 )
32 23 26 31 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐴 ∘ 𝑦 ) ∈ Word 𝐵 )
33 wrdco ⊢ ( ( 𝑧 ∈ Word 𝐼 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝐴 ∘ 𝑧 ) ∈ Word 𝐵 )
34 25 26 33 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐴 ∘ 𝑧 ) ∈ Word 𝐵 )
35 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
36 2 35 gsumccat ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝐴 ∘ 𝑦 ) ∈ Word 𝐵 ∧ ( 𝐴 ∘ 𝑧 ) ∈ Word 𝐵 ) → ( 𝐺 Σg ( ( 𝐴 ∘ 𝑦 ) ++ ( 𝐴 ∘ 𝑧 ) ) ) = ( ( 𝐺 Σg ( 𝐴 ∘ 𝑦 ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐴 ∘ 𝑧 ) ) ) )
37 30 32 34 36 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 Σg ( ( 𝐴 ∘ 𝑦 ) ++ ( 𝐴 ∘ 𝑧 ) ) ) = ( ( 𝐺 Σg ( 𝐴 ∘ 𝑦 ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐴 ∘ 𝑧 ) ) ) )
38 29 37 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 Σg ( 𝐴 ∘ ( 𝑦 ++ 𝑧 ) ) ) = ( ( 𝐺 Σg ( 𝐴 ∘ 𝑦 ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐴 ∘ 𝑧 ) ) ) )
39 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
40 1 17 39 frmdadd ⊢ ( ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑦 ++ 𝑧 ) )
41 40 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑦 ++ 𝑧 ) )
42 41 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐸 ‘ ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) = ( 𝐸 ‘ ( 𝑦 ++ 𝑧 ) ) )
43 ccatcl ⊢ ( ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ Word 𝐼 ) → ( 𝑦 ++ 𝑧 ) ∈ Word 𝐼 )
44 23 25 43 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑦 ++ 𝑧 ) ∈ Word 𝐼 )
45 coeq2 ⊢ ( 𝑥 = ( 𝑦 ++ 𝑧 ) → ( 𝐴 ∘ 𝑥 ) = ( 𝐴 ∘ ( 𝑦 ++ 𝑧 ) ) )
46 45 oveq2d ⊢ ( 𝑥 = ( 𝑦 ++ 𝑧 ) → ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) = ( 𝐺 Σg ( 𝐴 ∘ ( 𝑦 ++ 𝑧 ) ) ) )
47 ovex ⊢ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ∈ V
48 46 3 47 fvmpt3i ⊢ ( ( 𝑦 ++ 𝑧 ) ∈ Word 𝐼 → ( 𝐸 ‘ ( 𝑦 ++ 𝑧 ) ) = ( 𝐺 Σg ( 𝐴 ∘ ( 𝑦 ++ 𝑧 ) ) ) )
49 44 48 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐸 ‘ ( 𝑦 ++ 𝑧 ) ) = ( 𝐺 Σg ( 𝐴 ∘ ( 𝑦 ++ 𝑧 ) ) ) )
50 42 49 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐸 ‘ ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) = ( 𝐺 Σg ( 𝐴 ∘ ( 𝑦 ++ 𝑧 ) ) ) )
51 coeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∘ 𝑥 ) = ( 𝐴 ∘ 𝑦 ) )
52 51 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) = ( 𝐺 Σg ( 𝐴 ∘ 𝑦 ) ) )
53 52 3 47 fvmpt3i ⊢ ( 𝑦 ∈ Word 𝐼 → ( 𝐸 ‘ 𝑦 ) = ( 𝐺 Σg ( 𝐴 ∘ 𝑦 ) ) )
54 coeq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐴 ∘ 𝑥 ) = ( 𝐴 ∘ 𝑧 ) )
55 54 oveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) = ( 𝐺 Σg ( 𝐴 ∘ 𝑧 ) ) )
56 55 3 47 fvmpt3i ⊢ ( 𝑧 ∈ Word 𝐼 → ( 𝐸 ‘ 𝑧 ) = ( 𝐺 Σg ( 𝐴 ∘ 𝑧 ) ) )
57 53 56 oveqan12d ⊢ ( ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ Word 𝐼 ) → ( ( 𝐸 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝐸 ‘ 𝑧 ) ) = ( ( 𝐺 Σg ( 𝐴 ∘ 𝑦 ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐴 ∘ 𝑧 ) ) ) )
58 23 25 57 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐸 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝐸 ‘ 𝑧 ) ) = ( ( 𝐺 Σg ( 𝐴 ∘ 𝑦 ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐴 ∘ 𝑧 ) ) ) )
59 38 50 58 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐸 ‘ ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) = ( ( 𝐸 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝐸 ‘ 𝑧 ) ) )
60 59 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ∀ 𝑧 ∈ ( Base ‘ 𝑀 ) ( 𝐸 ‘ ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) = ( ( 𝐸 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝐸 ‘ 𝑧 ) ) )
61 wrd0 ⊢ ∅ ∈ Word 𝐼
62 coeq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ∘ 𝑥 ) = ( 𝐴 ∘ ∅ ) )
63 co02 ⊢ ( 𝐴 ∘ ∅ ) = ∅
64 62 63 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝐴 ∘ 𝑥 ) = ∅ )
65 64 oveq2d ⊢ ( 𝑥 = ∅ → ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) = ( 𝐺 Σg ∅ ) )
66 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
67 66 gsum0 ⊢ ( 𝐺 Σg ∅ ) = ( 0g ‘ 𝐺 )
68 65 67 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) = ( 0g ‘ 𝐺 ) )
69 68 3 47 fvmpt3i ⊢ ( ∅ ∈ Word 𝐼 → ( 𝐸 ‘ ∅ ) = ( 0g ‘ 𝐺 ) )
70 61 69 mp1i ⊢ ( 𝜑 → ( 𝐸 ‘ ∅ ) = ( 0g ‘ 𝐺 ) )
71 21 60 70 3jca ⊢ ( 𝜑 → ( 𝐸 : ( Base ‘ 𝑀 ) ⟶ 𝐵 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ∀ 𝑧 ∈ ( Base ‘ 𝑀 ) ( 𝐸 ‘ ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) = ( ( 𝐸 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝐸 ‘ 𝑧 ) ) ∧ ( 𝐸 ‘ ∅ ) = ( 0g ‘ 𝐺 ) ) )
72 1 frmd0 ⊢ ∅ = ( 0g ‘ 𝑀 )
73 17 2 39 35 72 66 ismhm ⊢ ( 𝐸 ∈ ( 𝑀 MndHom 𝐺 ) ↔ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ∈ Mnd ) ∧ ( 𝐸 : ( Base ‘ 𝑀 ) ⟶ 𝐵 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ∀ 𝑧 ∈ ( Base ‘ 𝑀 ) ( 𝐸 ‘ ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) = ( ( 𝐸 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝐸 ‘ 𝑧 ) ) ∧ ( 𝐸 ‘ ∅ ) = ( 0g ‘ 𝐺 ) ) ) )
74 8 4 71 73 syl21anbrc ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑀 MndHom 𝐺 ) )