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

Metamath Proof Explorer

Theorem frgpupf

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, 2-Oct-2015)

Ref Expression
Hypotheses frgpup.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
frgpup.n ⊢ 𝑁 = ( invg ‘ 𝐻 )
frgpup.t ⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
frgpup.h ⊢ ( 𝜑 → 𝐻 ∈ Grp )
frgpup.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
frgpup.a ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
frgpup.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
frgpup.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
frgpup.g ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
frgpup.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
frgpup.e ⊢ 𝐸 = ran ( 𝑔 ∈ 𝑊 ↦ ⟨ [ 𝑔 ] ∼ , ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) ⟩ )
Assertion frgpupf ( 𝜑 → 𝐸 : 𝑋 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 frgpup.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
2 frgpup.n ⊢ 𝑁 = ( invg ‘ 𝐻 )
3 frgpup.t ⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
4 frgpup.h ⊢ ( 𝜑 → 𝐻 ∈ Grp )
5 frgpup.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 frgpup.a ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
7 frgpup.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
8 frgpup.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
9 frgpup.g ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
10 frgpup.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
11 frgpup.e ⊢ 𝐸 = ran ( 𝑔 ∈ 𝑊 ↦ ⟨ [ 𝑔 ] ∼ , ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) ⟩ )
12 4 grpmndd ⊢ ( 𝜑 → 𝐻 ∈ Mnd )
13 fviss ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
14 7 13 eqsstri ⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
15 14 sseli ⊢ ( 𝑔 ∈ 𝑊 → 𝑔 ∈ Word ( 𝐼 × 2o ) )
16 1 2 3 4 5 6 frgpuptf ⊢ ( 𝜑 → 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 )
17 wrdco ⊢ ( ( 𝑔 ∈ Word ( 𝐼 × 2o ) ∧ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 ) → ( 𝑇 ∘ 𝑔 ) ∈ Word 𝐵 )
18 15 16 17 syl2anr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑊 ) → ( 𝑇 ∘ 𝑔 ) ∈ Word 𝐵 )
19 1 gsumwcl ⊢ ( ( 𝐻 ∈ Mnd ∧ ( 𝑇 ∘ 𝑔 ) ∈ Word 𝐵 ) → ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) ∈ 𝐵 )
20 12 18 19 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑊 ) → ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) ∈ 𝐵 )
21 7 8 efger ⊢ ∼ Er 𝑊
22 21 a1i ⊢ ( 𝜑 → ∼ Er 𝑊 )
23 7 fvexi ⊢ 𝑊 ∈ V
24 23 a1i ⊢ ( 𝜑 → 𝑊 ∈ V )
25 coeq2 ⊢ ( 𝑔 = ℎ → ( 𝑇 ∘ 𝑔 ) = ( 𝑇 ∘ ℎ ) )
26 25 oveq2d ⊢ ( 𝑔 = ℎ → ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) = ( 𝐻 Σg ( 𝑇 ∘ ℎ ) ) )
27 1 2 3 4 5 6 7 8 frgpuplem ⊢ ( ( 𝜑 ∧ 𝑔 ∼ ℎ ) → ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) = ( 𝐻 Σg ( 𝑇 ∘ ℎ ) ) )
28 11 20 22 24 26 27 qliftfund ⊢ ( 𝜑 → Fun 𝐸 )
29 11 20 22 24 qliftf ⊢ ( 𝜑 → ( Fun 𝐸 ↔ 𝐸 : ( 𝑊 / ∼ ) ⟶ 𝐵 ) )
30 28 29 mpbid ⊢ ( 𝜑 → 𝐸 : ( 𝑊 / ∼ ) ⟶ 𝐵 )
31 eqid ⊢ ( freeMnd ‘ ( 𝐼 × 2o ) ) = ( freeMnd ‘ ( 𝐼 × 2o ) )
32 9 31 8 frgpval ⊢ ( 𝐼 ∈ 𝑉 → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ∼ ) )
33 5 32 syl ⊢ ( 𝜑 → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ∼ ) )
34 2on ⊢ 2o ∈ On
35 xpexg ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
36 5 34 35 sylancl ⊢ ( 𝜑 → ( 𝐼 × 2o ) ∈ V )
37 wrdexg ⊢ ( ( 𝐼 × 2o ) ∈ V → Word ( 𝐼 × 2o ) ∈ V )
38 fvi ⊢ ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
39 36 37 38 3syl ⊢ ( 𝜑 → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
40 7 39 eqtrid ⊢ ( 𝜑 → 𝑊 = Word ( 𝐼 × 2o ) )
41 eqid ⊢ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) )
42 31 41 frmdbas ⊢ ( ( 𝐼 × 2o ) ∈ V → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
43 36 42 syl ⊢ ( 𝜑 → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
44 40 43 eqtr4d ⊢ ( 𝜑 → 𝑊 = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
45 8 fvexi ⊢ ∼ ∈ V
46 45 a1i ⊢ ( 𝜑 → ∼ ∈ V )
47 fvexd ⊢ ( 𝜑 → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ V )
48 33 44 46 47 qusbas ⊢ ( 𝜑 → ( 𝑊 / ∼ ) = ( Base ‘ 𝐺 ) )
49 10 48 eqtr4id ⊢ ( 𝜑 → 𝑋 = ( 𝑊 / ∼ ) )
50 49 feq2d ⊢ ( 𝜑 → ( 𝐸 : 𝑋 ⟶ 𝐵 ↔ 𝐸 : ( 𝑊 / ∼ ) ⟶ 𝐵 ) )
51 30 50 mpbird ⊢ ( 𝜑 → 𝐸 : 𝑋 ⟶ 𝐵 )