Metamath Proof Explorer


Theorem frgpup1

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) (Revised by Mario Carneiro, 28-Feb-2016)

Ref Expression
Hypotheses frgpup.b B=BaseH
frgpup.n N=invgH
frgpup.t T=yI,z2𝑜ifz=FyNFy
frgpup.h φHGrp
frgpup.i φIV
frgpup.a φF:IB
frgpup.w W=IWordI×2𝑜
frgpup.r ˙=~FGI
frgpup.g G=freeGrpI
frgpup.x X=BaseG
frgpup.e E=rangWg˙HTg
Assertion frgpup1 φEGGrpHomH

Proof

Step Hyp Ref Expression
1 frgpup.b B=BaseH
2 frgpup.n N=invgH
3 frgpup.t T=yI,z2𝑜ifz=FyNFy
4 frgpup.h φHGrp
5 frgpup.i φIV
6 frgpup.a φF:IB
7 frgpup.w W=IWordI×2𝑜
8 frgpup.r ˙=~FGI
9 frgpup.g G=freeGrpI
10 frgpup.x X=BaseG
11 frgpup.e E=rangWg˙HTg
12 eqid +G=+G
13 eqid +H=+H
14 9 frgpgrp IVGGrp
15 5 14 syl φGGrp
16 1 2 3 4 5 6 7 8 9 10 11 frgpupf φE:XB
17 eqid freeMndI×2𝑜=freeMndI×2𝑜
18 9 17 8 frgpval IVG=freeMndI×2𝑜/𝑠˙
19 5 18 syl φG=freeMndI×2𝑜/𝑠˙
20 2on 2𝑜On
21 xpexg IV2𝑜OnI×2𝑜V
22 5 20 21 sylancl φI×2𝑜V
23 wrdexg I×2𝑜VWordI×2𝑜V
24 fvi WordI×2𝑜VIWordI×2𝑜=WordI×2𝑜
25 22 23 24 3syl φIWordI×2𝑜=WordI×2𝑜
26 7 25 eqtrid φW=WordI×2𝑜
27 eqid BasefreeMndI×2𝑜=BasefreeMndI×2𝑜
28 17 27 frmdbas I×2𝑜VBasefreeMndI×2𝑜=WordI×2𝑜
29 22 28 syl φBasefreeMndI×2𝑜=WordI×2𝑜
30 26 29 eqtr4d φW=BasefreeMndI×2𝑜
31 8 fvexi ˙V
32 31 a1i φ˙V
33 fvexd φfreeMndI×2𝑜V
34 19 30 32 33 qusbas φW/˙=BaseG
35 10 34 eqtr4id φX=W/˙
36 eqimss X=W/˙XW/˙
37 35 36 syl φXW/˙
38 37 adantr φaXXW/˙
39 38 sselda φaXcXcW/˙
40 eqid W/˙=W/˙
41 oveq2 u˙=ca+Gu˙=a+Gc
42 41 fveq2d u˙=cEa+Gu˙=Ea+Gc
43 fveq2 u˙=cEu˙=Ec
44 43 oveq2d u˙=cEa+HEu˙=Ea+HEc
45 42 44 eqeq12d u˙=cEa+Gu˙=Ea+HEu˙Ea+Gc=Ea+HEc
46 37 sselda φaXaW/˙
47 46 adantlr φuWaXaW/˙
48 fvoveq1 t˙=aEt˙+Gu˙=Ea+Gu˙
49 fveq2 t˙=aEt˙=Ea
50 49 oveq1d t˙=aEt˙+HEu˙=Ea+HEu˙
51 48 50 eqeq12d t˙=aEt˙+Gu˙=Et˙+HEu˙Ea+Gu˙=Ea+HEu˙
52 fviss IWordI×2𝑜WordI×2𝑜
53 7 52 eqsstri WWordI×2𝑜
54 53 sseli tWtWordI×2𝑜
55 53 sseli uWuWordI×2𝑜
56 ccatcl tWordI×2𝑜uWordI×2𝑜t++uWordI×2𝑜
57 54 55 56 syl2an tWuWt++uWordI×2𝑜
58 7 efgrcl tWIVW=WordI×2𝑜
59 58 adantr tWuWIVW=WordI×2𝑜
60 59 simprd tWuWW=WordI×2𝑜
61 57 60 eleqtrrd tWuWt++uW
62 1 2 3 4 5 6 7 8 9 10 11 frgpupval φt++uWEt++u˙=HTt++u
63 61 62 sylan2 φtWuWEt++u˙=HTt++u
64 54 ad2antrl φtWuWtWordI×2𝑜
65 55 ad2antll φtWuWuWordI×2𝑜
66 1 2 3 4 5 6 frgpuptf φT:I×2𝑜B
67 66 adantr φtWuWT:I×2𝑜B
68 ccatco tWordI×2𝑜uWordI×2𝑜T:I×2𝑜BTt++u=Tt++Tu
69 64 65 67 68 syl3anc φtWuWTt++u=Tt++Tu
70 69 oveq2d φtWuWHTt++u=HTt++Tu
71 4 grpmndd φHMnd
72 71 adantr φtWuWHMnd
73 wrdco tWordI×2𝑜T:I×2𝑜BTtWordB
74 54 66 73 syl2anr φtWTtWordB
75 74 adantrr φtWuWTtWordB
76 wrdco uWordI×2𝑜T:I×2𝑜BTuWordB
77 65 67 76 syl2anc φtWuWTuWordB
78 1 13 gsumccat HMndTtWordBTuWordBHTt++Tu=HTt+HHTu
79 72 75 77 78 syl3anc φtWuWHTt++Tu=HTt+HHTu
80 63 70 79 3eqtrd φtWuWEt++u˙=HTt+HHTu
81 7 9 8 12 frgpadd tWuWt˙+Gu˙=t++u˙
82 81 adantl φtWuWt˙+Gu˙=t++u˙
83 82 fveq2d φtWuWEt˙+Gu˙=Et++u˙
84 1 2 3 4 5 6 7 8 9 10 11 frgpupval φtWEt˙=HTt
85 84 adantrr φtWuWEt˙=HTt
86 1 2 3 4 5 6 7 8 9 10 11 frgpupval φuWEu˙=HTu
87 86 adantrl φtWuWEu˙=HTu
88 85 87 oveq12d φtWuWEt˙+HEu˙=HTt+HHTu
89 80 83 88 3eqtr4d φtWuWEt˙+Gu˙=Et˙+HEu˙
90 89 anass1rs φuWtWEt˙+Gu˙=Et˙+HEu˙
91 40 51 90 ectocld φuWaW/˙Ea+Gu˙=Ea+HEu˙
92 47 91 syldan φuWaXEa+Gu˙=Ea+HEu˙
93 92 an32s φaXuWEa+Gu˙=Ea+HEu˙
94 40 45 93 ectocld φaXcW/˙Ea+Gc=Ea+HEc
95 39 94 syldan φaXcXEa+Gc=Ea+HEc
96 95 anasss φaXcXEa+Gc=Ea+HEc
97 10 1 12 13 15 4 16 96 isghmd φEGGrpHomH