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	syl5eq	⊢ ( 𝜑 → 𝑊 = 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	⊢ ( 𝜑 → 𝐸 : 𝑋 ⟶ 𝐵 )