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

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

Proof of Theorem revccat
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ccatcl 12601 . . . 4 Word Word ++ Word
2 revcl 12746 . . . 4 ++ Word reverse ++ Word
3 wrdf 12557 . . . 4 reverse ++ Word reverse ++ ..^reverse ++
4 ffn 5737 . . . 4 reverse ++ ..^reverse ++ reverse ++ ..^reverse ++
51, 2, 3, 44syl 21 . . 3 Word Word reverse ++ ..^reverse ++
6 revlen 12747 . . . . . . 7 ++ Word reverse ++ ++
71, 6syl 16 . . . . . 6 Word Word reverse ++ ++
8 ccatlen 12602 . . . . . . 7 Word Word ++
9 lencl 12568 . . . . . . . . 9 Word
109nn0cnd 10875 . . . . . . . 8 Word
11 lencl 12568 . . . . . . . . 9 Word
1211nn0cnd 10875 . . . . . . . 8 Word
13 addcom 9783 . . . . . . . 8
1410, 12, 13syl2an 477 . . . . . . 7 Word Word
158, 14eqtrd 2498 . . . . . 6 Word Word ++
167, 15eqtrd 2498 . . . . 5 Word Word reverse ++
1716oveq2d 6312 . . . 4 Word Word ..^reverse ++ ..^
1817fneq2d 5678 . . 3 Word Word reverse ++ ..^reverse ++ reverse ++ ..^
195, 18mpbid 210 . 2 Word Word reverse ++ ..^
20 revcl 12746 . . . . 5 Word reverse Word
21 revcl 12746 . . . . 5 Word reverse Word
22 ccatcl 12601 . . . . 5 reverse Word reverse Word reverse ++ reverse Word
2320, 21, 22syl2anr 478 . . . 4 Word Word reverse ++ reverse Word
24 wrdf 12557 . . . 4 reverse ++ reverse Word reverse ++ reverse..^reverse ++ reverse
25 ffn 5737 . . . 4 reverse ++ reverse..^reverse ++ reverse reverse ++ reverse ..^reverse ++ reverse
2623, 24, 253syl 20 . . 3 Word Word reverse ++ reverse ..^reverse ++ reverse
27 ccatlen 12602 . . . . . . 7 reverse Word reverse Word reverse ++ reverse reverse reverse
2820, 21, 27syl2anr 478 . . . . . 6 Word Word reverse ++ reverse reverse reverse
29 revlen 12747 . . . . . . 7 Word reverse
30 revlen 12747 . . . . . . 7 Word reverse
3129, 30oveqan12rd 6316 . . . . . 6 Word Word reverse reverse
3228, 31eqtrd 2498 . . . . 5 Word Word reverse ++ reverse
3332oveq2d 6312 . . . 4 Word Word ..^reverse ++ reverse ..^
3433fneq2d 5678 . . 3 Word Word reverse ++ reverse ..^reverse ++ reverse reverse ++ reverse ..^
3526, 34mpbid 210 . 2 Word Word reverse ++ reverse ..^
36 id 22 . . . 4 ..^ ..^
3711nn0zd 10988 . . . . 5 Word
3837adantl 466 . . . 4 Word Word
39 fzospliti 11855 . . . 4 ..^ ..^ ..^
4036, 38, 39syl2anr 478 . . 3 Word Word ..^ ..^ ..^
41 simpll 753 . . . . . . 7 Word Word ..^ Word
42 simplr 755 . . . . . . 7 Word Word ..^ Word
43 fzoval 11826 . . . . . . . . . . . 12 ..^
4438, 43syl 16 . . . . . . . . . . 11 Word Word ..^
4544eleq2d 2527 . . . . . . . . . 10 Word Word ..^
4645biimpa 484 . . . . . . . . 9 Word Word ..^
47 fznn0sub2 11806 . . . . . . . . 9
4846, 47syl 16 . . . . . . . 8 Word Word ..^
4944adantr 465 . . . . . . . 8 Word Word ..^ ..^
5048, 49eleqtrrd 2548 . . . . . . 7 Word Word ..^ ..^
51 ccatval3 12605 . . . . . . 7 Word Word ..^ ++
5241, 42, 50, 51syl3anc 1228 . . . . . 6 Word Word ..^ ++
5315oveq1d 6311 . . . . . . . . . . 11 Word Word ++
5412adantl 466 . . . . . . . . . . . 12 Word Word
5510adantr 465 . . . . . . . . . . . 12 Word Word
56 1cnd 9629 . . . . . . . . . . . 12 Word Word
5754, 55, 56addsubd 9971 . . . . . . . . . . 11 Word Word
5853, 57eqtrd 2498 . . . . . . . . . 10 Word Word ++
5958oveq1d 6311 . . . . . . . . 9 Word Word ++
6059adantr 465 . . . . . . . 8 Word Word ..^ ++
61 peano2zm 10928 . . . . . . . . . . . 12
6237, 61syl 16 . . . . . . . . . . 11 Word
6362zcnd 10991 . . . . . . . . . 10 Word
6463ad2antlr 726 . . . . . . . . 9 Word Word ..^
6510ad2antrr 725 . . . . . . . . 9 Word Word ..^
66 elfzoelz 11825 . . . . . . . . . . 11 ..^
6766zcnd 10991 . . . . . . . . . 10 ..^
6867adantl 466 . . . . . . . . 9 Word Word ..^
6964, 65, 68addsubd 9971 . . . . . . . 8 Word Word ..^
7060, 69eqtrd 2498 . . . . . . 7 Word Word ..^ ++
7170fveq2d 5876 . . . . . 6 Word Word ..^ ++ ++ ++
72 revfv 12748 . . . . . . 7 Word ..^ reverse
7372adantll 713 . . . . . 6 Word Word ..^ reverse
7452, 71, 733eqtr4d 2508 . . . . 5 Word Word ..^ ++ ++ reverse
751adantr 465 . . . . . 6 Word Word ..^ ++ Word
76 uzid 11120 . . . . . . . . . . 11
7738, 76syl 16 . . . . . . . . . 10 Word Word
789adantr 465 . . . . . . . . . 10 Word Word
79 uzaddcl 11162 . . . . . . . . . 10
8077, 78, 79syl2anc 661 . . . . . . . . 9 Word Word
8115, 80eqeltrd 2545 . . . . . . . 8 Word Word ++
82 fzoss2 11851 . . . . . . . 8 ++ ..^ ..^ ++
8381, 82syl 16 . . . . . . 7 Word Word ..^ ..^ ++
8483sselda 3499 . . . . . 6 Word Word ..^ ..^ ++
85 revfv 12748 . . . . . 6 ++ Word ..^ ++ reverse ++ ++ ++
8675, 84, 85syl2anc 661 . . . . 5 Word Word ..^ reverse ++ ++ ++
8720ad2antlr 726 . . . . . 6 Word Word ..^ reverse Word
8821ad2antrr 725 . . . . . 6 Word Word ..^ reverse Word
8929adantl 466 . . . . . . . . 9 Word Word reverse
9089oveq2d 6312 . . . . . . . 8 Word Word ..^reverse ..^
9190eleq2d 2527 . . . . . . 7 Word Word ..^reverse ..^
9291biimpar 485 . . . . . 6 Word Word ..^ ..^reverse
93 ccatval1 12603 . . . . . 6 reverse Word reverse Word ..^reverse reverse ++ reverse reverse
9487, 88, 92, 93syl3anc 1228 . . . . 5 Word Word ..^ reverse ++ reverse reverse
9574, 86, 943eqtr4d 2508 . . . 4 Word Word ..^ reverse ++ reverse ++ reverse
968oveq1d 6311 . . . . . . . . . . . 12 Word Word ++
9755, 54, 56addsubd 9971 . . . . . . . . . . . 12 Word Word
9896, 97eqtrd 2498 . . . . . . . . . . 11 Word Word ++
9998oveq1d 6311 . . . . . . . . . 10 Word Word ++
10099adantr 465 . . . . . . . . 9 Word Word ..^ ++
1019nn0zd 10988 . . . . . . . . . . . . 13 Word
102 peano2zm 10928 . . . . . . . . . . . . 13
103101, 102syl 16 . . . . . . . . . . . 12 Word
104103zcnd 10991 . . . . . . . . . . 11 Word
105104ad2antrr 725 . . . . . . . . . 10 Word Word ..^
106 elfzoelz 11825 . . . . . . . . . . . 12 ..^
107106zcnd 10991 . . . . . . . . . . 11 ..^
108107adantl 466 . . . . . . . . . 10 Word Word ..^
10912ad2antlr 726 . . . . . . . . . 10 Word Word ..^
110105, 108, 109subsub3d 9980 . . . . . . . . 9 Word Word ..^
111100, 110eqtr4d 2501 . . . . . . . 8 Word Word ..^ ++
11289oveq2d 6312 . . . . . . . . . 10 Word Word reverse
113112oveq2d 6312 . . . . . . . . 9 Word Word reverse
114113adantr 465 . . . . . . . 8 Word Word ..^ reverse
115111, 114eqtr4d 2501 . . . . . . 7 Word Word ..^ ++ reverse
116115fveq2d 5876 . . . . . 6 Word Word ..^ ++ reverse
117 simpll 753 . . . . . . 7 Word Word ..^ Word
118 simplr 755 . . . . . . 7 Word Word ..^ Word
119 zaddcl 10925 . . . . . . . . . . . 12
12037, 101, 119syl2anr 478 . . . . . . . . . . 11 Word Word
121 peano2zm 10928 . . . . . . . . . . 11
122120, 121syl 16 . . . . . . . . . 10 Word Word
123122adantr 465 . . . . . . . . 9 Word Word ..^
124 fzoval 11826 . . . . . . . . . . . 12 ..^
125120, 124syl 16 . . . . . . . . . . 11 Word Word ..^
126125eleq2d 2527 . . . . . . . . . 10 Word Word ..^
127126biimpa 484 . . . . . . . . 9 Word Word ..^
128 fzrev2i 11769 . . . . . . . . 9
129123, 127, 128syl2anc 661 . . . . . . . 8 Word Word ..^
13053oveq1d 6311 . . . . . . . . 9 Word Word ++
131130adantr 465 . . . . . . . 8 Word Word ..^ ++
132101adantr 465 . . . . . . . . . . 11 Word Word
133 fzoval 11826 . . . . . . . . . . 11 ..^
134132, 133syl 16 . . . . . . . . . 10 Word Word ..^
135122zcnd 10991 . . . . . . . . . . . 12 Word Word
136135subidd 9938 . . . . . . . . . . 11 Word Word
137 addcl 9591 . . . . . . . . . . . . . 14
13812, 10, 137syl2anr 478 . . . . . . . . . . . . 13 Word Word
139138, 56, 54sub32d 9982 . . . . . . . . . . . 12 Word Word
140 pncan2 9846 . . . . . . . . . . . . . 14
14112, 10, 140syl2anr 478 . . . . . . . . . . . . 13 Word Word
142141oveq1d 6311 . . . . . . . . . . . 12 Word Word
143139, 142eqtrd 2498 . . . . . . . . . . 11 Word Word
144136, 143oveq12d 6314 . . . . . . . . . 10 Word Word
145134, 144eqtr4d 2501 . . . . . . . . 9 Word Word ..^
146145adantr 465 . . . . . . . 8 Word Word ..^ ..^
147129, 131, 1463eltr4d 2560 . . . . . . 7 Word Word ..^ ++ ..^
148 ccatval1 12603 . . . . . . 7 Word Word ++ ..^ ++ ++ ++
149117, 118, 147, 148syl3anc 1228 . . . . . 6 Word Word ..^ ++ ++ ++
15029ad2antlr 726 . . . . . . . . 9 Word Word ..^ reverse
151150oveq2d 6312 . . . . . . . 8 Word Word ..^ reverse
152 id 22 . . . . . . . . 9 ..^ ..^
153 fzosubel3 11879 . . . . . . . . 9 ..^ ..^
154152, 132, 153syl2anr 478 . . . . . . . 8 Word Word ..^ ..^
155151, 154eqeltrd 2545 . . . . . . 7 Word Word ..^ reverse ..^
156 revfv 12748 . . . . . . 7 Word reverse ..^ reverse reverse reverse
157117, 155, 156syl2anc 661 . . . . . 6 Word Word ..^ reverse reverse reverse
158116, 149, 1573eqtr4d 2508 . . . . 5 Word Word ..^ ++ ++ reverse reverse
1591adantr 465 . . . . . 6 Word Word ..^ ++ Word
16011adantl 466 . . . . . . . . 9 Word Word
161 fzoss1 11850 . . . . . . . . . 10 ..^ ..^
162 nn0uz 11140 . . . . . . . . . 10
163161, 162eleq2s 2565 . . . . . . . . 9 ..^ ..^
164160, 163syl 16 . . . . . . . 8 Word Word ..^ ..^
16515oveq2d 6312 . . . . . . . 8 Word Word ..^ ++ ..^
166164, 165sseqtr4d 3536 . . . . . . 7 Word Word ..^ ..^ ++
167166sselda 3499 . . . . . 6 Word Word ..^ ..^ ++
168159, 167, 85syl2anc 661 . . . . 5 Word Word ..^ reverse ++ ++ ++
16920ad2antlr 726 . . . . . 6 Word Word ..^ reverse Word
17021ad2antrr 725 . . . . . 6 Word Word ..^ reverse Word
17189, 31oveq12d 6314 . . . . . . . 8 Word Word reverse..^reverse reverse ..^
172171eleq2d 2527 . . . . . . 7 Word Word reverse..^reverse reverse ..^
173172biimpar 485 . . . . . 6 Word Word ..^ reverse..^reverse reverse
174 ccatval2 12604 . . . . . 6 reverse Word reverse Word reverse..^reverse reverse reverse ++ reverse reverse reverse
175169, 170, 173, 174syl3anc 1228 . . . . 5 Word Word ..^ reverse ++ reverse reverse reverse
176158, 168, 1753eqtr4d 2508 . . . 4 Word Word ..^ reverse ++ reverse ++ reverse
17795, 176jaodan 785 . . 3 Word Word ..^ ..^ reverse ++ reverse ++ reverse
17840, 177syldan 470 . 2 Word Word ..^ reverse ++ reverse ++ reverse
17919, 35, 178eqfnfvd 5985 1 Word Word reverse ++ reverse ++ reverse
 Colors of variables: wff setvar class Syntax hints:   wi 4   wo 368   wa 369   wceq 1395   wcel 1819   wss 3471   wfn 5589  wf 5590  cfv 5594  (class class class)co 6296  cc 9507  cc0 9509  c1 9510   caddc 9512   cmin 9824  cn0 10816  cz 10885  cuz 11106  cfz 11697  ..^cfzo 11820  chash 12407  Word cword 12537   ++ cconcat 12539  reversecreverse 12543 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-1st 6799  df-2nd 6800  df-recs 7060  df-rdg 7094  df-1o 7148  df-oadd 7152  df-er 7329  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-card 8337  df-cda 8565  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-nn 10557  df-2 10615  df-n0 10817  df-z 10886  df-uz 11107  df-fz 11698  df-fzo 11821  df-hash 12408  df-word 12545  df-concat 12547  df-reverse 12551 This theorem is referenced by:  gsumwrev  16527  efginvrel2  16871
 Copyright terms: Public domain W3C validator