Metamath Proof Explorer


Theorem frgpupf

Description: Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses frgpup.b B = Base H
frgpup.n N = inv g H
frgpup.t T = y I , z 2 𝑜 if z = F y N F y
frgpup.h φ H Grp
frgpup.i φ I V
frgpup.a φ F : I B
frgpup.w W = I Word I × 2 𝑜
frgpup.r ˙ = ~ FG I
frgpup.g G = freeGrp I
frgpup.x X = Base G
frgpup.e E = ran g W g ˙ H T g
Assertion frgpupf φ E : X B

Proof

Step Hyp Ref Expression
1 frgpup.b B = Base H
2 frgpup.n N = inv g H
3 frgpup.t T = y I , z 2 𝑜 if z = F y N F y
4 frgpup.h φ H Grp
5 frgpup.i φ I V
6 frgpup.a φ F : I B
7 frgpup.w W = I Word I × 2 𝑜
8 frgpup.r ˙ = ~ FG I
9 frgpup.g G = freeGrp I
10 frgpup.x X = Base G
11 frgpup.e E = ran g W g ˙ H T g
12 grpmnd H Grp H Mnd
13 4 12 syl φ H Mnd
14 fviss I Word I × 2 𝑜 Word I × 2 𝑜
15 7 14 eqsstri W Word I × 2 𝑜
16 15 sseli g W g Word I × 2 𝑜
17 1 2 3 4 5 6 frgpuptf φ T : I × 2 𝑜 B
18 wrdco g Word I × 2 𝑜 T : I × 2 𝑜 B T g Word B
19 16 17 18 syl2anr φ g W T g Word B
20 1 gsumwcl H Mnd T g Word B H T g B
21 13 19 20 syl2an2r φ g W H T g B
22 7 8 efger ˙ Er W
23 22 a1i φ ˙ Er W
24 7 fvexi W V
25 24 a1i φ W V
26 coeq2 g = h T g = T h
27 26 oveq2d g = h H T g = H T h
28 1 2 3 4 5 6 7 8 frgpuplem φ g ˙ h H T g = H T h
29 11 21 23 25 27 28 qliftfund φ Fun E
30 11 21 23 25 qliftf φ Fun E E : W / ˙ B
31 29 30 mpbid φ E : W / ˙ B
32 eqid freeMnd I × 2 𝑜 = freeMnd I × 2 𝑜
33 9 32 8 frgpval I V G = freeMnd I × 2 𝑜 / 𝑠 ˙
34 5 33 syl φ G = freeMnd I × 2 𝑜 / 𝑠 ˙
35 2on 2 𝑜 On
36 xpexg I V 2 𝑜 On I × 2 𝑜 V
37 5 35 36 sylancl φ I × 2 𝑜 V
38 wrdexg I × 2 𝑜 V Word I × 2 𝑜 V
39 fvi Word I × 2 𝑜 V I Word I × 2 𝑜 = Word I × 2 𝑜
40 37 38 39 3syl φ I Word I × 2 𝑜 = Word I × 2 𝑜
41 7 40 syl5eq φ W = Word I × 2 𝑜
42 eqid Base freeMnd I × 2 𝑜 = Base freeMnd I × 2 𝑜
43 32 42 frmdbas I × 2 𝑜 V Base freeMnd I × 2 𝑜 = Word I × 2 𝑜
44 37 43 syl φ Base freeMnd I × 2 𝑜 = Word I × 2 𝑜
45 41 44 eqtr4d φ W = Base freeMnd I × 2 𝑜
46 8 fvexi ˙ V
47 46 a1i φ ˙ V
48 fvexd φ freeMnd I × 2 𝑜 V
49 34 45 47 48 qusbas φ W / ˙ = Base G
50 49 10 syl6reqr φ X = W / ˙
51 50 feq2d φ E : X B E : W / ˙ B
52 31 51 mpbird φ E : X B