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

Theorem efgcpbllemb 15064
 Description: Lemma for efgrelex 15060. Show that is an equivalence relation containing all direct extensions of a word, so is closed under . (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 ..^
efgcpbllem.1 concat concat concat concat
Assertion
Ref Expression
efgcpbllemb
Distinct variable groups:   ,,   ,   ,,,,,   ,,,,,,,,   ,,,,,,   ,,,,   ,,,,,,,,,   ,,,,,,,   ,,   ,,   ,,,,,,,,,,   ,,,,
Allowed substitution hints:   (,,,,,,,,)   (,,,,,,,,)   (,,,,,,)   (,,,)   (,,,,,,,,)   (,,,,)   ()   (,,,,,,,,,,)   (,,)

Proof of Theorem efgcpbllemb
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efgval.w . . 3 Word
2 efgval.r . . 3 ~FG
3 efgval2.m . . 3
4 efgval2.t . . 3 splice
51, 2, 3, 4efgval2 15033 . 2
6 efgcpbllem.1 . . . . . . 7 concat concat concat concat
76relopabi 4811 . . . . . 6
87a1i 10 . . . . 5
9 efgred.d . . . . . . . . 9
10 efgred.s . . . . . . . . 9 Word ..^
111, 2, 3, 4, 9, 10, 6efgcpbllema 15063 . . . . . . . 8 concat concat concat concat
1211simp2bi 971 . . . . . . 7
1312adantl 452 . . . . . 6
1411simp1bi 970 . . . . . . 7
1514adantl 452 . . . . . 6
161, 2efger 15027 . . . . . . . 8
1716a1i 10 . . . . . . 7
1811simp3bi 972 . . . . . . . 8 concat concat concat concat
1918adantl 452 . . . . . . 7 concat concat concat concat
2017, 19ersym 6672 . . . . . 6 concat concat concat concat
211, 2, 3, 4, 9, 10, 6efgcpbllema 15063 . . . . . 6 concat concat concat concat
2213, 15, 20, 21syl3anbrc 1136 . . . . 5
2314ad2antrl 708 . . . . . 6
241, 2, 3, 4, 9, 10, 6efgcpbllema 15063 . . . . . . . 8 concat concat concat concat
2524simp2bi 971 . . . . . . 7
2625ad2antll 709 . . . . . 6
2716a1i 10 . . . . . . 7
2818ad2antrl 708 . . . . . . 7 concat concat concat concat
2924simp3bi 972 . . . . . . . 8 concat concat concat concat
3029ad2antll 709 . . . . . . 7 concat concat concat concat
3127, 28, 30ertrd 6676 . . . . . 6 concat concat concat concat
321, 2, 3, 4, 9, 10, 6efgcpbllema 15063 . . . . . 6 concat concat concat concat
3323, 26, 31, 32syl3anbrc 1136 . . . . 5
3416a1i 10 . . . . . . . . 9
35 fviss 5580 . . . . . . . . . . . . . 14 Word Word
361, 35eqsstri 3208 . . . . . . . . . . . . 13 Word
37 simpll 730 . . . . . . . . . . . . 13
3836, 37sseldi 3178 . . . . . . . . . . . 12 Word
39 simpr 447 . . . . . . . . . . . . 13
4036, 39sseldi 3178 . . . . . . . . . . . 12 Word
41 ccatcl 11429 . . . . . . . . . . . 12 Word Word concat Word
4238, 40, 41syl2anc 642 . . . . . . . . . . 11 concat Word
43 simplr 731 . . . . . . . . . . . 12
4436, 43sseldi 3178 . . . . . . . . . . 11 Word
45 ccatcl 11429 . . . . . . . . . . 11 concat Word Word concat concat Word
4642, 44, 45syl2anc 642 . . . . . . . . . 10 concat concat Word
471efgrcl 15024 . . . . . . . . . . . 12 Word
4847simprd 449 . . . . . . . . . . 11 Word
4948ad2antrr 706 . . . . . . . . . 10 Word
5046, 49eleqtrrd 2360 . . . . . . . . 9 concat concat
5134, 50erref 6680 . . . . . . . 8 concat concat concat concat
5251ex 423 . . . . . . 7 concat concat concat concat
5352pm4.71d 615 . . . . . 6 concat concat concat concat
541, 2, 3, 4, 9, 10, 6efgcpbllema 15063 . . . . . . 7 concat concat concat concat
55 df-3an 936 . . . . . . 7 concat concat concat concat concat concat concat concat
56 anidm 625 . . . . . . . 8
5756anbi1i 676 . . . . . . 7 concat concat concat concat concat concat concat concat
5854, 55, 573bitri 262 . . . . . 6 concat concat concat concat
5953, 58syl6bbr 254 . . . . 5
608, 22, 33, 59iserd 6686 . . . 4
611, 2, 3, 4efgtf 15031 . . . . . . . . . 10 splice
6261simprd 449 . . . . . . . . 9
6362adantl 452 . . . . . . . 8
64 ffn 5389 . . . . . . . 8
65 ovelrn 5996 . . . . . . . 8
6663, 64, 653syl 18 . . . . . . 7
67 simplr 731 . . . . . . . . . 10
6862ad2antlr 707 . . . . . . . . . . 11
69 simprl 732 . . . . . . . . . . 11
70 simprr 733 . . . . . . . . . . 11
71 fovrn 5990 . . . . . . . . . . 11
7268, 69, 70, 71syl3anc 1182 . . . . . . . . . 10
7350adantr 451 . . . . . . . . . . 11 concat concat
7437adantr 451 . . . . . . . . . . . . . . . . 17
7536, 74sseldi 3178 . . . . . . . . . . . . . . . 16 Word
7640adantr 451 . . . . . . . . . . . . . . . . 17 Word
77 swrdcl 11452 . . . . . . . . . . . . . . . . 17 Word substr Word
7876, 77syl 15 . . . . . . . . . . . . . . . 16 substr Word
79 ccatcl 11429 . . . . . . . . . . . . . . . 16 Word substr Word concat substr Word
8075, 78, 79syl2anc 642 . . . . . . . . . . . . . . 15 concat substr Word
813efgmf 15022 . . . . . . . . . . . . . . . . . 18
8281ffvelrni 5664 . . . . . . . . . . . . . . . . 17
8382ad2antll 709 . . . . . . . . . . . . . . . 16
8470, 83s2cld 11519 . . . . . . . . . . . . . . 15 Word
85 ccatcl 11429 . . . . . . . . . . . . . . 15 concat substr Word Word concat substr concat Word
8680, 84, 85syl2anc 642 . . . . . . . . . . . . . 14 concat substr concat Word
87 swrdcl 11452 . . . . . . . . . . . . . . 15 Word substr Word
8876, 87syl 15 . . . . . . . . . . . . . 14 substr Word
8944adantr 451 . . . . . . . . . . . . . 14 Word
90 ccatass 11436 . . . . . . . . . . . . . 14 concat substr concat Word substr Word Word concat substr concat concat substr concat concat substr concat concat substr concat
9186, 88, 89, 90syl3anc 1182 . . . . . . . . . . . . 13 concat substr concat concat substr concat concat substr concat concat substr concat
92 ccatcl 11429 . . . . . . . . . . . . . . . . 17 substr Word Word substr concat Word
9378, 84, 92syl2anc 642 . . . . . . . . . . . . . . . 16 substr concat Word
94 ccatass 11436 . . . . . . . . . . . . . . . 16 Word substr concat Word substr Word concat substr concat concat substr concat substr concat concat substr
9575, 93, 88, 94syl3anc 1182 . . . . . . . . . . . . . . 15 concat substr concat concat substr concat substr concat concat substr
96 ccatass 11436 . . . . . . . . . . . . . . . . 17 Word substr Word Word concat substr concat concat substr concat
9775, 78, 84, 96syl3anc 1182 . . . . . . . . . . . . . . . 16 concat substr concat concat substr concat
9897oveq1d 5873 . . . . . . . . . . . . . . 15 concat substr concat concat substr concat substr concat concat substr
991, 2, 3, 4efgtval 15032 . . . . . . . . . . . . . . . . . 18 splice
10067, 69, 70, 99syl3anc 1182 . . . . . . . . . . . . . . . . 17 splice
101 splval 11466 . . . . . . . . . . . . . . . . . 18 Word splice substr concat concat substr
10267, 69, 69, 84, 101syl13anc 1184 . . . . . . . . . . . . . . . . 17 splice substr concat concat substr
103100, 102eqtrd 2315 . . . . . . . . . . . . . . . 16 substr concat concat substr
104103oveq2d 5874 . . . . . . . . . . . . . . 15 concat concat substr concat concat substr
10595, 98, 1043eqtr4rd 2326 . . . . . . . . . . . . . 14 concat concat substr concat concat substr
106105oveq1d 5873 . . . . . . . . . . . . 13 concat concat concat substr concat concat substr concat
107 lencl 11421 . . . . . . . . . . . . . . . . . . 19 Word
10875, 107syl 15 . . . . . . . . . . . . . . . . . 18
109 nn0uz 10262 . . . . . . . . . . . . . . . . . 18
110108, 109syl6eleq 2373 . . . . . . . . . . . . . . . . 17
111 elfznn0 10822 . . . . . . . . . . . . . . . . . 18
112111ad2antrl 708 . . . . . . . . . . . . . . . . 17
113 uzaddcl 10275 . . . . . . . . . . . . . . . . 17
114110, 112, 113syl2anc 642 . . . . . . . . . . . . . . . 16
11542adantr 451 . . . . . . . . . . . . . . . . . 18 concat Word
116 ccatlen 11430 . . . . . . . . . . . . . . . . . 18 concat Word Word concat concat concat
117115, 89, 116syl2anc 642 . . . . . . . . . . . . . . . . 17 concat concat concat
118 ccatlen 11430 . . . . . . . . . . . . . . . . . . . 20 Word Word concat
11975, 76, 118syl2anc 642 . . . . . . . . . . . . . . . . . . 19 concat
120 elfzuz3 10795 . . . . . . . . . . . . . . . . . . . . . 22
121120ad2antrl 708 . . . . . . . . . . . . . . . . . . . . 21
122108nn0zd 10115 . . . . . . . . . . . . . . . . . . . . 21
123 eluzadd 10256 . . . . . . . . . . . . . . . . . . . . 21
124121, 122, 123syl2anc 642 . . . . . . . . . . . . . . . . . . . 20
125 lencl 11421 . . . . . . . . . . . . . . . . . . . . . . . 24 Word
12676, 125syl 15 . . . . . . . . . . . . . . . . . . . . . . 23
127126nn0cnd 10020 . . . . . . . . . . . . . . . . . . . . . 22
128108nn0cnd 10020 . . . . . . . . . . . . . . . . . . . . . 22
129127, 128addcomd 9014 . . . . . . . . . . . . . . . . . . . . 21
130112nn0cnd 10020 . . . . . . . . . . . . . . . . . . . . . . 23
131130, 128addcomd 9014 . . . . . . . . . . . . . . . . . . . . . 22
132131fveq2d 5529 . . . . . . . . . . . . . . . . . . . . 21
133129, 132eleq12d 2351 . . . . . . . . . . . . . . . . . . . 20
134124, 133mpbid 201 . . . . . . . . . . . . . . . . . . 19
135119, 134eqeltrd 2357 . . . . . . . . . . . . . . . . . 18 concat
136 lencl 11421 . . . . . . . . . . . . . . . . . . 19 Word
13789, 136syl 15 . . . . . . . . . . . . . . . . . 18
138 uzaddcl 10275 . . . . . . . . . . . . . . . . . 18 concat concat
139135, 137, 138syl2anc 642 . . . . . . . . . . . . . . . . 17 concat
140117, 139eqeltrd 2357 . . . . . . . . . . . . . . . 16 concat concat
141 elfzuzb 10792 . . . . . . . . . . . . . . . 16 concat concat concat concat
142114, 140, 141sylanbrc 645 . . . . . . . . . . . . . . 15 concat concat
1431, 2, 3, 4efgtval 15032 . . . . . . . . . . . . . . 15 concat concat concat concat concat concat concat concat splice
14473, 142, 70, 143syl3anc 1182 . . . . . . . . . . . . . 14 concat concat concat concat splice
145 wrd0 11418 . . . . . . . . . . . . . . . 16 Word
146145a1i 10 . . . . . . . . . . . . . . 15 Word
147 ccatcl 11429 . . . . . . . . . . . . . . . 16 substr Word Word substr concat Word
14888, 89, 147syl2anc 642 . . . . . . . . . . . . . . 15 substr concat Word
149 ccatrid 11435 . . . . . . . . . . . . . . . . . 18 concat substr Word concat substr concat concat substr
15080, 149syl 15 . . . . . . . . . . . . . . . . 17 concat substr concat concat substr
151150oveq1d 5873 . . . . . . . . . . . . . . . 16 concat substr concat concat substr concat concat substr concat substr concat
152 ccatass 11436 . . . . . . . . . . . . . . . . 17 concat substr Word substr Word Word concat substr concat substr concat concat substr concat substr concat
15380, 88, 89, 152syl3anc 1182 . . . . . . . . . . . . . . . 16 concat substr concat substr concat concat substr concat substr concat
154 ccatass 11436 . . . . . . . . . . . . . . . . . . 19 Word substr Word substr Word concat substr concat substr concat substr concat substr
15575, 78, 88, 154syl3anc 1182 . . . . . . . . . . . . . . . . . 18 concat substr concat substr concat substr concat substr
156112, 109syl6eleq 2373 . . . . . . . . . . . . . . . . . . . . . 22
157 eluzfz1 10803 . . . . . . . . . . . . . . . . . . . . . 22
158156, 157syl 15 . . . . . . . . . . . . . . . . . . . . 21
159126, 109syl6eleq 2373 . . . . . . . . . . . . . . . . . . . . . 22
160 eluzfz2 10804 . . . . . . . . . . . . . . . . . . . . . 22
161159, 160syl 15 . . . . . . . . . . . . . . . . . . . . 21
162 ccatswrd 11459 . . . . . . . . . . . . . . . . . . . . 21 Word substr concat substr substr
16376, 158, 69, 161, 162syl13anc 1184 . . . . . . . . . . . . . . . . . . . 20 substr concat substr substr
164 swrdid 11458 . . . . . . . . . . . . . . . . . . . . 21 Word substr
16576, 164syl 15 . . . . . . . . . . . . . . . . . . . 20 substr
166163, 165eqtrd 2315 . . . . . . . . . . . . . . . . . . 19 substr concat substr
167166oveq2d 5874 . . . . . . . . . . . . . . . . . 18 concat substr concat substr concat
168155, 167eqtrd 2315 . . . . . . . . . . . . . . . . 17 concat substr concat substr concat
169168oveq1d 5873 . . . . . . . . . . . . . . . 16 concat substr concat substr concat concat concat
170151, 153, 1693eqtr2rd 2322 . . . . . . . . . . . . . . 15 concat concat concat substr concat concat substr concat
171 ccatlen 11430 . . . . . . . . . . . . . . . . 17 Word substr Word concat substr substr
17275, 78, 171syl2anc 642 . . . . . . . . . . . . . . . 16 concat substr substr
173 swrd0len 11455 . . . . . . . . . . . . . . . . . 18 Word substr
17476, 69, 173syl2anc 642 . . . . . . . . . . . . . . . . 17 substr
175174oveq2d 5874 . . . . . . . . . . . . . . . 16 substr
176172, 175eqtr2d 2316 . . . . . . . . . . . . . . 15 concat substr
177 hash0 11355 . . . . . . . . . . . . . . . . 17
178177oveq2i 5869 . . . . . . . . . . . . . . . 16
179108, 112nn0addcld 10022 . . . . . . . . . . . . . . . . . 18
180179nn0cnd 10020 . . . . . . . . . . . . . . . . 17
181180addid1d 9012 . . . . . . . . . . . . . . . 16
182178, 181syl5req 2328 . . . . . . . . . . . . . . 15
18380, 146, 148, 84, 170, 176, 182splval2 11472 . . . . . . . . . . . . . 14 concat concat splice concat substr concat concat substr concat
184144, 183eqtrd 2315 . . . . . . . . . . . . 13 concat concat concat substr concat concat substr concat
18591, 106, 1843eqtr4d 2325 . . . . . . . . . . . 12 concat concat concat concat
1861, 2, 3, 4efgtf 15031 . . . . . . . . . . . . . . 15 concat concat concat concat concat concat concat concat splice concat concat concat concat
187186simprd 449 . . . . . . . . . . . . . 14 concat concat concat concat concat concat
188 ffn 5389 . . . . . . . . . . . . . 14 concat concat concat concat concat concat concat concat
18973, 187, 1883syl 18 . . . . . . . . . . . . 13 concat concat concat concat
190 fnovrn 5995 . . . . . . . . . . . . 13 concat concat concat concat concat concat concat concat concat concat
191189, 142, 70, 190syl3anc 1182 . . . . . . . . . . . 12 concat concat concat concat
192185, 191eqeltrd 2357 . . . . . . . . . . 11 concat concat concat concat
1931, 2, 3, 4efgi2 15034 . . . . . . . . . . 11 concat concat concat concat concat concat concat concat concat concat
19473, 192, 193syl2anc 642 . . . . . . . . . 10 concat concat concat concat
1951, 2, 3, 4, 9, 10, 6efgcpbllema 15063 . . . . . . . . . 10 concat concat concat concat
19667, 72, 194, 195syl3anbrc 1136 . . . . . . . . 9
197 vex 2791 . . . . . . . . . . 11
198 vex 2791 . . . . . . . . . . 11
199197, 198elec 6699 . . . . . . . . . 10
200 breq2 4027 . . . . . . . . . 10
201199, 200syl5bb 248 . . . . . . . . 9
202196, 201syl5ibrcom 213 . . . . . . . 8
203202rexlimdvva 2674 . . . . . . 7
20466, 203sylbid 206 . . . . . 6
205204ssrdv 3185 . . . . 5
206205ralrimiva 2626 . . . 4
207 fvex 5539 . . . . . . 7 Word
2081, 207eqeltri 2353 . . . . . 6
209 erex 6684 . . . . . 6
21060, 208, 209ee10 1366 . . . . 5
211 ereq1 6667 . . . . . . 7
212 eceq2 6697 . . . . . . . . 9
213212sseq2d 3206 . . . . . . . 8
214213ralbidv 2563 . . . . . . 7
215211, 214anbi12d 691 . . . . . 6
216215elabg 2915 . . . . 5
217210, 216syl 15 . . . 4
21860, 206, 217mpbir2and 888 . . 3
219 intss1 3877 . . 3
220218, 219syl 15 . 2
2215, 220syl5eqss 3222 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1623   wcel 1684  cab 2269  wral 2543  wrex 2544  crab 2547  cvv 2788   cdif 3149   wss 3152  c0 3455  csn 3640  cpr 3641  cop 3643  cotp 3644  cint 3862  ciun 3905   class class class wbr 4023  copab 4076   cmpt 4077   cid 4304   cxp 4687   crn 4690   wrel 4694   wfn 5250  wf 5251  cfv 5255  (class class class)co 5858   cmpt2 5860  c1o 6472  c2o 6473   wer 6657  cec 6658  cc0 8737  c1 8738   caddc 8740   cmin 9037  cn0 9965  cz 10024  cuz 10230  cfz 10782  ..^cfzo 10870  chash 11337  Word cword 11403   concat cconcat 11404   substr csubstr 11406   splice csplice 11407  cs2 11491   ~FG cefg 15015 This theorem is referenced by:  efgcpbl  15065 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-ot 3650  df-uni 3828  df-int 3863  df-iun 3907  df-iin 3908  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-2o 6480  df-oadd 6483  df-er 6660  df-ec 6662  df-map 6774  df-pm 6775  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-card 7572  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-nn 9747  df-n0 9966  df-z 10025  df-uz 10231  df-fz 10783  df-fzo 10871  df-hash 11338  df-word 11409  df-concat 11410  df-s1 11411  df-substr 11412  df-splice 11413  df-s2 11498  df-efg 15018
 Copyright terms: Public domain W3C validator