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

Theorem efgredlemd 15368
 Description: The reduced word that forms the base of the sequence in efgsval 15355 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015.)
Hypotheses
Ref Expression
efgval.w Word
efgval.r ~FG
efgval2.m
efgval2.t splice
efgred.d
efgred.s Word ..^
efgredlem.1
efgredlem.2
efgredlem.3
efgredlem.4
efgredlem.5
efgredlemb.k
efgredlemb.l
efgredlemb.p
efgredlemb.q
efgredlemb.u
efgredlemb.v
efgredlemb.6
efgredlemb.7
efgredlemb.8
efgredlemd.9
efgredlemd.c
efgredlemd.sc substr concat substr
Assertion
Ref Expression
efgredlemd
Distinct variable groups:   ,,   ,,,   ,,   ,,   ,,,,,,   ,,,,,,,,   ,,,,,   ,,,,,,   ,,,,,   ,,,,,,   ,,   ,,,,,,,,,   ,,,,,,,   ,,   ,,,,,,,,,,,   ,,   ,,,,,,,,,,   ,,,,
Allowed substitution hints:   (,,,,,,,,,,)   (,,,,,,,,)   (,,,,,,,,)   (,,,,,,)   (,,,,)   (,,,,)   (,,,)   (,,,,,,,,)   (,,,,)   (,,,,,)   ()   (,,,,,,,,)   (,,,,,,,,)   (,,)   (,,,,,)

