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 ⊢ M = freeMnd ⁡ I × 2 𝑜
frgpmhm.w ⊢ W = Base M
frgpmhm.g ⊢ G = freeGrp ⁡ I
frgpmhm.r ⊢ ∼ ˙ = ~ FG ⁡ I
frgpmhm.f ⊢ F = x ∈ W ⟼ x ∼ ˙
Assertion frgpmhm ⊢ I ∈ V → F ∈ M MndHom G

Proof

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