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

Theorem efgred 17336
 Description: The reduced word that forms the base of the sequence in efgsval 17319 is uniquely determined, given the terminal point. (Contributed by Mario Carneiro, 28-Sep-2015.)
Hypotheses
Ref Expression
efgval.w Word
efgval.r ~FG
efgval2.m
efgval2.t splice
efgred.d
efgred.s Word ..^
Assertion
Ref Expression
efgred
Distinct variable groups:   ,   ,,,,,,,   ,   ,,,,,   ,,,,   ,,,,,,,,,   ,,,,,   ,,,,,,,,   ,,
Allowed substitution hints:   (,,,,,,,,)   (,,,,,,,,)   (,,,,,,)   (,,,)   (,,,,,,,,)   (,,,,)   ()   (,,)

Proof of Theorem efgred
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efgval.w . . . . . . . 8 Word
2 fviss 5878 . . . . . . . 8 Word Word
31, 2eqsstri 3432 . . . . . . 7 Word
4 efgval.r . . . . . . . . . . 11 ~FG
5 efgval2.m . . . . . . . . . . 11
6 efgval2.t . . . . . . . . . . 11 splice
7 efgred.d . . . . . . . . . . 11
8 efgred.s . . . . . . . . . . 11 Word ..^
91, 4, 5, 6, 7, 8efgsf 17317 . . . . . . . . . 10 Word ..^
109fdmi 5689 . . . . . . . . . . 11 Word ..^
1110feq2i 5677 . . . . . . . . . 10 Word ..^
129, 11mpbir 212 . . . . . . . . 9
1312ffvelrni 5975 . . . . . . . 8
1413adantr 466 . . . . . . 7
153, 14sseldi 3400 . . . . . 6 Word
16 lencl 12630 . . . . . 6 Word
1715, 16syl 17 . . . . 5
18 peano2nn0 10856 . . . . 5
1917, 18syl 17 . . . 4
20 breq2 4365 . . . . . . 7
2120imbi1d 318 . . . . . 6
22212ralbidv 2804 . . . . 5
23 breq2 4365 . . . . . . 7
2423imbi1d 318 . . . . . 6
25242ralbidv 2804 . . . . 5
26 breq2 4365 . . . . . . 7
2726imbi1d 318 . . . . . 6
28272ralbidv 2804 . . . . 5
29 breq2 4365 . . . . . . 7
3029imbi1d 318 . . . . . 6
31302ralbidv 2804 . . . . 5
3212ffvelrni 5975 . . . . . . . . . . 11
333, 32sseldi 3400 . . . . . . . . . 10 Word
34 lencl 12630 . . . . . . . . . 10 Word
3533, 34syl 17 . . . . . . . . 9
36 nn0nlt0 10842 . . . . . . . . 9
3735, 36syl 17 . . . . . . . 8
3837pm2.21d 109 . . . . . . 7
3938adantr 466 . . . . . 6
4039rgen2a 2787 . . . . 5
41 simpl1 1008 . . . . . . . . . . . . . 14
42 simpl3l 1060 . . . . . . . . . . . . . . 15
43 breq2 4365 . . . . . . . . . . . . . . . . 17
4443imbi1d 318 . . . . . . . . . . . . . . . 16
45442ralbidv 2804 . . . . . . . . . . . . . . 15
4642, 45syl 17 . . . . . . . . . . . . . 14
4741, 46mpbird 235 . . . . . . . . . . . . 13
48 simpl2l 1058 . . . . . . . . . . . . 13
49 simpl2r 1059 . . . . . . . . . . . . 13
50 simpl3r 1061 . . . . . . . . . . . . 13
51 simpr 462 . . . . . . . . . . . . 13
521, 4, 5, 6, 7, 8, 47, 48, 49, 50, 51efgredlem 17335 . . . . . . . . . . . 12
53 iman 425 . . . . . . . . . . . 12
5452, 53mpbir 212 . . . . . . . . . . 11
55543expia 1207 . . . . . . . . . 10
5655expd 437 . . . . . . . . 9
5756ralrimivva 2781 . . . . . . . 8
58 fveq2 5820 . . . . . . . . . . . 12
5958fveq2d 5824 . . . . . . . . . . 11
6059eqeq1d 2425 . . . . . . . . . 10
6158eqeq1d 2425 . . . . . . . . . . 11
62 fveq1 5819 . . . . . . . . . . . 12
6362eqeq1d 2425 . . . . . . . . . . 11
6461, 63imbi12d 321 . . . . . . . . . 10
6560, 64imbi12d 321 . . . . . . . . 9
66 fveq2 5820 . . . . . . . . . . . 12
6766eqeq2d 2433 . . . . . . . . . . 11
68 fveq1 5819 . . . . . . . . . . . 12
6968eqeq2d 2433 . . . . . . . . . . 11
7067, 69imbi12d 321 . . . . . . . . . 10
7170imbi2d 317 . . . . . . . . 9
7265, 71cbvral2v 2999 . . . . . . . 8
7357, 72sylib 199 . . . . . . 7
7473ancli 553 . . . . . 6
7535adantr 466 . . . . . . . . . . 11
76 nn0leltp1 10941 . . . . . . . . . . . . 13
77 nn0re 10824 . . . . . . . . . . . . . 14
78 nn0re 10824 . . . . . . . . . . . . . 14
79 leloe 9666 . . . . . . . . . . . . . 14
8077, 78, 79syl2an 479 . . . . . . . . . . . . 13
8176, 80bitr3d 258 . . . . . . . . . . . 12
8281ancoms 454 . . . . . . . . . . 11
8375, 82sylan2 476 . . . . . . . . . 10
8483imbi1d 318 . . . . . . . . 9
85 jaob 790 . . . . . . . . 9
8684, 85syl6bb 264 . . . . . . . 8
87862ralbidva 2802 . . . . . . 7
88 r19.26-2 2890 . . . . . . 7
8987, 88syl6bb 264 . . . . . 6
9074, 89syl5ibr 224 . . . . 5
9122, 25, 28, 31, 40, 90nn0ind 10976 . . . 4
9219, 91syl 17 . . 3
9317nn0red 10872 . . . 4
9493ltp1d 10483 . . 3
95 fveq2 5820 . . . . . . 7
9695fveq2d 5824 . . . . . 6
9796breq1d 4371 . . . . 5
9895eqeq1d 2425 . . . . . 6
99 fveq1 5819 . . . . . . 7
10099eqeq1d 2425 . . . . . 6
10198, 100imbi12d 321 . . . . 5
10297, 101imbi12d 321 . . . 4
103 fveq2 5820 . . . . . . 7
104103eqeq2d 2433 . . . . . 6
105 fveq1 5819 . . . . . . 7
106105eqeq2d 2433 . . . . . 6
107104, 106imbi12d 321 . . . . 5
108107imbi2d 317 . . . 4
109102, 108rspc2v 3129 . . 3
11092, 94, 109mp2d 46 . 2
1111103impia 1202 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wo 369   wa 370   w3a 982   wceq 1437   wcel 1872  wral 2709  crab 2713   cdif 3371  c0 3699  csn 3936  cop 3942  cotp 3944  ciun 4237   class class class wbr 4361   cmpt 4420   cid 4701   cxp 4789   cdm 4791   crn 4792  wf 5535  cfv 5539  (class class class)co 6244   cmpt2 6246  c1o 7125  c2o 7126  cr 9484  cc0 9485  c1 9486   caddc 9488   clt 9621   cle 9622   cmin 9806  cn0 10815  cfz 11730  ..^cfzo 11861  chash 12460  Word cword 12599   splice csplice 12604  cs2 12878   ~FG cefg 17294 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-ot 3945  df-uni 4158  df-int 4194  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-1st 6746  df-2nd 6747  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-2o 7133  df-oadd 7136  df-er 7313  df-map 7424  df-pm 7425  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-card 8320  df-cda 8544  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-nn 10556  df-2 10614  df-n0 10816  df-z 10884  df-uz 11106  df-rp 11249  df-fz 11731  df-fzo 11862  df-hash 12461  df-word 12607  df-concat 12609  df-s1 12610  df-substr 12611  df-splice 12612  df-s2 12885 This theorem is referenced by:  efgrelexlemb  17338
 Copyright terms: Public domain W3C validator