Theorem frgpmhm

Description: The "natural map" from words of the free monoid to their cosets in the free group is a surjective monoid homomorphism. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	frgpmhm.m	⊢ 𝑀 = ( freeMnd ‘ ( 𝐼 × 2o ) )
	frgpmhm.w	⊢ 𝑊 = ( Base ‘ 𝑀 )
	frgpmhm.g	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
	frgpmhm.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
	frgpmhm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑊 ↦ [ 𝑥 ] ∼ )
Assertion	frgpmhm	⊢ ( 𝐼 ∈ 𝑉 → 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		frgpmhm.m	⊢ 𝑀 = ( freeMnd ‘ ( 𝐼 × 2o ) )
2		frgpmhm.w	⊢ 𝑊 = ( Base ‘ 𝑀 )
3		frgpmhm.g	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
4		frgpmhm.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
5		frgpmhm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑊 ↦ [ 𝑥 ] ∼ )
6		2on	⊢ 2o ∈ On
7		xpexg	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
8	6 7	mpan2	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × 2o ) ∈ V )
9	1	frmdmnd	⊢ ( ( 𝐼 × 2o ) ∈ V → 𝑀 ∈ Mnd )
10	8 9	syl	⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd )
11	3	frgpgrp	⊢ ( 𝐼 ∈ 𝑉 → 𝐺 ∈ Grp )
12	11	grpmndd	⊢ ( 𝐼 ∈ 𝑉 → 𝐺 ∈ Mnd )
13	1 2	frmdbas	⊢ ( ( 𝐼 × 2o ) ∈ V → 𝑊 = Word ( 𝐼 × 2o ) )
14		wrdexg	⊢ ( ( 𝐼 × 2o ) ∈ V → Word ( 𝐼 × 2o ) ∈ V )
15		fvi	⊢ ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
16	14 15	syl	⊢ ( ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
17	13 16	eqtr4d	⊢ ( ( 𝐼 × 2o ) ∈ V → 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) ) )
18	8 17	syl	⊢ ( 𝐼 ∈ 𝑉 → 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) ) )
19	18	eleq2d	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) )
20	19	biimpa	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) → 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) )
21		eqid	⊢ ( I ‘ Word ( 𝐼 × 2o ) ) = ( I ‘ Word ( 𝐼 × 2o ) )
22		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
23	3 4 21 22	frgpeccl	⊢ ( 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) → [ 𝑥 ] ∼ ∈ ( Base ‘ 𝐺 ) )
24	20 23	syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) → [ 𝑥 ] ∼ ∈ ( Base ‘ 𝐺 ) )
25	24 5	fmptd	⊢ ( 𝐼 ∈ 𝑉 → 𝐹 : 𝑊 ⟶ ( Base ‘ 𝐺 ) )
26	21 4	efger	⊢ ∼ Er ( I ‘ Word ( 𝐼 × 2o ) )
27		ereq2	⊢ ( 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) ) → ( ∼ Er 𝑊 ↔ ∼ Er ( I ‘ Word ( 𝐼 × 2o ) ) ) )
28	18 27	syl	⊢ ( 𝐼 ∈ 𝑉 → ( ∼ Er 𝑊 ↔ ∼ Er ( I ‘ Word ( 𝐼 × 2o ) ) ) )
29	26 28	mpbiri	⊢ ( 𝐼 ∈ 𝑉 → ∼ Er 𝑊 )
30	29	adantr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ∼ Er 𝑊 )
31	2	fvexi	⊢ 𝑊 ∈ V
32	31	a1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → 𝑊 ∈ V )
33	30 32 5	divsfval	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝐹 ‘ ( 𝑎 ++ 𝑏 ) ) = [ ( 𝑎 ++ 𝑏 ) ] ∼ )
34		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
35	1 2 34	frmdadd	⊢ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝑎 ++ 𝑏 ) )
36	35	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝑎 ++ 𝑏 ) )
37	36	fveq2d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑎 ++ 𝑏 ) ) )
38	30 32 5	divsfval	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑎 ) = [ 𝑎 ] ∼ )
39	30 32 5	divsfval	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑏 ) = [ 𝑏 ] ∼ )
40	38 39	oveq12d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) = ( [ 𝑎 ] ∼ ( +g ‘ 𝐺 ) [ 𝑏 ] ∼ ) )
41	18	eleq2d	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑎 ∈ 𝑊 ↔ 𝑎 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) )
42	18	eleq2d	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑏 ∈ 𝑊 ↔ 𝑏 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) )
43	41 42	anbi12d	⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ↔ ( 𝑎 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ∧ 𝑏 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) ) )
44	43	biimpa	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝑎 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ∧ 𝑏 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) )
45		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
46	21 3 4 45	frgpadd	⊢ ( ( 𝑎 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ∧ 𝑏 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) → ( [ 𝑎 ] ∼ ( +g ‘ 𝐺 ) [ 𝑏 ] ∼ ) = [ ( 𝑎 ++ 𝑏 ) ] ∼ )
47	44 46	syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( [ 𝑎 ] ∼ ( +g ‘ 𝐺 ) [ 𝑏 ] ∼ ) = [ ( 𝑎 ++ 𝑏 ) ] ∼ )
48	40 47	eqtrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) = [ ( 𝑎 ++ 𝑏 ) ] ∼ )
49	33 37 48	3eqtr4d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) )
50	49	ralrimivva	⊢ ( 𝐼 ∈ 𝑉 → ∀ 𝑎 ∈ 𝑊 ∀ 𝑏 ∈ 𝑊 ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) )
51	31	a1i	⊢ ( 𝐼 ∈ 𝑉 → 𝑊 ∈ V )
52	29 51 5	divsfval	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 ‘ ∅ ) = [ ∅ ] ∼ )
53	3 4	frgp0	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐺 ∈ Grp ∧ [ ∅ ] ∼ = ( 0g ‘ 𝐺 ) ) )
54	53	simprd	⊢ ( 𝐼 ∈ 𝑉 → [ ∅ ] ∼ = ( 0g ‘ 𝐺 ) )
55	52 54	eqtrd	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 ‘ ∅ ) = ( 0g ‘ 𝐺 ) )
56	25 50 55	3jca	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 : 𝑊 ⟶ ( Base ‘ 𝐺 ) ∧ ∀ 𝑎 ∈ 𝑊 ∀ 𝑏 ∈ 𝑊 ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝐹 ‘ ∅ ) = ( 0g ‘ 𝐺 ) ) )
57	1	frmd0	⊢ ∅ = ( 0g ‘ 𝑀 )
58		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
59	2 22 34 45 57 58	ismhm	⊢ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ↔ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ∈ Mnd ) ∧ ( 𝐹 : 𝑊 ⟶ ( Base ‘ 𝐺 ) ∧ ∀ 𝑎 ∈ 𝑊 ∀ 𝑏 ∈ 𝑊 ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝐹 ‘ ∅ ) = ( 0g ‘ 𝐺 ) ) ) )
60	10 12 56 59	syl21anbrc	⊢ ( 𝐼 ∈ 𝑉 → 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) )