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		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
13	11 12	syl	⊢ ( 𝐼 ∈ 𝑉 → 𝐺 ∈ Mnd )
14	1 2	frmdbas	⊢ ( ( 𝐼 × 2o ) ∈ V → 𝑊 = Word ( 𝐼 × 2o ) )
15		wrdexg	⊢ ( ( 𝐼 × 2o ) ∈ V → Word ( 𝐼 × 2o ) ∈ V )
16		fvi	⊢ ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
17	15 16	syl	⊢ ( ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
18	14 17	eqtr4d	⊢ ( ( 𝐼 × 2o ) ∈ V → 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) ) )
19	8 18	syl	⊢ ( 𝐼 ∈ 𝑉 → 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) ) )
20	19	eleq2d	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) )
21	20	biimpa	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) → 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) )
22		eqid	⊢ ( I ‘ Word ( 𝐼 × 2o ) ) = ( I ‘ Word ( 𝐼 × 2o ) )
23		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
24	3 4 22 23	frgpeccl	⊢ ( 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) → [ 𝑥 ] ∼ ∈ ( Base ‘ 𝐺 ) )
25	21 24	syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) → [ 𝑥 ] ∼ ∈ ( Base ‘ 𝐺 ) )
26	25 5	fmptd	⊢ ( 𝐼 ∈ 𝑉 → 𝐹 : 𝑊 ⟶ ( Base ‘ 𝐺 ) )
27	22 4	efger	⊢ ∼ Er ( I ‘ Word ( 𝐼 × 2o ) )
28		ereq2	⊢ ( 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) ) → ( ∼ Er 𝑊 ↔ ∼ Er ( I ‘ Word ( 𝐼 × 2o ) ) ) )
29	19 28	syl	⊢ ( 𝐼 ∈ 𝑉 → ( ∼ Er 𝑊 ↔ ∼ Er ( I ‘ Word ( 𝐼 × 2o ) ) ) )
30	27 29	mpbiri	⊢ ( 𝐼 ∈ 𝑉 → ∼ Er 𝑊 )
31	30	adantr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ∼ Er 𝑊 )
32	2	fvexi	⊢ 𝑊 ∈ V
33	32	a1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → 𝑊 ∈ V )
34	31 33 5	divsfval	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝐹 ‘ ( 𝑎 ++ 𝑏 ) ) = [ ( 𝑎 ++ 𝑏 ) ] ∼ )
35		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
36	1 2 35	frmdadd	⊢ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝑎 ++ 𝑏 ) )
37	36	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝑎 ++ 𝑏 ) )
38	37	fveq2d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑎 ++ 𝑏 ) ) )
39	31 33 5	divsfval	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑎 ) = [ 𝑎 ] ∼ )
40	31 33 5	divsfval	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑏 ) = [ 𝑏 ] ∼ )
41	39 40	oveq12d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) = ( [ 𝑎 ] ∼ ( +g ‘ 𝐺 ) [ 𝑏 ] ∼ ) )
42	19	eleq2d	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑎 ∈ 𝑊 ↔ 𝑎 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) )
43	19	eleq2d	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑏 ∈ 𝑊 ↔ 𝑏 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) )
44	42 43	anbi12d	⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ↔ ( 𝑎 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ∧ 𝑏 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) ) )
45	44	biimpa	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝑎 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ∧ 𝑏 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) )
46		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
47	22 3 4 46	frgpadd	⊢ ( ( 𝑎 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ∧ 𝑏 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) → ( [ 𝑎 ] ∼ ( +g ‘ 𝐺 ) [ 𝑏 ] ∼ ) = [ ( 𝑎 ++ 𝑏 ) ] ∼ )
48	45 47	syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( [ 𝑎 ] ∼ ( +g ‘ 𝐺 ) [ 𝑏 ] ∼ ) = [ ( 𝑎 ++ 𝑏 ) ] ∼ )
49	41 48	eqtrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) = [ ( 𝑎 ++ 𝑏 ) ] ∼ )
50	34 38 49	3eqtr4d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) )
51	50	ralrimivva	⊢ ( 𝐼 ∈ 𝑉 → ∀ 𝑎 ∈ 𝑊 ∀ 𝑏 ∈ 𝑊 ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) )
52	32	a1i	⊢ ( 𝐼 ∈ 𝑉 → 𝑊 ∈ V )
53	30 52 5	divsfval	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 ‘ ∅ ) = [ ∅ ] ∼ )
54	3 4	frgp0	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐺 ∈ Grp ∧ [ ∅ ] ∼ = ( 0g ‘ 𝐺 ) ) )
55	54	simprd	⊢ ( 𝐼 ∈ 𝑉 → [ ∅ ] ∼ = ( 0g ‘ 𝐺 ) )
56	53 55	eqtrd	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 ‘ ∅ ) = ( 0g ‘ 𝐺 ) )
57	26 51 56	3jca	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 : 𝑊 ⟶ ( Base ‘ 𝐺 ) ∧ ∀ 𝑎 ∈ 𝑊 ∀ 𝑏 ∈ 𝑊 ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝐹 ‘ ∅ ) = ( 0g ‘ 𝐺 ) ) )
58	1	frmd0	⊢ ∅ = ( 0g ‘ 𝑀 )
59		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
60	2 23 35 46 58 59	ismhm	⊢ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ↔ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ∈ Mnd ) ∧ ( 𝐹 : 𝑊 ⟶ ( Base ‘ 𝐺 ) ∧ ∀ 𝑎 ∈ 𝑊 ∀ 𝑏 ∈ 𝑊 ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝐹 ‘ ∅ ) = ( 0g ‘ 𝐺 ) ) ) )
61	10 13 57 60	syl21anbrc	⊢ ( 𝐼 ∈ 𝑉 → 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) )