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