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

Theorem revccat 12398
 Description: Antiautomorphic property of the reversal operation. (Contributed by Stefan O'Rear, 27-Aug-2015.)
Assertion
Ref Expression
revccat Word Word reverse concat reverse concat reverse

Proof of Theorem revccat
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ccatcl 12266 . . . 4 Word Word concat Word
2 revcl 12393 . . . 4 concat Word reverse concat Word
3 wrdf 12232 . . . 4 reverse concat Word reverse concat ..^reverse concat
4 ffn 5554 . . . 4 reverse concat ..^reverse concat reverse concat ..^reverse concat
51, 2, 3, 44syl 21 . . 3 Word Word reverse concat ..^reverse concat
6 revlen 12394 . . . . . . 7 concat Word reverse concat concat
71, 6syl 16 . . . . . 6 Word Word reverse concat concat
8 ccatlen 12267 . . . . . . 7 Word Word concat
9 lencl 12241 . . . . . . . . 9 Word
109nn0cnd 10630 . . . . . . . 8 Word
11 lencl 12241 . . . . . . . . 9 Word
1211nn0cnd 10630 . . . . . . . 8 Word
13 addcom 9547 . . . . . . . 8
1410, 12, 13syl2an 477 . . . . . . 7 Word Word
158, 14eqtrd 2470 . . . . . 6 Word Word concat
167, 15eqtrd 2470 . . . . 5 Word Word reverse concat
1716oveq2d 6102 . . . 4 Word Word ..^reverse concat ..^
1817fneq2d 5497 . . 3 Word Word reverse concat ..^reverse concat reverse concat ..^
195, 18mpbid 210 . 2 Word Word reverse concat ..^
20 revcl 12393 . . . . 5 Word reverse Word
21 revcl 12393 . . . . 5 Word reverse Word
22 ccatcl 12266 . . . . 5 reverse Word reverse Word reverse concat reverse Word
2320, 21, 22syl2anr 478 . . . 4 Word Word reverse concat reverse Word
24 wrdf 12232 . . . 4 reverse concat reverse Word reverse concat reverse..^reverse concat reverse
25 ffn 5554 . . . 4 reverse concat reverse..^reverse concat reverse reverse concat reverse ..^reverse concat reverse
2623, 24, 253syl 20 . . 3 Word Word reverse concat reverse ..^reverse concat reverse
27 ccatlen 12267 . . . . . . 7 reverse Word reverse Word reverse concat reverse reverse reverse
2820, 21, 27syl2anr 478 . . . . . 6 Word Word reverse concat reverse reverse reverse
29 revlen 12394 . . . . . . 7 Word reverse
30 revlen 12394 . . . . . . 7 Word reverse
3129, 30oveqan12rd 6106 . . . . . 6 Word Word reverse reverse
3228, 31eqtrd 2470 . . . . 5 Word Word reverse concat reverse
3332oveq2d 6102 . . . 4 Word Word ..^reverse concat reverse ..^
3433fneq2d 5497 . . 3 Word Word reverse concat reverse ..^reverse concat reverse reverse concat reverse ..^
3526, 34mpbid 210 . 2 Word Word reverse concat reverse ..^
36 id 22 . . . 4 ..^ ..^
3711nn0zd 10737 . . . . 5 Word
3837adantl 466 . . . 4 Word Word
39 fzospliti 11573 . . . 4 ..^ ..^ ..^
4036, 38, 39syl2anr 478 . . 3 Word Word ..^ ..^ ..^
41 simpll 753 . . . . . . 7 Word Word ..^ Word
42 simplr 754 . . . . . . 7 Word Word ..^ Word
43 fzoval 11546 . . . . . . . . . . . 12 ..^
4438, 43syl 16 . . . . . . . . . . 11 Word Word ..^
4544eleq2d 2505 . . . . . . . . . 10 Word Word ..^
4645biimpa 484 . . . . . . . . 9 Word Word ..^
47 fznn0sub2 11480 . . . . . . . . 9
4846, 47syl 16 . . . . . . . 8 Word Word ..^
4944adantr 465 . . . . . . . 8 Word Word ..^ ..^
5048, 49eleqtrrd 2515 . . . . . . 7 Word Word ..^ ..^
51 ccatval3 12270 . . . . . . 7 Word Word ..^ concat
5241, 42, 50, 51syl3anc 1218 . . . . . 6 Word Word ..^ concat
5315oveq1d 6101 . . . . . . . . . . 11 Word Word concat
5412adantl 466 . . . . . . . . . . . 12 Word Word
5510adantr 465 . . . . . . . . . . . 12 Word Word
56 ax-1cn 9332 . . . . . . . . . . . . 13
5756a1i 11 . . . . . . . . . . . 12 Word Word
5854, 55, 57addsubd 9732 . . . . . . . . . . 11 Word Word
5953, 58eqtrd 2470 . . . . . . . . . 10 Word Word concat
6059oveq1d 6101 . . . . . . . . 9 Word Word concat
6160adantr 465 . . . . . . . 8 Word Word ..^ concat
62 peano2zm 10680 . . . . . . . . . . . 12
6337, 62syl 16 . . . . . . . . . . 11 Word
6463zcnd 10740 . . . . . . . . . 10 Word
6564ad2antlr 726 . . . . . . . . 9 Word Word ..^
6610ad2antrr 725 . . . . . . . . 9 Word Word ..^
67 elfzoelz 11545 . . . . . . . . . . 11 ..^
6867zcnd 10740 . . . . . . . . . 10 ..^
6968adantl 466 . . . . . . . . 9 Word Word ..^
7065, 66, 69addsubd 9732 . . . . . . . 8 Word Word ..^
7161, 70eqtrd 2470 . . . . . . 7 Word Word ..^ concat
7271fveq2d 5690 . . . . . 6 Word Word ..^ concat concat concat
73 revfv 12395 . . . . . . 7 Word ..^ reverse
7473adantll 713 . . . . . 6 Word Word ..^ reverse
7552, 72, 743eqtr4d 2480 . . . . 5 Word Word ..^ concat concat reverse
761adantr 465 . . . . . 6 Word Word ..^ concat Word
77 uzid 10867 . . . . . . . . . . 11
7838, 77syl 16 . . . . . . . . . 10 Word Word
799adantr 465 . . . . . . . . . 10 Word Word
80 uzaddcl 10903 . . . . . . . . . 10
8178, 79, 80syl2anc 661 . . . . . . . . 9 Word Word
8215, 81eqeltrd 2512 . . . . . . . 8 Word Word concat
83 fzoss2 11569 . . . . . . . 8 concat ..^ ..^ concat
8482, 83syl 16 . . . . . . 7 Word Word ..^ ..^ concat
8584sselda 3351 . . . . . 6 Word Word ..^ ..^ concat
86 revfv 12395 . . . . . 6 concat Word ..^ concat reverse concat concat concat
8776, 85, 86syl2anc 661 . . . . 5 Word Word ..^ reverse concat concat concat
8820ad2antlr 726 . . . . . 6 Word Word ..^ reverse Word
8921ad2antrr 725 . . . . . 6 Word Word ..^ reverse Word
9029adantl 466 . . . . . . . . 9 Word Word reverse
9190oveq2d 6102 . . . . . . . 8 Word Word ..^reverse ..^
9291eleq2d 2505 . . . . . . 7 Word Word ..^reverse ..^
9392biimpar 485 . . . . . 6 Word Word ..^ ..^reverse
94 ccatval1 12268 . . . . . 6 reverse Word reverse Word ..^reverse reverse concat reverse reverse
9588, 89, 93, 94syl3anc 1218 . . . . 5 Word Word ..^ reverse concat reverse reverse
9675, 87, 953eqtr4d 2480 . . . 4 Word Word ..^ reverse concat reverse concat reverse
978oveq1d 6101 . . . . . . . . . . . 12 Word Word concat
9855, 54, 57addsubd 9732 . . . . . . . . . . . 12 Word Word
9997, 98eqtrd 2470 . . . . . . . . . . 11 Word Word concat
10099oveq1d 6101 . . . . . . . . . 10 Word Word concat
101100adantr 465 . . . . . . . . 9 Word Word ..^ concat
1029nn0zd 10737 . . . . . . . . . . . . 13 Word
103 peano2zm 10680 . . . . . . . . . . . . 13
104102, 103syl 16 . . . . . . . . . . . 12 Word
105104zcnd 10740 . . . . . . . . . . 11 Word
106105ad2antrr 725 . . . . . . . . . 10 Word Word ..^
107 elfzoelz 11545 . . . . . . . . . . . 12 ..^
108107zcnd 10740 . . . . . . . . . . 11 ..^
109108adantl 466 . . . . . . . . . 10 Word Word ..^
11012ad2antlr 726 . . . . . . . . . 10 Word Word ..^
111106, 109, 110subsub3d 9741 . . . . . . . . 9 Word Word ..^
112101, 111eqtr4d 2473 . . . . . . . 8 Word Word ..^ concat
11390oveq2d 6102 . . . . . . . . . 10 Word Word reverse
114113oveq2d 6102 . . . . . . . . 9 Word Word reverse
115114adantr 465 . . . . . . . 8 Word Word ..^ reverse
116112, 115eqtr4d 2473 . . . . . . 7 Word Word ..^ concat reverse
117116fveq2d 5690 . . . . . 6 Word Word ..^ concat reverse
118 simpll 753 . . . . . . 7 Word Word ..^ Word
119 simplr 754 . . . . . . 7 Word Word ..^ Word
120 zaddcl 10677 . . . . . . . . . . . 12
12137, 102, 120syl2anr 478 . . . . . . . . . . 11 Word Word
122 peano2zm 10680 . . . . . . . . . . 11
123121, 122syl 16 . . . . . . . . . 10 Word Word
124123adantr 465 . . . . . . . . 9 Word Word ..^
125 fzoval 11546 . . . . . . . . . . . 12 ..^
126121, 125syl 16 . . . . . . . . . . 11 Word Word ..^
127126eleq2d 2505 . . . . . . . . . 10 Word Word ..^
128127biimpa 484 . . . . . . . . 9 Word Word ..^
129 fzrev2i 11513 . . . . . . . . 9
130124, 128, 129syl2anc 661 . . . . . . . 8 Word Word ..^
13153oveq1d 6101 . . . . . . . . 9 Word Word concat
132131adantr 465 . . . . . . . 8 Word Word ..^ concat
133102adantr 465 . . . . . . . . . . 11 Word Word
134 fzoval 11546 . . . . . . . . . . 11 ..^
135133, 134syl 16 . . . . . . . . . 10 Word Word ..^
136123zcnd 10740 . . . . . . . . . . . 12 Word Word
137136subidd 9699 . . . . . . . . . . 11 Word Word
138 addcl 9356 . . . . . . . . . . . . . 14
13912, 10, 138syl2anr 478 . . . . . . . . . . . . 13 Word Word
140139, 57, 54sub32d 9743 . . . . . . . . . . . 12 Word Word
141 pncan2 9609 . . . . . . . . . . . . . 14
14212, 10, 141syl2anr 478 . . . . . . . . . . . . 13 Word Word
143142oveq1d 6101 . . . . . . . . . . . 12 Word Word
144140, 143eqtrd 2470 . . . . . . . . . . 11 Word Word
145137, 144oveq12d 6104 . . . . . . . . . 10 Word Word
146135, 145eqtr4d 2473 . . . . . . . . 9 Word Word ..^
147146adantr 465 . . . . . . . 8 Word Word ..^ ..^
148130, 132, 1473eltr4d 2519 . . . . . . 7 Word Word ..^ concat ..^
149 ccatval1 12268 . . . . . . 7 Word Word concat ..^ concat concat concat
150118, 119, 148, 149syl3anc 1218 . . . . . 6 Word Word ..^ concat concat concat
15129ad2antlr 726 . . . . . . . . 9 Word Word ..^ reverse
152151oveq2d 6102 . . . . . . . 8 Word Word ..^ reverse
153 id 22 . . . . . . . . 9 ..^ ..^
154 fzosubel3 11593 . . . . . . . . 9 ..^ ..^
155153, 133, 154syl2anr 478 . . . . . . . 8 Word Word ..^ ..^
156152, 155eqeltrd 2512 . . . . . . 7 Word Word ..^ reverse ..^
157 revfv 12395 . . . . . . 7 Word reverse ..^ reverse reverse reverse
158118, 156, 157syl2anc 661 . . . . . 6 Word Word ..^ reverse reverse reverse
159117, 150, 1583eqtr4d 2480 . . . . 5 Word Word ..^ concat concat reverse reverse
1601adantr 465 . . . . . 6 Word Word ..^ concat Word
16111adantl 466 . . . . . . . . 9 Word Word
162 fzoss1 11568 . . . . . . . . . 10 ..^ ..^
163 nn0uz 10887 . . . . . . . . . 10
164162, 163eleq2s 2530 . . . . . . . . 9 ..^ ..^
165161, 164syl 16 . . . . . . . 8 Word Word ..^ ..^
16615oveq2d 6102 . . . . . . . 8 Word Word ..^ concat ..^
167165, 166sseqtr4d 3388 . . . . . . 7 Word Word ..^ ..^ concat
168167sselda 3351 . . . . . 6 Word Word ..^ ..^ concat
169160, 168, 86syl2anc 661 . . . . 5 Word Word ..^ reverse concat concat concat
17020ad2antlr 726 . . . . . 6 Word Word ..^ reverse Word
17121ad2antrr 725 . . . . . 6 Word Word ..^ reverse Word
17290, 31oveq12d 6104 . . . . . . . 8 Word Word reverse..^reverse reverse ..^
173172eleq2d 2505 . . . . . . 7 Word Word reverse..^reverse reverse ..^
174173biimpar 485 . . . . . 6 Word Word ..^ reverse..^reverse reverse
175 ccatval2 12269 . . . . . 6 reverse Word reverse Word reverse..^reverse reverse reverse concat reverse reverse reverse
176170, 171, 174, 175syl3anc 1218 . . . . 5 Word Word ..^ reverse concat reverse reverse reverse
177159, 169, 1763eqtr4d 2480 . . . 4 Word Word ..^ reverse concat reverse concat reverse
17896, 177jaodan 783 . . 3 Word Word ..^ ..^ reverse concat reverse concat reverse
17940, 178syldan 470 . 2 Word Word ..^ reverse concat reverse concat reverse
18019, 35, 179eqfnfvd 5795 1 Word Word reverse concat reverse concat reverse
 Colors of variables: wff setvar class Syntax hints:   wi 4   wo 368   wa 369   wceq 1369   wcel 1756   wss 3323   wfn 5408  wf 5409  cfv 5413  (class class class)co 6086  cc 9272  cc0 9274  c1 9275   caddc 9277   cmin 9587  cn0 10571  cz 10638  cuz 10853  cfz 11429  ..^cfzo 11540  chash 12095  Word cword 12213   concat cconcat 12215  reversecreverse 12219 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-1st 6572  df-2nd 6573  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-card 8101  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-n0 10572  df-z 10639  df-uz 10854  df-fz 11430  df-fzo 11541  df-hash 12096  df-word 12221  df-concat 12223  df-reverse 12227 This theorem is referenced by:  gsumwrev  15872  efginvrel2  16215
 Copyright terms: Public domain W3C validator