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

Metamath Proof Explorer

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 𝐺 ) )