revccat - Metamath Proof Explorer

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

Theorem revccat 11753

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.

Step	Hyp	Ref	Expression
1		ccatcl 11698	. . . . 5 Word $/\$ Word concat Word
2		revcl 11748	. . . . 5 concat Word reverse concat Word
3	1, 2	syl 16	. . . 4 Word $/\$ Word reverse concat Word
4		wrdf 11688	. . . 4 reverse concat Word reverse concat ..^reverse concat
5		ffn 5550	. . . 4 reverse concat ..^reverse concat reverse concat ..^reverse concat
6	3, 4, 5	3syl 19	. . 3 Word $/\$ Word reverse concat ..^reverse concat
7		revlen 11749	. . . . . . 7 concat Word reverse concat concat
8	1, 7	syl 16	. . . . . 6 Word $/\$ Word reverse concat concat
9		ccatlen 11699	. . . . . . 7 Word $/\$ Word concat
10		lencl 11690	. . . . . . . . 9 Word
11	10	nn0cnd 10232	. . . . . . . 8 Word
12		lencl 11690	. . . . . . . . 9 Word
13	12	nn0cnd 10232	. . . . . . . 8 Word
14		addcom 9208	. . . . . . . 8 $/\$
15	11, 13, 14	syl2an 464	. . . . . . 7 Word $/\$ Word
16	9, 15	eqtrd 2436	. . . . . 6 Word $/\$ Word concat
17	8, 16	eqtrd 2436	. . . . 5 Word $/\$ Word reverse concat
18	17	oveq2d 6056	. . . 4 Word $/\$ Word ..^reverse concat ..^
19	18	fneq2d 5496	. . 3 Word $/\$ Word reverse concat ..^reverse concat reverse concat ..^
20	6, 19	mpbid 202	. 2 Word $/\$ Word reverse concat ..^
21		revcl 11748	. . . . 5 Word reverse Word
22		revcl 11748	. . . . 5 Word reverse Word
23		ccatcl 11698	. . . . 5 reverse Word $/\$ reverse Word reverse concat reverse Word
24	21, 22, 23	syl2anr 465	. . . 4 Word $/\$ Word reverse concat reverse Word
25		wrdf 11688	. . . 4 reverse concat reverse Word reverse concat reverse..^reverse concat reverse
26		ffn 5550	. . . 4 reverse concat reverse..^reverse concat reverse reverse concat reverse ..^reverse concat reverse
27	24, 25, 26	3syl 19	. . 3 Word $/\$ Word reverse concat reverse ..^reverse concat reverse
28		ccatlen 11699	. . . . . . 7 reverse Word $/\$ reverse Word reverse concat reverse reverse reverse
29	21, 22, 28	syl2anr 465	. . . . . 6 Word $/\$ Word reverse concat reverse reverse reverse
30		revlen 11749	. . . . . . 7 Word reverse
31		revlen 11749	. . . . . . 7 Word reverse
32	30, 31	oveqan12rd 6060	. . . . . 6 Word $/\$ Word reverse reverse
33	29, 32	eqtrd 2436	. . . . 5 Word $/\$ Word reverse concat reverse
34	33	oveq2d 6056	. . . 4 Word $/\$ Word ..^reverse concat reverse ..^
35	34	fneq2d 5496	. . 3 Word $/\$ Word reverse concat reverse ..^reverse concat reverse reverse concat reverse ..^
36	27, 35	mpbid 202	. 2 Word $/\$ Word reverse concat reverse ..^
37		id 20	. . . 4 ..^ ..^
38	12	nn0zd 10329	. . . . 5 Word
39	38	adantl 453	. . . 4 Word $/\$ Word
40		fzospliti 11120	. . . 4 ..^ $/\$ ..^ $\/$ ..^
41	37, 39, 40	syl2anr 465	. . 3 Word $/\$ Word $/\$ ..^ ..^ $\/$ ..^
42		simpll 731	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
43		simplr 732	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
44		fzoval 11096	. . . . . . . . . . . 12 ..^
45	39, 44	syl 16	. . . . . . . . . . 11 Word $/\$ Word ..^
46	45	eleq2d 2471	. . . . . . . . . 10 Word $/\$ Word ..^
47	46	biimpa 471	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
48		fznn0sub2 11042	. . . . . . . . 9
49	47, 48	syl 16	. . . . . . . 8 Word $/\$ Word $/\$ ..^
50	45	adantr 452	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
51	49, 50	eleqtrrd 2481	. . . . . . 7 Word $/\$ Word $/\$ ..^ ..^
52		ccatval3 11702	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat
53	42, 43, 51, 52	syl3anc 1184	. . . . . 6 Word $/\$ Word $/\$ ..^ concat
54	16	oveq1d 6055	. . . . . . . . . . 11 Word $/\$ Word concat
55	13	adantl 453	. . . . . . . . . . . 12 Word $/\$ Word
56	11	adantr 452	. . . . . . . . . . . 12 Word $/\$ Word
57		ax-1cn 9004	. . . . . . . . . . . . 13
58	57	a1i 11	. . . . . . . . . . . 12 Word $/\$ Word
59	55, 56, 58	addsubd 9388	. . . . . . . . . . 11 Word $/\$ Word
60	54, 59	eqtrd 2436	. . . . . . . . . 10 Word $/\$ Word concat
61	60	oveq1d 6055	. . . . . . . . 9 Word $/\$ Word concat
62	61	adantr 452	. . . . . . . 8 Word $/\$ Word $/\$ ..^ concat
63		peano2zm 10276	. . . . . . . . . . . 12
64	38, 63	syl 16	. . . . . . . . . . 11 Word
65	64	zcnd 10332	. . . . . . . . . 10 Word
66	65	ad2antlr 708	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
67	11	ad2antrr 707	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
68		elfzoelz 11095	. . . . . . . . . . 11 ..^
69	68	zcnd 10332	. . . . . . . . . 10 ..^
70	69	adantl 453	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
71	66, 67, 70	addsubd 9388	. . . . . . . 8 Word $/\$ Word $/\$ ..^
72	62, 71	eqtrd 2436	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat
73	72	fveq2d 5691	. . . . . 6 Word $/\$ Word $/\$ ..^ concat concat concat
74		revfv 11750	. . . . . . 7 Word $/\$ ..^ reverse
75	74	adantll 695	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse
76	53, 73, 75	3eqtr4d 2446	. . . . 5 Word $/\$ Word $/\$ ..^ concat concat reverse
77	1	adantr 452	. . . . . 6 Word $/\$ Word $/\$ ..^ concat Word
78		uzid 10456	. . . . . . . . . . 11
79	39, 78	syl 16	. . . . . . . . . 10 Word $/\$ Word
80	10	adantr 452	. . . . . . . . . 10 Word $/\$ Word
81		uzaddcl 10489	. . . . . . . . . 10 $/\$
82	79, 80, 81	syl2anc 643	. . . . . . . . 9 Word $/\$ Word
83	16, 82	eqeltrd 2478	. . . . . . . 8 Word $/\$ Word concat
84		fzoss2 11118	. . . . . . . 8 concat ..^ ..^ concat
85	83, 84	syl 16	. . . . . . 7 Word $/\$ Word ..^ ..^ concat
86	85	sselda 3308	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^ concat
87		revfv 11750	. . . . . 6 concat Word $/\$ ..^ concat reverse concat concat concat
88	77, 86, 87	syl2anc 643	. . . . 5 Word $/\$ Word $/\$ ..^ reverse concat concat concat
89	21	ad2antlr 708	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
90	22	ad2antrr 707	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
91	30	adantl 453	. . . . . . . . 9 Word $/\$ Word reverse
92	91	oveq2d 6056	. . . . . . . 8 Word $/\$ Word ..^reverse ..^
93	92	eleq2d 2471	. . . . . . 7 Word $/\$ Word ..^reverse ..^
94	93	biimpar 472	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^reverse
95		ccatval1 11700	. . . . . 6 reverse Word $/\$ reverse Word $/\$ ..^reverse reverse concat reverse reverse
96	89, 90, 94, 95	syl3anc 1184	. . . . 5 Word $/\$ Word $/\$ ..^ reverse concat reverse reverse
97	76, 88, 96	3eqtr4d 2446	. . . 4 Word $/\$ Word $/\$ ..^ reverse concat reverse concat reverse
98	9	oveq1d 6055	. . . . . . . . . . . 12 Word $/\$ Word concat
99	56, 55, 58	addsubd 9388	. . . . . . . . . . . 12 Word $/\$ Word
100	98, 99	eqtrd 2436	. . . . . . . . . . 11 Word $/\$ Word concat
101	100	oveq1d 6055	. . . . . . . . . 10 Word $/\$ Word concat
102	101	adantr 452	. . . . . . . . 9 Word $/\$ Word $/\$ ..^ concat
103	10	nn0zd 10329	. . . . . . . . . . . . 13 Word
104		peano2zm 10276	. . . . . . . . . . . . 13
105	103, 104	syl 16	. . . . . . . . . . . 12 Word
106	105	zcnd 10332	. . . . . . . . . . 11 Word
107	106	ad2antrr 707	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
108		elfzoelz 11095	. . . . . . . . . . . 12 ..^
109	108	zcnd 10332	. . . . . . . . . . 11 ..^
110	109	adantl 453	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
111	13	ad2antlr 708	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
112	107, 110, 111	subsub3d 9397	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
113	102, 112	eqtr4d 2439	. . . . . . . 8 Word $/\$ Word $/\$ ..^ concat
114	91	oveq2d 6056	. . . . . . . . . 10 Word $/\$ Word reverse
115	114	oveq2d 6056	. . . . . . . . 9 Word $/\$ Word reverse
116	115	adantr 452	. . . . . . . 8 Word $/\$ Word $/\$ ..^ reverse
117	113, 116	eqtr4d 2439	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat reverse
118	117	fveq2d 5691	. . . . . 6 Word $/\$ Word $/\$ ..^ concat reverse
119		simpll 731	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
120		simplr 732	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
121		zaddcl 10273	. . . . . . . . . . . 12 $/\$
122	38, 103, 121	syl2anr 465	. . . . . . . . . . 11 Word $/\$ Word
123		peano2zm 10276	. . . . . . . . . . 11
124	122, 123	syl 16	. . . . . . . . . 10 Word $/\$ Word
125	124	adantr 452	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
126		fzoval 11096	. . . . . . . . . . . 12 ..^
127	122, 126	syl 16	. . . . . . . . . . 11 Word $/\$ Word ..^
128	127	eleq2d 2471	. . . . . . . . . 10 Word $/\$ Word ..^
129	128	biimpa 471	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
130		fzrev2i 11066	. . . . . . . . 9 $/\$
131	125, 129, 130	syl2anc 643	. . . . . . . 8 Word $/\$ Word $/\$ ..^
132	54	oveq1d 6055	. . . . . . . . 9 Word $/\$ Word concat
133	132	adantr 452	. . . . . . . 8 Word $/\$ Word $/\$ ..^ concat
134	103	adantr 452	. . . . . . . . . . 11 Word $/\$ Word
135		fzoval 11096	. . . . . . . . . . 11 ..^
136	134, 135	syl 16	. . . . . . . . . 10 Word $/\$ Word ..^
137	124	zcnd 10332	. . . . . . . . . . . 12 Word $/\$ Word
138	137	subidd 9355	. . . . . . . . . . 11 Word $/\$ Word
139		addcl 9028	. . . . . . . . . . . . . 14 $/\$
140	13, 11, 139	syl2anr 465	. . . . . . . . . . . . 13 Word $/\$ Word
141	140, 58, 55	sub32d 9399	. . . . . . . . . . . 12 Word $/\$ Word
142		pncan2 9268	. . . . . . . . . . . . . 14 $/\$
143	13, 11, 142	syl2anr 465	. . . . . . . . . . . . 13 Word $/\$ Word
144	143	oveq1d 6055	. . . . . . . . . . . 12 Word $/\$ Word
145	141, 144	eqtrd 2436	. . . . . . . . . . 11 Word $/\$ Word
146	138, 145	oveq12d 6058	. . . . . . . . . 10 Word $/\$ Word
147	136, 146	eqtr4d 2439	. . . . . . . . 9 Word $/\$ Word ..^
148	147	adantr 452	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
149	131, 133, 148	3eltr4d 2485	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat ..^
150		ccatval1 11700	. . . . . . 7 Word $/\$ Word $/\$ concat ..^ concat concat concat
151	119, 120, 149, 150	syl3anc 1184	. . . . . 6 Word $/\$ Word $/\$ ..^ concat concat concat
152	30	ad2antlr 708	. . . . . . . . 9 Word $/\$ Word $/\$ ..^ reverse
153	152	oveq2d 6056	. . . . . . . 8 Word $/\$ Word $/\$ ..^ reverse
154		id 20	. . . . . . . . 9 ..^ ..^
155		fzosubel3 11134	. . . . . . . . 9 ..^ $/\$ ..^
156	154, 134, 155	syl2anr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
157	153, 156	eqeltrd 2478	. . . . . . 7 Word $/\$ Word $/\$ ..^ reverse ..^
158		revfv 11750	. . . . . . 7 Word $/\$ reverse ..^ reverse reverse reverse
159	119, 157, 158	syl2anc 643	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse reverse reverse
160	118, 151, 159	3eqtr4d 2446	. . . . 5 Word $/\$ Word $/\$ ..^ concat concat reverse reverse
161	1	adantr 452	. . . . . 6 Word $/\$ Word $/\$ ..^ concat Word
162	12	adantl 453	. . . . . . . . 9 Word $/\$ Word
163		fzoss1 11117	. . . . . . . . . 10 ..^ ..^
164		nn0uz 10476	. . . . . . . . . 10
165	163, 164	eleq2s 2496	. . . . . . . . 9 ..^ ..^
166	162, 165	syl 16	. . . . . . . 8 Word $/\$ Word ..^ ..^
167	16	oveq2d 6056	. . . . . . . 8 Word $/\$ Word ..^ concat ..^
168	166, 167	sseqtr4d 3345	. . . . . . 7 Word $/\$ Word ..^ ..^ concat
169	168	sselda 3308	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^ concat
170	161, 169, 87	syl2anc 643	. . . . 5 Word $/\$ Word $/\$ ..^ reverse concat concat concat
171	21	ad2antlr 708	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
172	22	ad2antrr 707	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
173	91, 32	oveq12d 6058	. . . . . . . 8 Word $/\$ Word reverse..^reverse reverse ..^
174	173	eleq2d 2471	. . . . . . 7 Word $/\$ Word reverse..^reverse reverse ..^
175	174	biimpar 472	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse..^reverse reverse
176		ccatval2 11701	. . . . . 6 reverse Word $/\$ reverse Word $/\$ reverse..^reverse reverse reverse concat reverse reverse reverse
177	171, 172, 175, 176	syl3anc 1184	. . . . 5 Word $/\$ Word $/\$ ..^ reverse concat reverse reverse reverse
178	160, 170, 177	3eqtr4d 2446	. . . 4 Word $/\$ Word $/\$ ..^ reverse concat reverse concat reverse
179	97, 178	jaodan 761	. . 3 Word $/\$ Word $/\$ ..^ $\/$ ..^ reverse concat reverse concat reverse
180	41, 179	syldan 457	. 2 Word $/\$ Word $/\$ ..^ reverse concat reverse concat reverse
181	20, 36, 180	eqfnfvd 5789	1 Word $/\$ Word reverse concat reverse concat reverse

Colors of variables: wff set class

Syntax hints:

wi 4 $\/$ wo 358 $/\$ wa 359

wceq 1649

wcel 1721

wss 3280

wfn 5408

wf 5409

cfv 5413 (class class class)co 6040

cc 8944

cc0 8946

c1 8947

caddc 8949

cmin 9247

cn0 10177

cz 10238

cuz 10444

cfz 10999 ..^cfzo 11090

chash 11573 Word cword 11672 concat cconcat 11673 reversecreverse 11677

This theorem is referenced by: gsumwrev 15117 efginvrel2 15314

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 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-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-card 7782 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-nn 9957 df-n0 10178 df-z 10239 df-uz 10445 df-fz 11000 df-fzo 11091 df-hash 11574 df-word 11678 df-concat 11679 df-reverse 11683

W3C validator