Proof of Theorem efgredlemd
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 efgredlemd.c . . . . . . 7
2 efgval.w . . . . . . . . 9 Word
3 efgval.r . . . . . . . . 9 ~FG
4 efgval2.m . . . . . . . . 9
5 efgval2.t . . . . . . . . 9 splice
6 efgred.d . . . . . . . . 9
7 efgred.s . . . . . . . . 9 Word ..^
82, 3, 4, 5, 6, 7efgsdm 15354 . . . . . . . 8 Word ..^
98simp1bi 972 . . . . . . 7 Word
101, 9syl 16 . . . . . 6 Word
1110eldifad 3324 . . . . 5 Word
12 efgredlem.2 . . . . . . . . . 10
132, 3, 4, 5, 6, 7efgsdm 15354 . . . . . . . . . . 11 Word ..^
1413simp1bi 972 . . . . . . . . . 10 Word
1512, 14syl 16 . . . . . . . . 9 Word
1615eldifad 3324 . . . . . . . 8 Word
17 wrdf 11725 . . . . . . . 8 Word ..^
1816, 17syl 16 . . . . . . 7 ..^
19 fzossfz 11149 . . . . . . . . 9 ..^
20 lencl 11727 . . . . . . . . . . . 12 Word
2116, 20syl 16 . . . . . . . . . . 11
2221nn0zd 10365 . . . . . . . . . 10
23 fzoval 11133 . . . . . . . . . 10 ..^
2422, 23syl 16 . . . . . . . . 9 ..^
2519, 24syl5sseqr 3389 . . . . . . . 8 ..^ ..^
26 efgredlemb.k . . . . . . . . 9
27 efgredlem.1 . . . . . . . . . . . 12
28 efgredlem.3 . . . . . . . . . . . 12
29 efgredlem.4 . . . . . . . . . . . 12
30 efgredlem.5 . . . . . . . . . . . 12
312, 3, 4, 5, 6, 7, 27, 12, 28, 29, 30efgredlema 15364 . . . . . . . . . . 11
3231simpld 446 . . . . . . . . . 10
33 fzo0end 11180 . . . . . . . . . 10 ..^
3432, 33syl 16 . . . . . . . . 9 ..^
3526, 34syl5eqel 2519 . . . . . . . 8 ..^
3625, 35sseldd 3341 . . . . . . 7 ..^
3718, 36ffvelrnd 5863 . . . . . 6
3837s1cld 11748 . . . . 5 Word
39 eldifsn 3919 . . . . . . . 8 Word Word
40 lennncl 11728 . . . . . . . 8 Word
4139, 40sylbi 188 . . . . . . 7 Word
4210, 41syl 16 . . . . . 6
43 lbfzo0 11162 . . . . . 6 ..^
4442, 43sylibr 204 . . . . 5 ..^
45 ccatval1 11737 . . . . 5 Word Word ..^ concat
4611, 38, 44, 45syl3anc 1184 . . . 4 concat
472, 3, 4, 5, 6, 7efgsdm 15354 . . . . . . . . . . 11 Word ..^
4847simp1bi 972 . . . . . . . . . 10 Word
4928, 48syl 16 . . . . . . . . 9 Word
5049eldifad 3324 . . . . . . . 8 Word
51 wrdf 11725 . . . . . . . 8 Word ..^
5250, 51syl 16 . . . . . . 7 ..^
53 fzossfz 11149 . . . . . . . . 9 ..^
54 lencl 11727 . . . . . . . . . . . 12 Word
5550, 54syl 16 . . . . . . . . . . 11
5655nn0zd 10365 . . . . . . . . . 10
57 fzoval 11133 . . . . . . . . . 10 ..^
5856, 57syl 16 . . . . . . . . 9 ..^
5953, 58syl5sseqr 3389 . . . . . . . 8 ..^ ..^
60 efgredlemb.l . . . . . . . . 9
6131simprd 450 . . . . . . . . . 10
62 fzo0end 11180 . . . . . . . . . 10 ..^
6361, 62syl 16 . . . . . . . . 9 ..^
6460, 63syl5eqel 2519 . . . . . . . 8 ..^
6559, 64sseldd 3341 . . . . . . 7 ..^
6652, 65ffvelrnd 5863 . . . . . 6
6766s1cld 11748 . . . . 5 Word
68 ccatval1 11737 . . . . 5 Word Word ..^ concat
6911, 67, 44, 68syl3anc 1184 . . . 4 concat
7046, 69eqtr4d 2470 . . 3 concat concat
71 fviss 5776 . . . . . . . . . 10 Word Word
722, 71eqsstri 3370 . . . . . . . . 9 Word
7372, 37sseldi 3338 . . . . . . . 8 Word
74 lencl 11727 . . . . . . . 8 Word
7573, 74syl 16 . . . . . . 7
7675nn0red 10267 . . . . . 6
77 2rp 10609 . . . . . 6
78 ltaddrp 10636 . . . . . 6
7976, 77, 78sylancl 644 . . . . 5
8021nn0red 10267 . . . . . . . . . . 11
8180lem1d 9936 . . . . . . . . . 10
82 fznn 11107 . . . . . . . . . . 11
8322, 82syl 16 . . . . . . . . . 10
8432, 81, 83mpbir2and 889 . . . . . . . . 9
852, 3, 4, 5, 6, 7efgsres 15362 . . . . . . . . 9 ..^
8612, 84, 85syl2anc 643 . . . . . . . 8 ..^
872, 3, 4, 5, 6, 7efgsval 15355 . . . . . . . 8 ..^ ..^ ..^ ..^
8886, 87syl 16 . . . . . . 7 ..^ ..^ ..^
89 1nn0 10229 . . . . . . . . . . . . . . . 16
90 nn0uz 10512 . . . . . . . . . . . . . . . 16
9189, 90eleqtri 2507 . . . . . . . . . . . . . . 15
92 fzss1 11083 . . . . . . . . . . . . . . 15
9391, 92ax-mp 8 . . . . . . . . . . . . . 14
9493, 84sseldi 3338 . . . . . . . . . . . . 13
95 swrd0val 11760 . . . . . . . . . . . . 13 Word substr ..^
9616, 94, 95syl2anc 643 . . . . . . . . . . . 12 substr ..^
9796fveq2d 5724 . . . . . . . . . . 11 substr ..^
98 swrd0len 11761 . . . . . . . . . . . 12 Word substr
9916, 94, 98syl2anc 643 . . . . . . . . . . 11 substr
10097, 99eqtr3d 2469 . . . . . . . . . 10 ..^
101100oveq1d 6088 . . . . . . . . 9 ..^
102101, 26syl6eqr 2485 . . . . . . . 8 ..^
103102fveq2d 5724 . . . . . . 7 ..^ ..^ ..^
104 fvres 5737 . . . . . . . 8 ..^ ..^
10535, 104syl 16 . . . . . . 7 ..^
10688, 103, 1053eqtrd 2471 . . . . . 6 ..^
107106fveq2d 5724 . . . . 5 ..^
1082, 3, 4, 5, 6, 7efgsdmi 15356 . . . . . . . 8
10912, 32, 108syl2anc 643 . . . . . . 7
11026fveq2i 5723 . . . . . . . . 9
111110fveq2i 5723 . . . . . . . 8
112111rneqi 5088 . . . . . . 7
113109, 112syl6eleqr 2526 . . . . . 6
1142, 3, 4, 5efgtlen 15350 . . . . . 6
11537, 113, 114syl2anc 643 . . . . 5
11679, 107, 1153brtr4d 4234 . . . 4 ..^
117 efgredlemb.p . . . . . . . . 9
118 efgredlemb.q . . . . . . . . 9
119 efgredlemb.u . . . . . . . . 9
120 efgredlemb.v . . . . . . . . 9
121 efgredlemb.6 . . . . . . . . 9
122 efgredlemb.7 . . . . . . . . 9
123 efgredlemb.8 . . . . . . . . 9
124 efgredlemd.9 . . . . . . . . 9
125 efgredlemd.sc . . . . . . . . 9 substr concat substr
1262, 3, 4, 5, 6, 7, 27, 12, 28, 29, 30, 26, 60, 117, 118, 119, 120, 121, 122, 123, 124, 1, 125efgredleme 15367 . . . . . . . 8
127126simpld 446 . . . . . . 7
1282, 3, 4, 5, 6, 7efgsp1 15361 . . . . . . 7 concat
1291, 127, 128syl2anc 643 . . . . . 6 concat
1302, 3, 4, 5, 6, 7efgsval2 15357 . . . . . 6 Word concat concat
13111, 37, 129, 130syl3anc 1184 . . . . 5 concat
132106, 131eqtr4d 2470 . . . 4 ..^ concat
133 fveq2 5720 . . . . . . . . 9 ..^ ..^
134133fveq2d 5724 . . . . . . . 8 ..^ ..^
135134breq1d 4214 . . . . . . 7 ..^ ..^
136133eqeq1d 2443 . . . . . . . 8 ..^ ..^
137 fveq1 5719 . . . . . . . . 9 ..^ ..^
138137eqeq1d 2443 . . . . . . . 8 ..^ ..^
139136, 138imbi12d 312 . . . . . . 7 ..^ ..^ ..^
140135, 139imbi12d 312 . . . . . 6 ..^ ..^ ..^ ..^
141 fveq2 5720 . . . . . . . . 9 concat concat
142141eqeq2d 2446 . . . . . . . 8 concat ..^ ..^ concat
143 fveq1 5719 . . . . . . . . 9 concat concat
144143eqeq2d 2446 . . . . . . . 8 concat ..^ ..^ concat
145142, 144imbi12d 312 . . . . . . 7 concat ..^ ..^ ..^ concat ..^ concat
146145imbi2d 308 . . . . . 6 concat ..^ ..^ ..^ ..^ ..^ concat ..^ concat
147140, 146rspc2va 3051 . . . . 5 ..^ concat ..^ ..^ concat ..^ concat
14886, 129, 27, 147syl21anc 1183 . . . 4 ..^ ..^ concat ..^ concat
149116, 132, 148mp2d 43 . . 3 ..^ concat
15072, 66sseldi 3338 . . . . . . . 8 Word
151 lencl 11727 . . . . . . . 8 Word
152150, 151syl 16 . . . . . . 7
153152nn0red 10267 . . . . . 6
154 ltaddrp 10636 . . . . . 6
155153, 77, 154sylancl 644 . . . . 5
15655nn0red 10267 . . . . . . . . . . 11
157156lem1d 9936 . . . . . . . . . 10
158 fznn 11107 . . . . . . . . . . 11
15956, 158syl 16 . . . . . . . . . 10
16061, 157, 159mpbir2and 889 . . . . . . . . 9
1612, 3, 4, 5, 6, 7efgsres 15362 . . . . . . . . 9 ..^
16228, 160, 161syl2anc 643 . . . . . . . 8 ..^
1632, 3, 4, 5, 6, 7efgsval 15355 . . . . . . . 8 ..^ ..^ ..^ ..^
164162, 163syl 16 . . . . . . 7 ..^ ..^ ..^
165 fzss1 11083 . . . . . . . . . . . . . . 15
16691, 165ax-mp 8 . . . . . . . . . . . . . 14
167166, 160sseldi 3338 . . . . . . . . . . . . 13
168 swrd0val 11760 . . . . . . . . . . . . 13 Word substr ..^
16950, 167, 168syl2anc 643 . . . . . . . . . . . 12 substr ..^
170169fveq2d 5724 . . . . . . . . . . 11 substr ..^
171 swrd0len 11761 . . . . . . . . . . . 12 Word substr
17250, 167, 171syl2anc 643 . . . . . . . . . . 11 substr
173170, 172eqtr3d 2469 . . . . . . . . . 10 ..^
174173oveq1d 6088 . . . . . . . . 9 ..^
175174, 60syl6eqr 2485 . . . . . . . 8 ..^
176175fveq2d 5724 . . . . . . 7 ..^ ..^ ..^
177 fvres 5737 . . . . . . . 8 ..^ ..^
17864, 177syl 16 . . . . . . 7 ..^
179164, 176, 1783eqtrd 2471 . . . . . 6 ..^
180179fveq2d 5724 . . . . 5 ..^
1812, 3, 4, 5, 6, 7efgsdmi 15356 . . . . . . . . 9
18228, 61, 181syl2anc 643 . . . . . . . 8
18329, 182eqeltrd 2509 . . . . . . 7
18460fveq2i 5723 . . . . . . . . 9
185184fveq2i 5723 . . . . . . . 8
186185rneqi 5088 . . . . . . 7
187183, 186syl6eleqr 2526 . . . . . 6
1882, 3, 4, 5efgtlen 15350 . . . . . 6
18966, 187, 188syl2anc 643 . . . . 5
190155, 180, 1893brtr4d 4234 . . . 4 ..^
191126simprd 450 . . . . . . 7
1922, 3, 4, 5, 6, 7efgsp1 15361 . . . . . . 7 concat
1931, 191, 192syl2anc 643 . . . . . 6 concat
1942, 3, 4, 5, 6, 7efgsval2 15357 . . . . . 6 Word concat concat
19511, 66, 193, 194syl3anc 1184 . . . . 5 concat
196179, 195eqtr4d 2470 . . . 4 ..^ concat
197 fveq2 5720 . . . . . . . . 9 ..^ ..^
198197fveq2d 5724 . . . . . . . 8 ..^ ..^
199198breq1d 4214 . . . . . . 7 ..^ ..^
200197eqeq1d 2443 . . . . . . . 8 ..^ ..^
201 fveq1 5719 . . . . . . . . 9 ..^ ..^
202201eqeq1d 2443 . . . . . . . 8 ..^ ..^
203200, 202imbi12d 312 . . . . . . 7 ..^ ..^ ..^
204199, 203imbi12d 312 . . . . . 6 ..^ ..^ ..^ ..^
205 fveq2 5720 . . . . . . . . 9 concat concat
206205eqeq2d 2446 . . . . . . . 8 concat ..^ ..^ concat
207 fveq1 5719 . . . . . . . . 9 concat concat
208207eqeq2d 2446 . . . . . . . 8 concat ..^ ..^ concat
209206, 208imbi12d 312 . . . . . . 7 concat ..^ ..^ ..^ concat ..^ concat
210209imbi2d 308 . . . . . 6 concat ..^ ..^ ..^ ..^ ..^ concat ..^ concat
211204, 210rspc2va 3051 . . . . 5 ..^ concat ..^ ..^ concat ..^ concat
212162, 193, 27, 211syl21anc 1183 . . . 4 ..^ ..^ concat ..^ concat
213190, 196, 212mp2d 43 . . 3 ..^ concat
21470, 149, 2133eqtr4d 2477 . 2 ..^ ..^
215 lbfzo0 11162 . . . 4 ..^
21632, 215sylibr 204 . . 3 ..^
217 fvres 5737 . . 3 ..^ ..^
218216, 217syl 16 . 2 ..^
219 lbfzo0 11162 . . . 4 ..^
22061, 219sylibr 204 . . 3 ..^
221 fvres 5737 . . 3 ..^ ..^
222220, 221syl 16 . 2 ..^
223214, 218, 2223eqtr3d 2475 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   wceq 1652   wcel 1725   wne 2598  wral 2697  crab 2701   cdif 3309   wss 3312  c0 3620  csn 3806  cop 3809  cotp 3810  ciun 4085   class class class wbr 4204   cmpt 4258   cid 4485   cxp 4868   cdm 4870   crn 4871   cres 4872  wf 5442  cfv 5446  (class class class)co 6073   cmpt2 6075  c1o 6709  c2o 6710  cr 8981  cc0 8982  c1 8983   caddc 8985   clt 9112   cle 9113   cmin 9283  cn 9992  c2 10041  cn0 10213  cz 10274  cuz 10480  crp 10604  cfz 11035  ..^cfzo 11127  chash 11610  Word cword 11709   concat cconcat 11710  cs1 11711   substr csubstr 11712   splice csplice 11713  cs2 11797   ~FG cefg 15330 This theorem is referenced by:  efgredlemc  15369 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-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-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-rp 10605  df-fz 11036  df-fzo 11128  df-hash 11611  df-word 11715  df-concat 11716  df-s1 11717  df-substr 11718  df-splice 11719  df-s2 11804
 Copyright terms: Public domain W3C validator