revccat - Metamath Proof Explorer

	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.

Step	Hyp	Ref	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
5	1, 2, 3, 4	4syl 21	. . 3 Word $/\$ Word reverse concat ..^reverse concat
6		revlen 12394	. . . . . . 7 concat Word reverse concat concat
7	1, 6	syl 16	. . . . . 6 Word $/\$ Word reverse concat concat
8		ccatlen 12267	. . . . . . 7 Word $/\$ Word concat
9		lencl 12241	. . . . . . . . 9 Word
10	9	nn0cnd 10630	. . . . . . . 8 Word
11		lencl 12241	. . . . . . . . 9 Word
12	11	nn0cnd 10630	. . . . . . . 8 Word
13		addcom 9547	. . . . . . . 8 $/\$
14	10, 12, 13	syl2an 477	. . . . . . 7 Word $/\$ Word
15	8, 14	eqtrd 2470	. . . . . 6 Word $/\$ Word concat
16	7, 15	eqtrd 2470	. . . . 5 Word $/\$ Word reverse concat
17	16	oveq2d 6102	. . . 4 Word $/\$ Word ..^reverse concat ..^
18	17	fneq2d 5497	. . 3 Word $/\$ Word reverse concat ..^reverse concat reverse concat ..^
19	5, 18	mpbid 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
23	20, 21, 22	syl2anr 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
26	23, 24, 25	3syl 20	. . 3 Word $/\$ Word reverse concat reverse ..^reverse concat reverse
27		ccatlen 12267	. . . . . . 7 reverse Word $/\$ reverse Word reverse concat reverse reverse reverse
28	20, 21, 27	syl2anr 478	. . . . . 6 Word $/\$ Word reverse concat reverse reverse reverse
29		revlen 12394	. . . . . . 7 Word reverse
30		revlen 12394	. . . . . . 7 Word reverse
31	29, 30	oveqan12rd 6106	. . . . . 6 Word $/\$ Word reverse reverse
32	28, 31	eqtrd 2470	. . . . 5 Word $/\$ Word reverse concat reverse
33	32	oveq2d 6102	. . . 4 Word $/\$ Word ..^reverse concat reverse ..^
34	33	fneq2d 5497	. . 3 Word $/\$ Word reverse concat reverse ..^reverse concat reverse reverse concat reverse ..^
35	26, 34	mpbid 210	. 2 Word $/\$ Word reverse concat reverse ..^
36		id 22	. . . 4 ..^ ..^
37	11	nn0zd 10737	. . . . 5 Word
38	37	adantl 466	. . . 4 Word $/\$ Word
39		fzospliti 11573	. . . 4 ..^ $/\$ ..^ $\/$ ..^
40	36, 38, 39	syl2anr 478	. . 3 Word $/\$ Word $/\$ ..^ ..^ $\/$ ..^
41		simpll 753	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
42		simplr 754	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
43		fzoval 11546	. . . . . . . . . . . 12 ..^
44	38, 43	syl 16	. . . . . . . . . . 11 Word $/\$ Word ..^
45	44	eleq2d 2505	. . . . . . . . . 10 Word $/\$ Word ..^
46	45	biimpa 484	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
47		fznn0sub2 11480	. . . . . . . . 9
48	46, 47	syl 16	. . . . . . . 8 Word $/\$ Word $/\$ ..^
49	44	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
50	48, 49	eleqtrrd 2515	. . . . . . 7 Word $/\$ Word $/\$ ..^ ..^
51		ccatval3 12270	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat
52	41, 42, 50, 51	syl3anc 1218	. . . . . 6 Word $/\$ Word $/\$ ..^ concat
53	15	oveq1d 6101	. . . . . . . . . . 11 Word $/\$ Word concat
54	12	adantl 466	. . . . . . . . . . . 12 Word $/\$ Word
55	10	adantr 465	. . . . . . . . . . . 12 Word $/\$ Word
56		ax-1cn 9332	. . . . . . . . . . . . 13
57	56	a1i 11	. . . . . . . . . . . 12 Word $/\$ Word
58	54, 55, 57	addsubd 9732	. . . . . . . . . . 11 Word $/\$ Word
59	53, 58	eqtrd 2470	. . . . . . . . . 10 Word $/\$ Word concat
60	59	oveq1d 6101	. . . . . . . . 9 Word $/\$ Word concat
61	60	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ concat
62		peano2zm 10680	. . . . . . . . . . . 12
63	37, 62	syl 16	. . . . . . . . . . 11 Word
64	63	zcnd 10740	. . . . . . . . . 10 Word
65	64	ad2antlr 726	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
66	10	ad2antrr 725	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
67		elfzoelz 11545	. . . . . . . . . . 11 ..^
68	67	zcnd 10740	. . . . . . . . . 10 ..^
69	68	adantl 466	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
70	65, 66, 69	addsubd 9732	. . . . . . . 8 Word $/\$ Word $/\$ ..^
71	61, 70	eqtrd 2470	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat
72	71	fveq2d 5690	. . . . . 6 Word $/\$ Word $/\$ ..^ concat concat concat
73		revfv 12395	. . . . . . 7 Word $/\$ ..^ reverse
74	73	adantll 713	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse
75	52, 72, 74	3eqtr4d 2480	. . . . 5 Word $/\$ Word $/\$ ..^ concat concat reverse
76	1	adantr 465	. . . . . 6 Word $/\$ Word $/\$ ..^ concat Word
77		uzid 10867	. . . . . . . . . . 11
78	38, 77	syl 16	. . . . . . . . . 10 Word $/\$ Word
79	9	adantr 465	. . . . . . . . . 10 Word $/\$ Word
80		uzaddcl 10903	. . . . . . . . . 10 $/\$
81	78, 79, 80	syl2anc 661	. . . . . . . . 9 Word $/\$ Word
82	15, 81	eqeltrd 2512	. . . . . . . 8 Word $/\$ Word concat
83		fzoss2 11569	. . . . . . . 8 concat ..^ ..^ concat
84	82, 83	syl 16	. . . . . . 7 Word $/\$ Word ..^ ..^ concat
85	84	sselda 3351	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^ concat
86		revfv 12395	. . . . . 6 concat Word $/\$ ..^ concat reverse concat concat concat
87	76, 85, 86	syl2anc 661	. . . . 5 Word $/\$ Word $/\$ ..^ reverse concat concat concat
88	20	ad2antlr 726	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
89	21	ad2antrr 725	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
90	29	adantl 466	. . . . . . . . 9 Word $/\$ Word reverse
91	90	oveq2d 6102	. . . . . . . 8 Word $/\$ Word ..^reverse ..^
92	91	eleq2d 2505	. . . . . . 7 Word $/\$ Word ..^reverse ..^
93	92	biimpar 485	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^reverse
94		ccatval1 12268	. . . . . 6 reverse Word $/\$ reverse Word $/\$ ..^reverse reverse concat reverse reverse
95	88, 89, 93, 94	syl3anc 1218	. . . . 5 Word $/\$ Word $/\$ ..^ reverse concat reverse reverse
96	75, 87, 95	3eqtr4d 2480	. . . 4 Word $/\$ Word $/\$ ..^ reverse concat reverse concat reverse
97	8	oveq1d 6101	. . . . . . . . . . . 12 Word $/\$ Word concat
98	55, 54, 57	addsubd 9732	. . . . . . . . . . . 12 Word $/\$ Word
99	97, 98	eqtrd 2470	. . . . . . . . . . 11 Word $/\$ Word concat
100	99	oveq1d 6101	. . . . . . . . . 10 Word $/\$ Word concat
101	100	adantr 465	. . . . . . . . 9 Word $/\$ Word $/\$ ..^ concat
102	9	nn0zd 10737	. . . . . . . . . . . . 13 Word
103		peano2zm 10680	. . . . . . . . . . . . 13
104	102, 103	syl 16	. . . . . . . . . . . 12 Word
105	104	zcnd 10740	. . . . . . . . . . 11 Word
106	105	ad2antrr 725	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
107		elfzoelz 11545	. . . . . . . . . . . 12 ..^
108	107	zcnd 10740	. . . . . . . . . . 11 ..^
109	108	adantl 466	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
110	12	ad2antlr 726	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
111	106, 109, 110	subsub3d 9741	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
112	101, 111	eqtr4d 2473	. . . . . . . 8 Word $/\$ Word $/\$ ..^ concat
113	90	oveq2d 6102	. . . . . . . . . 10 Word $/\$ Word reverse
114	113	oveq2d 6102	. . . . . . . . 9 Word $/\$ Word reverse
115	114	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ reverse
116	112, 115	eqtr4d 2473	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat reverse
117	116	fveq2d 5690	. . . . . 6 Word $/\$ Word $/\$ ..^ concat reverse
118		simpll 753	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
119		simplr 754	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
120		zaddcl 10677	. . . . . . . . . . . 12 $/\$
121	37, 102, 120	syl2anr 478	. . . . . . . . . . 11 Word $/\$ Word
122		peano2zm 10680	. . . . . . . . . . 11
123	121, 122	syl 16	. . . . . . . . . 10 Word $/\$ Word
124	123	adantr 465	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
125		fzoval 11546	. . . . . . . . . . . 12 ..^
126	121, 125	syl 16	. . . . . . . . . . 11 Word $/\$ Word ..^
127	126	eleq2d 2505	. . . . . . . . . 10 Word $/\$ Word ..^
128	127	biimpa 484	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
129		fzrev2i 11513	. . . . . . . . 9 $/\$
130	124, 128, 129	syl2anc 661	. . . . . . . 8 Word $/\$ Word $/\$ ..^
131	53	oveq1d 6101	. . . . . . . . 9 Word $/\$ Word concat
132	131	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ concat
133	102	adantr 465	. . . . . . . . . . 11 Word $/\$ Word
134		fzoval 11546	. . . . . . . . . . 11 ..^
135	133, 134	syl 16	. . . . . . . . . 10 Word $/\$ Word ..^
136	123	zcnd 10740	. . . . . . . . . . . 12 Word $/\$ Word
137	136	subidd 9699	. . . . . . . . . . 11 Word $/\$ Word
138		addcl 9356	. . . . . . . . . . . . . 14 $/\$
139	12, 10, 138	syl2anr 478	. . . . . . . . . . . . 13 Word $/\$ Word
140	139, 57, 54	sub32d 9743	. . . . . . . . . . . 12 Word $/\$ Word
141		pncan2 9609	. . . . . . . . . . . . . 14 $/\$
142	12, 10, 141	syl2anr 478	. . . . . . . . . . . . 13 Word $/\$ Word
143	142	oveq1d 6101	. . . . . . . . . . . 12 Word $/\$ Word
144	140, 143	eqtrd 2470	. . . . . . . . . . 11 Word $/\$ Word
145	137, 144	oveq12d 6104	. . . . . . . . . 10 Word $/\$ Word
146	135, 145	eqtr4d 2473	. . . . . . . . 9 Word $/\$ Word ..^
147	146	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
148	130, 132, 147	3eltr4d 2519	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat ..^
149		ccatval1 12268	. . . . . . 7 Word $/\$ Word $/\$ concat ..^ concat concat concat
150	118, 119, 148, 149	syl3anc 1218	. . . . . 6 Word $/\$ Word $/\$ ..^ concat concat concat
151	29	ad2antlr 726	. . . . . . . . 9 Word $/\$ Word $/\$ ..^ reverse
152	151	oveq2d 6102	. . . . . . . 8 Word $/\$ Word $/\$ ..^ reverse
153		id 22	. . . . . . . . 9 ..^ ..^
154		fzosubel3 11593	. . . . . . . . 9 ..^ $/\$ ..^
155	153, 133, 154	syl2anr 478	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
156	152, 155	eqeltrd 2512	. . . . . . 7 Word $/\$ Word $/\$ ..^ reverse ..^
157		revfv 12395	. . . . . . 7 Word $/\$ reverse ..^ reverse reverse reverse
158	118, 156, 157	syl2anc 661	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse reverse reverse
159	117, 150, 158	3eqtr4d 2480	. . . . 5 Word $/\$ Word $/\$ ..^ concat concat reverse reverse
160	1	adantr 465	. . . . . 6 Word $/\$ Word $/\$ ..^ concat Word
161	11	adantl 466	. . . . . . . . 9 Word $/\$ Word
162		fzoss1 11568	. . . . . . . . . 10 ..^ ..^
163		nn0uz 10887	. . . . . . . . . 10
164	162, 163	eleq2s 2530	. . . . . . . . 9 ..^ ..^
165	161, 164	syl 16	. . . . . . . 8 Word $/\$ Word ..^ ..^
166	15	oveq2d 6102	. . . . . . . 8 Word $/\$ Word ..^ concat ..^
167	165, 166	sseqtr4d 3388	. . . . . . 7 Word $/\$ Word ..^ ..^ concat
168	167	sselda 3351	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^ concat
169	160, 168, 86	syl2anc 661	. . . . 5 Word $/\$ Word $/\$ ..^ reverse concat concat concat
170	20	ad2antlr 726	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
171	21	ad2antrr 725	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
172	90, 31	oveq12d 6104	. . . . . . . 8 Word $/\$ Word reverse..^reverse reverse ..^
173	172	eleq2d 2505	. . . . . . 7 Word $/\$ Word reverse..^reverse reverse ..^
174	173	biimpar 485	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse..^reverse reverse
175		ccatval2 12269	. . . . . 6 reverse Word $/\$ reverse Word $/\$ reverse..^reverse reverse reverse concat reverse reverse reverse
176	170, 171, 174, 175	syl3anc 1218	. . . . 5 Word $/\$ Word $/\$ ..^ reverse concat reverse reverse reverse
177	159, 169, 176	3eqtr4d 2480	. . . 4 Word $/\$ Word $/\$ ..^ reverse concat reverse concat reverse
178	96, 177	jaodan 783	. . 3 Word $/\$ Word $/\$ ..^ $\/$ ..^ reverse concat reverse concat reverse
179	40, 178	syldan 470	. 2 Word $/\$ Word $/\$ ..^ reverse concat reverse concat reverse
180	19, 35, 179	eqfnfvd 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

W3C validator