Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  frgpuplem Structured version   Unicode version

Theorem frgpuplem 15396
 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.)
Hypotheses
Ref Expression
frgpup.b
frgpup.n
frgpup.t
frgpup.h
frgpup.i
frgpup.a
frgpup.w Word
frgpup.r ~FG
Assertion
Ref Expression
frgpuplem g g
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)   (,)   (,)

Proof of Theorem frgpuplem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frgpup.w . . . . . . 7 Word
2 frgpup.r . . . . . . 7 ~FG
31, 2efgval 15341 . . . . . 6 splice
4 coeq2 5023 . . . . . . . . . . . . 13
54oveq2d 6089 . . . . . . . . . . . 12 g g
6 eqid 2435 . . . . . . . . . . . 12 g g g g
75, 6eqer 6930 . . . . . . . . . . 11 g g
87a1i 11 . . . . . . . . . 10 g g
9 ssv 3360 . . . . . . . . . . 11
109a1i 11 . . . . . . . . . 10
118, 10erinxp 6970 . . . . . . . . 9 g g
12 df-xp 4876 . . . . . . . . . . . . 13
1312ineq1i 3530 . . . . . . . . . . . 12 g g g g
14 incom 3525 . . . . . . . . . . . 12 g g g g
15 inopab 4997 . . . . . . . . . . . 12 g g g g
1613, 14, 153eqtr3i 2463 . . . . . . . . . . 11 g g g g
17 vex 2951 . . . . . . . . . . . . . 14
18 vex 2951 . . . . . . . . . . . . . 14
1917, 18prss 3944 . . . . . . . . . . . . 13
2019anbi1i 677 . . . . . . . . . . . 12 g g g g
2120opabbii 4264 . . . . . . . . . . 11 g g g g
2216, 21eqtri 2455 . . . . . . . . . 10 g g g g
23 ereq1 6904 . . . . . . . . . 10 g g g g g g g g
2422, 23ax-mp 8 . . . . . . . . 9 g g g g
2511, 24sylib 189 . . . . . . . 8 g g
26 simplrl 737 . . . . . . . . . . . 12
27 fviss 5776 . . . . . . . . . . . . . . . 16 Word Word
281, 27eqsstri 3370 . . . . . . . . . . . . . . 15 Word
2928, 26sseldi 3338 . . . . . . . . . . . . . 14 Word
30 opelxpi 4902 . . . . . . . . . . . . . . . 16
3130adantl 453 . . . . . . . . . . . . . . 15
32 simprl 733 . . . . . . . . . . . . . . . 16
33 2oconcl 6739 . . . . . . . . . . . . . . . . 17
3433ad2antll 710 . . . . . . . . . . . . . . . 16
35 opelxpi 4902 . . . . . . . . . . . . . . . 16
3632, 34, 35syl2anc 643 . . . . . . . . . . . . . . 15
3731, 36s2cld 11825 . . . . . . . . . . . . . 14 Word
38 splcl 11773 . . . . . . . . . . . . . 14 Word Word splice Word
3929, 37, 38syl2anc 643 . . . . . . . . . . . . 13 splice Word
401efgrcl 15339 . . . . . . . . . . . . . . 15 Word
4126, 40syl 16 . . . . . . . . . . . . . 14 Word
4241simprd 450 . . . . . . . . . . . . 13 Word
4339, 42eleqtrrd 2512 . . . . . . . . . . . 12 splice
4426, 43jca 519 . . . . . . . . . . 11 splice
45 swrdcl 11758 . . . . . . . . . . . . . . . . . 18 Word substr Word
4629, 45syl 16 . . . . . . . . . . . . . . . . 17 substr Word
47 frgpup.b . . . . . . . . . . . . . . . . . . 19
48 frgpup.n . . . . . . . . . . . . . . . . . . 19
49 frgpup.t . . . . . . . . . . . . . . . . . . 19
50 frgpup.h . . . . . . . . . . . . . . . . . . 19
51 frgpup.i . . . . . . . . . . . . . . . . . . 19
52 frgpup.a . . . . . . . . . . . . . . . . . . 19
5347, 48, 49, 50, 51, 52frgpuptf 15394 . . . . . . . . . . . . . . . . . 18
5453ad2antrr 707 . . . . . . . . . . . . . . . . 17
55 ccatco 11796 . . . . . . . . . . . . . . . . 17 substr Word Word substr concat substr concat
5646, 37, 54, 55syl3anc 1184 . . . . . . . . . . . . . . . 16 substr concat substr concat
5756oveq2d 6089 . . . . . . . . . . . . . . 15 g substr concat g substr concat
5850ad2antrr 707 . . . . . . . . . . . . . . . . 17
59 grpmnd 14809 . . . . . . . . . . . . . . . . 17
6058, 59syl 16 . . . . . . . . . . . . . . . 16
61 wrdco 11792 . . . . . . . . . . . . . . . . 17 substr Word substr Word
6246, 54, 61syl2anc 643 . . . . . . . . . . . . . . . 16 substr Word
63 wrdco 11792 . . . . . . . . . . . . . . . . 17 Word Word
6437, 54, 63syl2anc 643 . . . . . . . . . . . . . . . 16 Word
65 eqid 2435 . . . . . . . . . . . . . . . . 17
6647, 65gsumccat 14779 . . . . . . . . . . . . . . . 16 substr Word Word g substr concat g substr g
6760, 62, 64, 66syl3anc 1184 . . . . . . . . . . . . . . 15 g substr concat g substr g
6854, 31, 36s2co 11859 . . . . . . . . . . . . . . . . . . . 20
69 df-ov 6076 . . . . . . . . . . . . . . . . . . . . . 22
7069a1i 11 . . . . . . . . . . . . . . . . . . . . 21
71 df-ov 6076 . . . . . . . . . . . . . . . . . . . . . . . . . 26
72 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7372efgmval 15336 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7471, 73syl5eqr 2481 . . . . . . . . . . . . . . . . . . . . . . . . 25
7574adantl 453 . . . . . . . . . . . . . . . . . . . . . . . 24
7675fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . 23
7747, 48, 49, 50, 51, 52, 72frgpuptinv 15395 . . . . . . . . . . . . . . . . . . . . . . . . 25
7830, 77sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . 24
7978adantlr 696 . . . . . . . . . . . . . . . . . . . . . . 23
8076, 79eqtr3d 2469 . . . . . . . . . . . . . . . . . . . . . 22
8169fveq2i 5723 . . . . . . . . . . . . . . . . . . . . . 22
8280, 81syl6reqr 2486 . . . . . . . . . . . . . . . . . . . . 21
8370, 82s2eqd 11818 . . . . . . . . . . . . . . . . . . . 20
8468, 83eqtr4d 2470 . . . . . . . . . . . . . . . . . . 19
8584oveq2d 6089 . . . . . . . . . . . . . . . . . 18 g g
86 simprr 734 . . . . . . . . . . . . . . . . . . . 20
8754, 32, 86fovrnd 6210 . . . . . . . . . . . . . . . . . . 19
8847, 48grpinvcl 14842 . . . . . . . . . . . . . . . . . . . 20
8958, 87, 88syl2anc 643 . . . . . . . . . . . . . . . . . . 19
9047, 65gsumws2 14780 . . . . . . . . . . . . . . . . . . 19 g
9160, 87, 89, 90syl3anc 1184 . . . . . . . . . . . . . . . . . 18 g
92 eqid 2435 . . . . . . . . . . . . . . . . . . . 20
9347, 65, 92, 48grprinv 14844 . . . . . . . . . . . . . . . . . . 19
9458, 87, 93syl2anc 643 . . . . . . . . . . . . . . . . . 18
9585, 91, 943eqtrd 2471 . . . . . . . . . . . . . . . . 17 g
9695oveq2d 6089 . . . . . . . . . . . . . . . 16 g substr g g substr
9747gsumwcl 14778 . . . . . . . . . . . . . . . . . 18 substr Word g substr
9860, 62, 97syl2anc 643 . . . . . . . . . . . . . . . . 17 g substr
9947, 65, 92grprid 14828 . . . . . . . . . . . . . . . . 17 g substr g substr g substr
10058, 98, 99syl2anc 643 . . . . . . . . . . . . . . . 16 g substr g substr
10196, 100eqtrd 2467 . . . . . . . . . . . . . . 15 g substr g g substr
10257, 67, 1013eqtrrd 2472 . . . . . . . . . . . . . 14 g substr g substr concat
103102oveq1d 6088 . . . . . . . . . . . . 13 g substr g substr g substr concat g substr
104 swrdcl 11758 . . . . . . . . . . . . . . . 16 Word substr Word
10529, 104syl 16 . . . . . . . . . . . . . . 15 substr Word
106 wrdco 11792 . . . . . . . . . . . . . . 15 substr Word substr Word
107105, 54, 106syl2anc 643 . . . . . . . . . . . . . 14 substr Word
10847, 65gsumccat 14779 . . . . . . . . . . . . . 14 substr Word substr Word g substr concat substr g substr g substr
10960, 62, 107, 108syl3anc 1184 . . . . . . . . . . . . 13 g substr concat substr g substr g substr
110 ccatcl 11735 . . . . . . . . . . . . . . . 16 substr Word Word substr concat Word
11146, 37, 110syl2anc 643 . . . . . . . . . . . . . . 15 substr concat Word
112 wrdco 11792 . . . . . . . . . . . . . . 15 substr concat Word substr concat Word
113111, 54, 112syl2anc 643 . . . . . . . . . . . . . 14 substr concat Word
11447, 65gsumccat 14779 . . . . . . . . . . . . . 14 substr concat Word substr Word g substr concat concat substr g substr concat g substr
11560, 113, 107, 114syl3anc 1184 . . . . . . . . . . . . 13 g substr concat concat substr g substr concat g substr
116103, 109, 1153eqtr4d 2477 . . . . . . . . . . . 12 g substr concat substr g substr concat concat substr
117 simplrr 738 . . . . . . . . . . . . . . . . . 18
118 elfzuz 11047 . . . . . . . . . . . . . . . . . 18
119 eluzfz1 11056 . . . . . . . . . . . . . . . . . 18
120117, 118, 1193syl 19 . . . . . . . . . . . . . . . . 17
121 lencl 11727 . . . . . . . . . . . . . . . . . . . 20 Word
12229, 121syl 16 . . . . . . . . . . . . . . . . . . 19
123 nn0uz 10512 . . . . . . . . . . . . . . . . . . 19
124122, 123syl6eleq 2525 . . . . . . . . . . . . . . . . . 18
125 eluzfz2 11057 . . . . . . . . . . . . . . . . . 18
126124, 125syl 16 . . . . . . . . . . . . . . . . 17
127 ccatswrd 11765 . . . . . . . . . . . . . . . . 17 Word substr concat substr substr
12829, 120, 117, 126, 127syl13anc 1186 . . . . . . . . . . . . . . . 16 substr concat substr substr
129 swrdid 11764 . . . . . . . . . . . . . . . . 17 Word substr
13029, 129syl 16 . . . . . . . . . . . . . . . 16 substr
131128, 130eqtrd 2467 . . . . . . . . . . . . . . 15 substr concat substr
132131coeq2d 5027 . . . . . . . . . . . . . 14 substr concat substr
133 ccatco 11796 . . . . . . . . . . . . . . 15 substr Word substr Word substr concat substr substr concat substr
13446, 105, 54, 133syl3anc 1184 . . . . . . . . . . . . . 14 substr concat substr substr concat substr
135132, 134eqtr3d 2469 . . . . . . . . . . . . 13 substr concat substr
136135oveq2d 6089 . . . . . . . . . . . 12 g g substr concat substr
137 splval 11772 . . . . . . . . . . . . . . . 16 Word splice substr concat concat substr
13826, 117, 117, 37, 137syl13anc 1186 . . . . . . . . . . . . . . 15 splice substr concat concat substr
139138coeq2d 5027 . . . . . . . . . . . . . 14 splice substr concat concat substr
140 ccatco 11796 . . . . . . . . . . . . . . 15 substr concat Word substr Word substr concat concat substr substr concat concat substr
141111, 105, 54, 140syl3anc 1184 . . . . . . . . . . . . . 14 substr concat concat substr substr concat concat substr
142139, 141eqtrd 2467 . . . . . . . . . . . . 13 splice substr concat concat substr
143142oveq2d 6089 . . . . . . . . . . . 12 g splice g substr concat concat substr
144116, 136, 1433eqtr4d 2477 . . . . . . . . . . 11 g g splice
145 vex 2951 . . . . . . . . . . . 12
146 ovex 6098 . . . . . . . . . . . 12 splice
147 eleq1 2495 . . . . . . . . . . . . . . 15
148 eleq1 2495 . . . . . . . . . . . . . . 15 splice splice
149147, 148bi2anan9 844 . . . . . . . . . . . . . 14 splice splice
15019, 149syl5bbr 251 . . . . . . . . . . . . 13 splice splice
151 coeq2 5023 . . . . . . . . . . . . . . 15
152151oveq2d 6089 . . . . . . . . . . . . . 14 g g
153 coeq2 5023 . . . . . . . . . . . . . . 15 splice splice
154153oveq2d 6089 . . . . . . . . . . . . . 14 splice g g splice
155152, 154eqeqan12d 2450 . . . . . . . . . . . . 13 splice g g g g splice
156150, 155anbi12d 692 . . . . . . . . . . . 12 splice g g splice g g splice
157 eqid 2435 . . . . . . . . . . . 12 g g g g
158145, 146, 156, 157braba 4464 . . . . . . . . . . 11 g g splice splice g g splice
15944, 144, 158sylanbrc 646 . . . . . . . . . 10 g g splice
160159ralrimivva 2790 . . . . . . . . 9 g g splice
161160ralrimivva 2790 . . . . . . . 8 g g splice
162 fvex 5734 . . . . . . . . . . 11 Word
1631, 162eqeltri 2505 . . . . . . . . . 10
164 erex 6921 . . . . . . . . . 10 g g g g
16525, 163, 164ee10 1385 . . . . . . . . 9 g g
166 ereq1 6904 . . . . . . . . . . 11 g g g g
167 breq 4206 . . . . . . . . . . . . 13 g g splice g g splice
1681672ralbidv 2739 . . . . . . . . . . . 12 g g splice g g splice
1691682ralbidv 2739 . . . . . . . . . . 11 g g splice g g splice
170166, 169anbi12d 692 . . . . . . . . . 10 g g splice g g g g splice
171170elabg 3075 . . . . . . . . 9 g g g g splice g g g g splice
172165, 171syl 16 . . . . . . . 8 g g splice g g g g splice
17325, 161, 172mpbir2and 889 . . . . . . 7 g g splice
174 intss1 4057 . . . . . . 7 g g splice splice g g
175173, 174syl 16 . . . . . 6 splice g g
1763, 175syl5eqss 3384 . . . . 5 g g
177176ssbrd 4245 . . . 4 g g
178177imp 419 . . 3 g g
1791, 2efger 15342 . . . . . 6
180 errel 6906 . . . . . 6
181179, 180mp1i 12 . . . . 5
182 brrelex12 4907 . . . . 5
183181, 182sylan 458 . . . 4
184 preq12 3877 . . . . . . 7
185184sseq1d 3367 . . . . . 6
186 coeq2 5023 . . . . . . . 8
187186oveq2d 6089 . . . . . . 7 g g
188 coeq2 5023 . . . . . . . 8
189188oveq2d 6089 . . . . . . 7 g g
190187, 189eqeqan12d 2450 . . . . . 6 g g g g
191185, 190anbi12d 692 . . . . 5 g g g g
192191, 157brabga 4461 . . . 4 g g g g
193183, 192syl 16 . . 3 g g g g
194178, 193mpbid 202 . 2 g g
195194simprd 450 1 g g
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1652   wcel 1725  cab 2421  wral 2697  cvv 2948   cdif 3309   cin 3311   wss 3312  c0 3620  cif 3731  cpr 3807  cop 3809  cotp 3810  cint 4042   class class class wbr 4204  copab 4257   cid 4485   cxp 4868   ccom 4874   wrel 4875  wf 5442  cfv 5446  (class class class)co 6073   cmpt2 6075  c1o 6709  c2o 6710   wer 6894  cc0 8982  cn0 10213  cuz 10480  cfz 11035  chash 11610  Word cword 11709   concat cconcat 11710   substr csubstr 11712   splice csplice 11713  cs2 11797  cbs 13461   cplusg 13521  c0g 13715   g cgsu 13716  cmnd 14676  cgrp 14677  cminusg 14678   ~FG cefg 15330 This theorem is referenced by:  frgpupf  15397 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-cnex 9038  ax-resscn 9039  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-mulcom 9046  ax-addass 9047  ax-mulass 9048  ax-distr 9049  ax-i2m1 9050  ax-1ne0 9051  ax-1rid 9052  ax-rnegex 9053  ax-rrecex 9054  ax-cnre 9055  ax-pre-lttri 9056  ax-pre-lttrn 9057  ax-pre-ltadd 9058  ax-pre-mulgt0 9059 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-ot 3816  df-uni 4008  df-int 4043  df-iun 4087  df-iin 4088  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-1o 6716  df-2o 6717  df-oadd 6720  df-er 6897  df-map 7012  df-pm 7013  df-en 7102  df-dom 7103  df-sdom 7104  df-fin 7105  df-card 7818  df-pnf 9114  df-mnf 9115  df-xr 9116  df-ltxr 9117  df-le 9118  df-sub 9285  df-neg 9286  df-nn 9993  df-2 10050  df-n0 10214  df-z 10275  df-uz 10481  df-fz 11036  df-fzo 11128  df-seq 11316  df-hash 11611  df-word 11715  df-concat 11716  df-s1 11717  df-substr 11718  df-splice 11719  df-s2 11804  df-ndx 13464  df-slot 13465  df-base 13466  df-sets 13467  df-ress 13468  df-plusg 13534  df-0g 13719  df-gsum 13720  df-mnd 14682  df-submnd 14731  df-grp 14804  df-minusg 14805  df-efg 15333
 Copyright terms: Public domain W3C validator