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

Theorem efgredlemd 17406
 Description: The reduced word that forms the base of the sequence in efgsval 17393 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 ++ 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 17392 . . . . . . . 8 Word ..^
98simp1bi 1024 . . . . . . 7 Word
101, 9syl 17 . . . . . 6 Word
1110eldifad 3418 . . . . 5 Word
12 efgredlem.2 . . . . . . . . . 10
132, 3, 4, 5, 6, 7efgsdm 17392 . . . . . . . . . . 11 Word ..^
1413simp1bi 1024 . . . . . . . . . 10 Word
1512, 14syl 17 . . . . . . . . 9 Word
1615eldifad 3418 . . . . . . . 8 Word
17 wrdf 12683 . . . . . . . 8 Word ..^
1816, 17syl 17 . . . . . . 7 ..^
19 fzossfz 11945 . . . . . . . . 9 ..^
20 lencl 12694 . . . . . . . . . . . 12 Word
2116, 20syl 17 . . . . . . . . . . 11
2221nn0zd 11045 . . . . . . . . . 10
23 fzoval 11928 . . . . . . . . . 10 ..^
2422, 23syl 17 . . . . . . . . 9 ..^
2519, 24syl5sseqr 3483 . . . . . . . 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 17402 . . . . . . . . . . 11
3231simpld 461 . . . . . . . . . 10
33 fzo0end 12010 . . . . . . . . . 10 ..^
3432, 33syl 17 . . . . . . . . 9 ..^
3526, 34syl5eqel 2535 . . . . . . . 8 ..^
3625, 35sseldd 3435 . . . . . . 7 ..^
3718, 36ffvelrnd 6028 . . . . . 6
3837s1cld 12749 . . . . 5 Word
39 eldifsn 4100 . . . . . . . 8 Word Word
40 lennncl 12695 . . . . . . . 8 Word
4139, 40sylbi 199 . . . . . . 7 Word
4210, 41syl 17 . . . . . 6
43 lbfzo0 11962 . . . . . 6 ..^
4442, 43sylibr 216 . . . . 5 ..^
45 ccatval1 12729 . . . . 5 Word Word ..^ ++
4611, 38, 44, 45syl3anc 1269 . . . 4 ++
472, 3, 4, 5, 6, 7efgsdm 17392 . . . . . . . . . . 11 Word ..^
4847simp1bi 1024 . . . . . . . . . 10 Word
4928, 48syl 17 . . . . . . . . 9 Word
5049eldifad 3418 . . . . . . . 8 Word
51 wrdf 12683 . . . . . . . 8 Word ..^
5250, 51syl 17 . . . . . . 7 ..^
53 fzossfz 11945 . . . . . . . . 9 ..^
54 lencl 12694 . . . . . . . . . . . 12 Word
5550, 54syl 17 . . . . . . . . . . 11
5655nn0zd 11045 . . . . . . . . . 10
57 fzoval 11928 . . . . . . . . . 10 ..^
5856, 57syl 17 . . . . . . . . 9 ..^
5953, 58syl5sseqr 3483 . . . . . . . 8 ..^ ..^
60 efgredlemb.l . . . . . . . . 9
6131simprd 465 . . . . . . . . . 10
62 fzo0end 12010 . . . . . . . . . 10 ..^
6361, 62syl 17 . . . . . . . . 9 ..^
6460, 63syl5eqel 2535 . . . . . . . 8 ..^
6559, 64sseldd 3435 . . . . . . 7 ..^
6652, 65ffvelrnd 6028 . . . . . 6
6766s1cld 12749 . . . . 5 Word
68 ccatval1 12729 . . . . 5 Word Word ..^ ++
6911, 67, 44, 68syl3anc 1269 . . . 4 ++
7046, 69eqtr4d 2490 . . 3 ++ ++
71 fviss 5928 . . . . . . . . . 10 Word Word
722, 71eqsstri 3464 . . . . . . . . 9 Word
7372, 37sseldi 3432 . . . . . . . 8 Word
74 lencl 12694 . . . . . . . 8 Word
7573, 74syl 17 . . . . . . 7
7675nn0red 10933 . . . . . 6
77 2rp 11314 . . . . . 6
78 ltaddrp 11343 . . . . . 6
7976, 77, 78sylancl 669 . . . . 5
8021nn0red 10933 . . . . . . . . . . 11
8180lem1d 10547 . . . . . . . . . 10
82 fznn 11870 . . . . . . . . . . 11
8322, 82syl 17 . . . . . . . . . 10
8432, 81, 83mpbir2and 934 . . . . . . . . 9
852, 3, 4, 5, 6, 7efgsres 17400 . . . . . . . . 9 ..^
8612, 84, 85syl2anc 667 . . . . . . . 8 ..^
872, 3, 4, 5, 6, 7efgsval 17393 . . . . . . . 8 ..^ ..^ ..^ ..^
8886, 87syl 17 . . . . . . 7 ..^ ..^ ..^
89 1eluzge0 11209 . . . . . . . . . . . . . . 15
90 fzss1 11844 . . . . . . . . . . . . . . 15
9189, 90ax-mp 5 . . . . . . . . . . . . . 14
9291, 84sseldi 3432 . . . . . . . . . . . . 13
93 swrd0val 12784 . . . . . . . . . . . . 13 Word substr ..^
9416, 92, 93syl2anc 667 . . . . . . . . . . . 12 substr ..^
9594fveq2d 5874 . . . . . . . . . . 11 substr ..^
96 swrd0len 12785 . . . . . . . . . . . 12 Word substr
9716, 92, 96syl2anc 667 . . . . . . . . . . 11 substr
9895, 97eqtr3d 2489 . . . . . . . . . 10 ..^
9998oveq1d 6310 . . . . . . . . 9 ..^
10099, 26syl6eqr 2505 . . . . . . . 8 ..^
101100fveq2d 5874 . . . . . . 7 ..^ ..^ ..^
102 fvres 5884 . . . . . . . 8 ..^ ..^
10335, 102syl 17 . . . . . . 7 ..^
10488, 101, 1033eqtrd 2491 . . . . . 6 ..^
105104fveq2d 5874 . . . . 5 ..^
1062, 3, 4, 5, 6, 7efgsdmi 17394 . . . . . . . 8
10712, 32, 106syl2anc 667 . . . . . . 7
10826fveq2i 5873 . . . . . . . . 9
109108fveq2i 5873 . . . . . . . 8
110109rneqi 5064 . . . . . . 7
111107, 110syl6eleqr 2542 . . . . . 6
1122, 3, 4, 5efgtlen 17388 . . . . . 6
11337, 111, 112syl2anc 667 . . . . 5
11479, 105, 1133brtr4d 4436 . . . 4 ..^
115 efgredlemb.p . . . . . . . . 9
116 efgredlemb.q . . . . . . . . 9
117 efgredlemb.u . . . . . . . . 9
118 efgredlemb.v . . . . . . . . 9
119 efgredlemb.6 . . . . . . . . 9
120 efgredlemb.7 . . . . . . . . 9
121 efgredlemb.8 . . . . . . . . 9
122 efgredlemd.9 . . . . . . . . 9
123 efgredlemd.sc . . . . . . . . 9 substr ++ substr
1242, 3, 4, 5, 6, 7, 27, 12, 28, 29, 30, 26, 60, 115, 116, 117, 118, 119, 120, 121, 122, 1, 123efgredleme 17405 . . . . . . . 8
125124simpld 461 . . . . . . 7
1262, 3, 4, 5, 6, 7efgsp1 17399 . . . . . . 7 ++
1271, 125, 126syl2anc 667 . . . . . 6 ++
1282, 3, 4, 5, 6, 7efgsval2 17395 . . . . . 6 Word ++ ++
12911, 37, 127, 128syl3anc 1269 . . . . 5 ++
130104, 129eqtr4d 2490 . . . 4 ..^ ++
131 fveq2 5870 . . . . . . . . 9 ..^ ..^
132131fveq2d 5874 . . . . . . . 8 ..^ ..^
133132breq1d 4415 . . . . . . 7 ..^ ..^
134131eqeq1d 2455 . . . . . . . 8 ..^ ..^
135 fveq1 5869 . . . . . . . . 9 ..^ ..^
136135eqeq1d 2455 . . . . . . . 8 ..^ ..^
137134, 136imbi12d 322 . . . . . . 7 ..^ ..^ ..^
138133, 137imbi12d 322 . . . . . 6 ..^ ..^ ..^ ..^
139 fveq2 5870 . . . . . . . . 9 ++ ++
140139eqeq2d 2463 . . . . . . . 8 ++ ..^ ..^ ++
141 fveq1 5869 . . . . . . . . 9 ++ ++
142141eqeq2d 2463 . . . . . . . 8 ++ ..^ ..^ ++
143140, 142imbi12d 322 . . . . . . 7 ++ ..^ ..^ ..^ ++ ..^ ++
144143imbi2d 318 . . . . . 6 ++ ..^ ..^ ..^ ..^ ..^ ++ ..^ ++
145138, 144rspc2va 3162 . . . . 5 ..^ ++ ..^ ..^ ++ ..^ ++
14686, 127, 27, 145syl21anc 1268 . . . 4 ..^ ..^ ++ ..^ ++
147114, 130, 146mp2d 46 . . 3 ..^ ++
14872, 66sseldi 3432 . . . . . . . 8 Word
149 lencl 12694 . . . . . . . 8 Word
150148, 149syl 17 . . . . . . 7
151150nn0red 10933 . . . . . 6
152 ltaddrp 11343 . . . . . 6
153151, 77, 152sylancl 669 . . . . 5
15455nn0red 10933 . . . . . . . . . . 11
155154lem1d 10547 . . . . . . . . . 10
156 fznn 11870 . . . . . . . . . . 11
15756, 156syl 17 . . . . . . . . . 10
15861, 155, 157mpbir2and 934 . . . . . . . . 9
1592, 3, 4, 5, 6, 7efgsres 17400 . . . . . . . . 9 ..^
16028, 158, 159syl2anc 667 . . . . . . . 8 ..^
1612, 3, 4, 5, 6, 7efgsval 17393 . . . . . . . 8 ..^ ..^ ..^ ..^
162160, 161syl 17 . . . . . . 7 ..^ ..^ ..^
163 fzss1 11844 . . . . . . . . . . . . . . 15
16489, 163ax-mp 5 . . . . . . . . . . . . . 14
165164, 158sseldi 3432 . . . . . . . . . . . . 13
166 swrd0val 12784 . . . . . . . . . . . . 13 Word substr ..^
16750, 165, 166syl2anc 667 . . . . . . . . . . . 12 substr ..^
168167fveq2d 5874 . . . . . . . . . . 11 substr ..^
169 swrd0len 12785 . . . . . . . . . . . 12 Word substr
17050, 165, 169syl2anc 667 . . . . . . . . . . 11 substr
171168, 170eqtr3d 2489 . . . . . . . . . 10 ..^
172171oveq1d 6310 . . . . . . . . 9 ..^
173172, 60syl6eqr 2505 . . . . . . . 8 ..^
174173fveq2d 5874 . . . . . . 7 ..^ ..^ ..^
175 fvres 5884 . . . . . . . 8 ..^ ..^
17664, 175syl 17 . . . . . . 7 ..^
177162, 174, 1763eqtrd 2491 . . . . . 6 ..^
178177fveq2d 5874 . . . . 5 ..^
1792, 3, 4, 5, 6, 7efgsdmi 17394 . . . . . . . . 9
18028, 61, 179syl2anc 667 . . . . . . . 8
18129, 180eqeltrd 2531 . . . . . . 7
18260fveq2i 5873 . . . . . . . . 9
183182fveq2i 5873 . . . . . . . 8
184183rneqi 5064 . . . . . . 7
185181, 184syl6eleqr 2542 . . . . . 6
1862, 3, 4, 5efgtlen 17388 . . . . . 6
18766, 185, 186syl2anc 667 . . . . 5
188153, 178, 1873brtr4d 4436 . . . 4 ..^
189124simprd 465 . . . . . . 7
1902, 3, 4, 5, 6, 7efgsp1 17399 . . . . . . 7 ++
1911, 189, 190syl2anc 667 . . . . . 6 ++
1922, 3, 4, 5, 6, 7efgsval2 17395 . . . . . 6 Word ++ ++
19311, 66, 191, 192syl3anc 1269 . . . . 5 ++
194177, 193eqtr4d 2490 . . . 4 ..^ ++
195 fveq2 5870 . . . . . . . . 9 ..^ ..^
196195fveq2d 5874 . . . . . . . 8 ..^ ..^
197196breq1d 4415 . . . . . . 7 ..^ ..^
198195eqeq1d 2455 . . . . . . . 8 ..^ ..^
199 fveq1 5869 . . . . . . . . 9 ..^ ..^
200199eqeq1d 2455 . . . . . . . 8 ..^ ..^
201198, 200imbi12d 322 . . . . . . 7 ..^ ..^ ..^
202197, 201imbi12d 322 . . . . . 6 ..^ ..^ ..^ ..^
203 fveq2 5870 . . . . . . . . 9 ++ ++
204203eqeq2d 2463 . . . . . . . 8 ++ ..^ ..^ ++
205 fveq1 5869 . . . . . . . . 9 ++ ++
206205eqeq2d 2463 . . . . . . . 8 ++ ..^ ..^ ++
207204, 206imbi12d 322 . . . . . . 7 ++ ..^ ..^ ..^ ++ ..^ ++
208207imbi2d 318 . . . . . 6 ++ ..^ ..^ ..^ ..^ ..^ ++ ..^ ++
209202, 208rspc2va 3162 . . . . 5 ..^ ++ ..^ ..^ ++ ..^ ++
210160, 191, 27, 209syl21anc 1268 . . . 4 ..^ ..^ ++ ..^ ++
211188, 194, 210mp2d 46 . . 3 ..^ ++
21270, 147, 2113eqtr4d 2497 . 2 ..^ ..^
213 lbfzo0 11962 . . . 4 ..^
21432, 213sylibr 216 . . 3 ..^
215 fvres 5884 . . 3 ..^ ..^
216214, 215syl 17 . 2 ..^
217 lbfzo0 11962 . . . 4 ..^
21861, 217sylibr 216 . . 3 ..^
219 fvres 5884 . . 3 ..^ ..^
220218, 219syl 17 . 2 ..^
221212, 216, 2203eqtr3d 2495 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wa 371   wceq 1446   wcel 1889   wne 2624  wral 2739  crab 2743   cdif 3403   wss 3406  c0 3733  csn 3970  cop 3976  cotp 3978  ciun 4281   class class class wbr 4405   cmpt 4464   cid 4747   cxp 4835   cdm 4837   crn 4838   cres 4839  wf 5581  cfv 5585  (class class class)co 6295   cmpt2 6297  c1o 7180  c2o 7181  cr 9543  cc0 9544  c1 9545   caddc 9547   clt 9680   cle 9681   cmin 9865  cn 10616  c2 10666  cn0 10876  cz 10944  cuz 11166  crp 11309  cfz 11791  ..^cfzo 11922  chash 12522  Word cword 12663   ++ cconcat 12665  cs1 12666   substr csubstr 12667   splice csplice 12668  cs2 12944   ~FG cefg 17368 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-cnex 9600  ax-resscn 9601  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-mulcom 9608  ax-addass 9609  ax-mulass 9610  ax-distr 9611  ax-i2m1 9612  ax-1ne0 9613  ax-1rid 9614  ax-rnegex 9615  ax-rrecex 9616  ax-cnre 9617  ax-pre-lttri 9618  ax-pre-lttrn 9619  ax-pre-ltadd 9620  ax-pre-mulgt0 9621 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-ot 3979  df-uni 4202  df-int 4238  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-2o 7188  df-oadd 7191  df-er 7368  df-map 7479  df-pm 7480  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-card 8378  df-cda 8603  df-pnf 9682  df-mnf 9683  df-xr 9684  df-ltxr 9685  df-le 9686  df-sub 9867  df-neg 9868  df-nn 10617  df-2 10675  df-n0 10877  df-z 10945  df-uz 11167  df-rp 11310  df-fz 11792  df-fzo 11923  df-hash 12523  df-word 12671  df-concat 12673  df-s1 12674  df-substr 12675  df-splice 12676  df-s2 12951 This theorem is referenced by:  efgredlemc  17407
 Copyright terms: Public domain W3C validator