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

Theorem frgpup3lem 15409
 Description: The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
Hypotheses
Ref Expression
frgpup.b
frgpup.n
frgpup.t
frgpup.h
frgpup.i
frgpup.a
frgpup.w Word
frgpup.r ~FG
frgpup.g freeGrp
frgpup.x
frgpup.e g
frgpup.u varFGrp
frgpup3.k
frgpup3.e
Assertion
Ref Expression
frgpup3lem
Distinct variable groups:   ,,   ,   ,,   ,,   ,,,   ,   ,   ,,,   ,,   ,
Allowed substitution hints:   (,)   (,)   (,,)   (,,)   ()   (,,)   (,)   ()   (,,)   ()   (,,)   (,)   (,,)

Proof of Theorem frgpup3lem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frgpup3.k . . 3
2 frgpup.x . . . 4
3 frgpup.b . . . 4
42, 3ghmf 15010 . . 3
5 ffn 5591 . . 3
61, 4, 53syl 19 . 2
7 frgpup.n . . . 4
8 frgpup.t . . . 4
9 frgpup.h . . . 4
10 frgpup.i . . . 4
11 frgpup.a . . . 4
12 frgpup.w . . . 4 Word
13 frgpup.r . . . 4 ~FG
14 frgpup.g . . . 4 freeGrp
15 frgpup.e . . . 4 g
163, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15frgpup1 15407 . . 3
172, 3ghmf 15010 . . 3
18 ffn 5591 . . 3
1916, 17, 183syl 19 . 2
20 eqid 2436 . . . . . . . . 9 freeMnd freeMnd
2114, 20, 13frgpval 15390 . . . . . . . 8 freeMnd s
2210, 21syl 16 . . . . . . 7 freeMnd s
23 2on 6732 . . . . . . . . . . 11
24 xpexg 4989 . . . . . . . . . . 11
2510, 23, 24sylancl 644 . . . . . . . . . 10
26 wrdexg 11739 . . . . . . . . . 10 Word
27 fvi 5783 . . . . . . . . . 10 Word Word Word
2825, 26, 273syl 19 . . . . . . . . 9 Word Word
2912, 28syl5eq 2480 . . . . . . . 8 Word
30 eqid 2436 . . . . . . . . . 10 freeMnd freeMnd
3120, 30frmdbas 14797 . . . . . . . . 9 freeMnd Word
3225, 31syl 16 . . . . . . . 8 freeMnd Word
3329, 32eqtr4d 2471 . . . . . . 7 freeMnd
34 fvex 5742 . . . . . . . . 9 ~FG
3513, 34eqeltri 2506 . . . . . . . 8
3635a1i 11 . . . . . . 7
37 fvex 5742 . . . . . . . 8 freeMnd
3837a1i 11 . . . . . . 7 freeMnd
3922, 33, 36, 38divsbas 13770 . . . . . 6
4039, 2syl6reqr 2487 . . . . 5
41 eqimss 3400 . . . . 5
4240, 41syl 16 . . . 4
4342sselda 3348 . . 3
44 eqid 2436 . . . 4
45 fveq2 5728 . . . . 5
46 fveq2 5728 . . . . 5
4745, 46eqeq12d 2450 . . . 4
48 simpr 448 . . . . . . . . . . . . . 14
4929adantr 452 . . . . . . . . . . . . . 14 Word
5048, 49eleqtrd 2512 . . . . . . . . . . . . 13 Word
51 wrdf 11733 . . . . . . . . . . . . 13 Word ..^
5250, 51syl 16 . . . . . . . . . . . 12 ..^
5352ffvelrnda 5870 . . . . . . . . . . 11 ..^
54 elxp2 4896 . . . . . . . . . . 11
5553, 54sylib 189 . . . . . . . . . 10 ..^
56 fveq2 5728 . . . . . . . . . . . . . . . . 17
5756fveq2d 5732 . . . . . . . . . . . . . . . . 17
5856, 57ifeq12d 3755 . . . . . . . . . . . . . . . 16
59 eqeq1 2442 . . . . . . . . . . . . . . . . 17
6059ifbid 3757 . . . . . . . . . . . . . . . 16
61 fvex 5742 . . . . . . . . . . . . . . . . 17
62 fvex 5742 . . . . . . . . . . . . . . . . 17
6361, 62ifex 3797 . . . . . . . . . . . . . . . 16
6458, 60, 8, 63ovmpt2 6209 . . . . . . . . . . . . . . 15
6564adantl 453 . . . . . . . . . . . . . 14
66 elpri 3834 . . . . . . . . . . . . . . . . 17
67 df2o3 6737 . . . . . . . . . . . . . . . . 17
6866, 67eleq2s 2528 . . . . . . . . . . . . . . . 16
69 frgpup3.e . . . . . . . . . . . . . . . . . . . . . 22
7069adantr 452 . . . . . . . . . . . . . . . . . . . . 21
7170fveq1d 5730 . . . . . . . . . . . . . . . . . . . 20
72 frgpup.u . . . . . . . . . . . . . . . . . . . . . . 23 varFGrp
7313, 72, 14, 2vrgpf 15400 . . . . . . . . . . . . . . . . . . . . . 22
7410, 73syl 16 . . . . . . . . . . . . . . . . . . . . 21
75 fvco3 5800 . . . . . . . . . . . . . . . . . . . . 21
7674, 75sylan 458 . . . . . . . . . . . . . . . . . . . 20
7771, 76eqtr3d 2470 . . . . . . . . . . . . . . . . . . 19
7877adantr 452 . . . . . . . . . . . . . . . . . 18
79 iftrue 3745 . . . . . . . . . . . . . . . . . . 19
8079adantl 453 . . . . . . . . . . . . . . . . . 18
81 simpr 448 . . . . . . . . . . . . . . . . . . . . . . 23
8281opeq2d 3991 . . . . . . . . . . . . . . . . . . . . . 22
8382s1eqd 11754 . . . . . . . . . . . . . . . . . . . . 21
84 eceq1 6941 . . . . . . . . . . . . . . . . . . . . 21
8583, 84syl 16 . . . . . . . . . . . . . . . . . . . 20
8613, 72vrgpval 15399 . . . . . . . . . . . . . . . . . . . . . 22
8710, 86sylan 458 . . . . . . . . . . . . . . . . . . . . 21
8887adantr 452 . . . . . . . . . . . . . . . . . . . 20
8985, 88eqtr4d 2471 . . . . . . . . . . . . . . . . . . 19
9089fveq2d 5732 . . . . . . . . . . . . . . . . . 18
9178, 80, 903eqtr4d 2478 . . . . . . . . . . . . . . . . 17
9277fveq2d 5732 . . . . . . . . . . . . . . . . . . . 20
931adantr 452 . . . . . . . . . . . . . . . . . . . . 21
9474ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . 21
95 eqid 2436 . . . . . . . . . . . . . . . . . . . . . 22
962, 95, 7ghminv 15013 . . . . . . . . . . . . . . . . . . . . 21
9793, 94, 96syl2anc 643 . . . . . . . . . . . . . . . . . . . 20
9892, 97eqtr4d 2471 . . . . . . . . . . . . . . . . . . 19
9998adantr 452 . . . . . . . . . . . . . . . . . 18
100 1n0 6739 . . . . . . . . . . . . . . . . . . . 20
101 simpr 448 . . . . . . . . . . . . . . . . . . . . 21
102101neeq1d 2614 . . . . . . . . . . . . . . . . . . . 20
103100, 102mpbiri 225 . . . . . . . . . . . . . . . . . . 19
104 ifnefalse 3747 . . . . . . . . . . . . . . . . . . 19
105103, 104syl 16 . . . . . . . . . . . . . . . . . 18
106101opeq2d 3991 . . . . . . . . . . . . . . . . . . . . . 22
107106s1eqd 11754 . . . . . . . . . . . . . . . . . . . . 21
108 eceq1 6941 . . . . . . . . . . . . . . . . . . . . 21
109107, 108syl 16 . . . . . . . . . . . . . . . . . . . 20
11013, 72, 14, 95vrgpinv 15401 . . . . . . . . . . . . . . . . . . . . . 22
11110, 110sylan 458 . . . . . . . . . . . . . . . . . . . . 21
112111adantr 452 . . . . . . . . . . . . . . . . . . . 20
113109, 112eqtr4d 2471 . . . . . . . . . . . . . . . . . . 19
114113fveq2d 5732 . . . . . . . . . . . . . . . . . 18
11599, 105, 1143eqtr4d 2478 . . . . . . . . . . . . . . . . 17
11691, 115jaodan 761 . . . . . . . . . . . . . . . 16
11768, 116sylan2 461 . . . . . . . . . . . . . . 15
118117anasss 629 . . . . . . . . . . . . . 14
11965, 118eqtrd 2468 . . . . . . . . . . . . 13
120 fveq2 5728 . . . . . . . . . . . . . . 15
121 df-ov 6084 . . . . . . . . . . . . . . 15
122120, 121syl6eqr 2486 . . . . . . . . . . . . . 14
123 s1eq 11753 . . . . . . . . . . . . . . . 16
124 eceq1 6941 . . . . . . . . . . . . . . . 16
125123, 124syl 16 . . . . . . . . . . . . . . 15
126125fveq2d 5732 . . . . . . . . . . . . . 14
127122, 126eqeq12d 2450 . . . . . . . . . . . . 13
128119, 127syl5ibrcom 214 . . . . . . . . . . . 12
129128rexlimdvva 2837 . . . . . . . . . . 11
130129ad2antrr 707 . . . . . . . . . 10 ..^
13155, 130mpd 15 . . . . . . . . 9 ..^
132131mpteq2dva 4295 . . . . . . . 8 ..^ ..^
1333, 7, 8, 9, 10, 11frgpuptf 15402 . . . . . . . . . 10
134133adantr 452 . . . . . . . . 9
135 fcompt 5904 . . . . . . . . 9 ..^ ..^
136134, 52, 135syl2anc 643 . . . . . . . 8 ..^
13753s1cld 11756 . . . . . . . . . . 11 ..^ Word
13829ad2antrr 707 . . . . . . . . . . 11 ..^ Word
139137, 138eleqtrrd 2513 . . . . . . . . . 10 ..^
14014, 13, 12, 2frgpeccl 15393 . . . . . . . . . 10
141139, 140syl 16 . . . . . . . . 9 ..^
14252feqmptd 5779 . . . . . . . . . . 11 ..^
14310adantr 452 . . . . . . . . . . . . 13
144143, 23, 24sylancl 644 . . . . . . . . . . . 12
145 eqid 2436 . . . . . . . . . . . . 13 varFMnd varFMnd
146145vrmdfval 14801 . . . . . . . . . . . 12 varFMnd
147144, 146syl 16 . . . . . . . . . . 11 varFMnd
148 s1eq 11753 . . . . . . . . . . 11
14953, 142, 147, 148fmptco 5901 . . . . . . . . . 10 varFMnd ..^
150 eqidd 2437 . . . . . . . . . 10
151 eceq1 6941 . . . . . . . . . 10
152139, 149, 150, 151fmptco 5901 . . . . . . . . 9 varFMnd ..^
1531adantr 452 . . . . . . . . . . 11
154153, 4syl 16 . . . . . . . . . 10
155154feqmptd 5779 . . . . . . . . 9
156 fveq2 5728 . . . . . . . . 9
157141, 152, 155, 156fmptco 5901 . . . . . . . 8 varFMnd ..^
158132, 136, 1573eqtr4d 2478 . . . . . . 7 varFMnd
159158oveq2d 6097 . . . . . 6 g g varFMnd
1603, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15frgpupval 15406 . . . . . 6 g
161 ghmmhm 15016 . . . . . . . 8 MndHom
162153, 161syl 16 . . . . . . 7 MndHom
163145vrmdf 14803 . . . . . . . . . . 11 varFMnd Word
164144, 163syl 16 . . . . . . . . . 10 varFMnd Word
165 feq3 5578 . . . . . . . . . . 11 Word varFMnd varFMnd Word
16649, 165syl 16 . . . . . . . . . 10 varFMnd varFMnd Word
167164, 166mpbird 224 . . . . . . . . 9 varFMnd
168 wrdco 11800 . . . . . . . . 9 Word varFMnd varFMnd Word
16950, 167, 168syl2anc 643 . . . . . . . 8 varFMnd Word
17033adantr 452 . . . . . . . . . . . 12 freeMnd
171170mpteq1d 4290 . . . . . . . . . . 11 freeMnd
172 eqid 2436 . . . . . . . . . . . . 13 freeMnd freeMnd
17320, 30, 14, 13, 172frgpmhm 15397 . . . . . . . . . . . 12 freeMnd freeMnd MndHom
174143, 173syl 16 . . . . . . . . . . 11 freeMnd freeMnd MndHom
175171, 174eqeltrd 2510 . . . . . . . . . 10 freeMnd MndHom
17630, 2mhmf 14743 . . . . . . . . . 10 freeMnd MndHom freeMnd
177175, 176syl 16 . . . . . . . . 9 freeMnd
178170feq2d 5581 . . . . . . . . 9 freeMnd
179177, 178mpbird 224 . . . . . . . 8
180 wrdco 11800 . . . . . . . 8 varFMnd Word varFMnd Word
181169, 179, 180syl2anc 643 . . . . . . 7 varFMnd Word
1822gsumwmhm 14790 . . . . . . 7 MndHom varFMnd Word g varFMnd g varFMnd
183162, 181, 182syl2anc 643 . . . . . 6 g varFMnd g varFMnd
184159, 160, 1833eqtr4d 2478 . . . . 5 g varFMnd
18520, 145frmdgsum 14807 . . . . . . . . 9 Word freeMnd g varFMnd
186144, 50, 185syl2anc 643 . . . . . . . 8 freeMnd g varFMnd
187186fveq2d 5732 . . . . . . 7 freeMnd g varFMnd
188 wrdco 11800 . . . . . . . . . 10 Word varFMnd Word varFMnd Word Word
18950, 164, 188syl2anc 643 . . . . . . . . 9 varFMnd Word Word
19032adantr 452 . . . . . . . . . 10 freeMnd Word
191 wrdeq 11738 . . . . . . . . . 10 freeMnd Word Word freeMnd Word Word
192190, 191syl 16 . . . . . . . . 9 Word freeMnd Word Word
193189, 192eleqtrrd 2513 . . . . . . . 8 varFMnd Word freeMnd
19430gsumwmhm 14790 . . . . . . . 8 freeMnd MndHom varFMnd Word freeMnd freeMnd g varFMnd g varFMnd
195175, 193, 194syl2anc 643 . . . . . . 7 freeMnd g varFMnd g varFMnd
19612, 13efger 15350 . . . . . . . . 9
197196a1i 11 . . . . . . . 8
198 fvex 5742 . . . . . . . . . 10 Word
19912, 198eqeltri 2506 . . . . . . . . 9
200199a1i 11 . . . . . . . 8
201 eqid 2436 . . . . . . . 8
202197, 200, 201divsfval 13772 . . . . . . 7
203187, 195, 2023eqtr3d 2476 . . . . . 6 g varFMnd
204203fveq2d 5732 . . . . 5 g varFMnd
205184, 204eqtr2d 2469 . . . 4
20644, 47, 205ectocld 6971 . . 3
20743, 206syldan 457 . 2
2086, 19, 207eqfnfvd 5830 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wo 358   wa 359   wceq 1652   wcel 1725   wne 2599  wrex 2706  cvv 2956   wss 3320  c0 3628  cif 3739  cpr 3815  cop 3817   cmpt 4266   cid 4493  con0 4581   cxp 4876   crn 4879   ccom 4882   wfn 5449  wf 5450  cfv 5454  (class class class)co 6081   cmpt2 6083  c1o 6717  c2o 6718   wer 6902  cec 6903  cqs 6904  cc0 8990  ..^cfzo 11135  chash 11618  Word cword 11717  cs1 11719  cbs 13469   g cgsu 13724   s cqus 13731  cgrp 14685  cminusg 14686   MndHom cmhm 14736  freeMndcfrmd 14792  varFMndcvrmd 14793   cghm 15003   ~FG cefg 15338  freeGrpcfrgp 15339  varFGrpcvrgp 15340 This theorem is referenced by:  frgpup3  15410 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 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701  ax-cnex 9046  ax-resscn 9047  ax-1cn 9048  ax-icn 9049  ax-addcl 9050  ax-addrcl 9051  ax-mulcl 9052  ax-mulrcl 9053  ax-mulcom 9054  ax-addass 9055  ax-mulass 9056  ax-distr 9057  ax-i2m1 9058  ax-1ne0 9059  ax-1rid 9060  ax-rnegex 9061  ax-rrecex 9062  ax-cnre 9063  ax-pre-lttri 9064  ax-pre-lttrn 9065  ax-pre-ltadd 9066  ax-pre-mulgt0 9067 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 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-ot 3824  df-uni 4016  df-int 4051  df-iun 4095  df-iin 4096  df-br 4213  df-opab 4267  df-mpt 4268  df-tr 4303  df-eprel 4494  df-id 4498  df-po 4503  df-so 4504  df-fr 4541  df-we 4543  df-ord 4584  df-on 4585  df-lim 4586  df-suc 4587  df-om 4846  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-1st 6349  df-2nd 6350  df-riota 6549  df-recs 6633  df-rdg 6668  df-1o 6724  df-2o 6725  df-oadd 6728  df-er 6905  df-ec 6907  df-qs 6911  df-map 7020  df-pm 7021  df-en 7110  df-dom 7111  df-sdom 7112  df-fin 7113  df-sup 7446  df-card 7826  df-pnf 9122  df-mnf 9123  df-xr 9124  df-ltxr 9125  df-le 9126  df-sub 9293  df-neg 9294  df-nn 10001  df-2 10058  df-3 10059  df-4 10060  df-5 10061  df-6 10062  df-7 10063  df-8 10064  df-9 10065  df-10 10066  df-n0 10222  df-z 10283  df-dec 10383  df-uz 10489  df-fz 11044  df-fzo 11136  df-seq 11324  df-hash 11619  df-word 11723  df-concat 11724  df-s1 11725  df-substr 11726  df-splice 11727  df-reverse 11728  df-s2 11812  df-struct 13471  df-ndx 13472  df-slot 13473  df-base 13474  df-sets 13475  df-ress 13476  df-plusg 13542  df-mulr 13543  df-sca 13545  df-vsca 13546  df-tset 13548  df-ple 13549  df-ds 13551  df-0g 13727  df-gsum 13728  df-imas 13734  df-divs 13735  df-mnd 14690  df-mhm 14738  df-submnd 14739  df-frmd 14794  df-vrmd 14795  df-grp 14812  df-minusg 14813  df-ghm 15004  df-efg 15341  df-frgp 15342  df-vrgp 15343
 Copyright terms: Public domain W3C validator