revccat - Metamath Proof Explorer

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

Theorem revccat 12697

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 12552	. . . 4 Word $/\$ Word concat Word
2		revcl 12692	. . . 4 concat Word reverse concat Word
3		wrdf 12513	. . . 4 reverse concat Word reverse concat ..^reverse concat
4		ffn 5729	. . . 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 12693	. . . . . . 7 concat Word reverse concat concat
7	1, 6	syl 16	. . . . . 6 Word $/\$ Word reverse concat concat
8		ccatlen 12553	. . . . . . 7 Word $/\$ Word concat
9		lencl 12522	. . . . . . . . 9 Word
10	9	nn0cnd 10850	. . . . . . . 8 Word
11		lencl 12522	. . . . . . . . 9 Word
12	11	nn0cnd 10850	. . . . . . . 8 Word
13		addcom 9761	. . . . . . . 8 $/\$
14	10, 12, 13	syl2an 477	. . . . . . 7 Word $/\$ Word
15	8, 14	eqtrd 2508	. . . . . 6 Word $/\$ Word concat
16	7, 15	eqtrd 2508	. . . . 5 Word $/\$ Word reverse concat
17	16	oveq2d 6298	. . . 4 Word $/\$ Word ..^reverse concat ..^
18	17	fneq2d 5670	. . 3 Word $/\$ Word reverse concat ..^reverse concat reverse concat ..^
19	5, 18	mpbid 210	. 2 Word $/\$ Word reverse concat ..^
20		revcl 12692	. . . . 5 Word reverse Word
21		revcl 12692	. . . . 5 Word reverse Word
22		ccatcl 12552	. . . . 5 reverse Word $/\$ reverse Word reverse concat reverse Word
23	20, 21, 22	syl2anr 478	. . . 4 Word $/\$ Word reverse concat reverse Word
24		wrdf 12513	. . . 4 reverse concat reverse Word reverse concat reverse..^reverse concat reverse
25		ffn 5729	. . . 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 12553	. . . . . . 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 12693	. . . . . . 7 Word reverse
30		revlen 12693	. . . . . . 7 Word reverse
31	29, 30	oveqan12rd 6302	. . . . . 6 Word $/\$ Word reverse reverse
32	28, 31	eqtrd 2508	. . . . 5 Word $/\$ Word reverse concat reverse
33	32	oveq2d 6298	. . . 4 Word $/\$ Word ..^reverse concat reverse ..^
34	33	fneq2d 5670	. . 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 10960	. . . . 5 Word
38	37	adantl 466	. . . 4 Word $/\$ Word
39		fzospliti 11821	. . . 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 11794	. . . . . . . . . . . 12 ..^
44	38, 43	syl 16	. . . . . . . . . . 11 Word $/\$ Word ..^
45	44	eleq2d 2537	. . . . . . . . . 10 Word $/\$ Word ..^
46	45	biimpa 484	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
47		fznn0sub2 11775	. . . . . . . . 9
48	46, 47	syl 16	. . . . . . . 8 Word $/\$ Word $/\$ ..^
49	44	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
50	48, 49	eleqtrrd 2558	. . . . . . 7 Word $/\$ Word $/\$ ..^ ..^
51		ccatval3 12556	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat
52	41, 42, 50, 51	syl3anc 1228	. . . . . 6 Word $/\$ Word $/\$ ..^ concat
53	15	oveq1d 6297	. . . . . . . . . . 11 Word $/\$ Word concat
54	12	adantl 466	. . . . . . . . . . . 12 Word $/\$ Word
55	10	adantr 465	. . . . . . . . . . . 12 Word $/\$ Word
56		ax-1cn 9546	. . . . . . . . . . . . 13
57	56	a1i 11	. . . . . . . . . . . 12 Word $/\$ Word
58	54, 55, 57	addsubd 9947	. . . . . . . . . . 11 Word $/\$ Word
59	53, 58	eqtrd 2508	. . . . . . . . . 10 Word $/\$ Word concat
60	59	oveq1d 6297	. . . . . . . . 9 Word $/\$ Word concat
61	60	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ concat
62		peano2zm 10902	. . . . . . . . . . . 12
63	37, 62	syl 16	. . . . . . . . . . 11 Word
64	63	zcnd 10963	. . . . . . . . . 10 Word
65	64	ad2antlr 726	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
66	10	ad2antrr 725	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
67		elfzoelz 11793	. . . . . . . . . . 11 ..^
68	67	zcnd 10963	. . . . . . . . . 10 ..^
69	68	adantl 466	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
70	65, 66, 69	addsubd 9947	. . . . . . . 8 Word $/\$ Word $/\$ ..^
71	61, 70	eqtrd 2508	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat
72	71	fveq2d 5868	. . . . . 6 Word $/\$ Word $/\$ ..^ concat concat concat
73		revfv 12694	. . . . . . 7 Word $/\$ ..^ reverse
74	73	adantll 713	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse
75	52, 72, 74	3eqtr4d 2518	. . . . 5 Word $/\$ Word $/\$ ..^ concat concat reverse
76	1	adantr 465	. . . . . 6 Word $/\$ Word $/\$ ..^ concat Word
77		uzid 11092	. . . . . . . . . . 11
78	38, 77	syl 16	. . . . . . . . . 10 Word $/\$ Word
79	9	adantr 465	. . . . . . . . . 10 Word $/\$ Word
80		uzaddcl 11133	. . . . . . . . . 10 $/\$
81	78, 79, 80	syl2anc 661	. . . . . . . . 9 Word $/\$ Word
82	15, 81	eqeltrd 2555	. . . . . . . 8 Word $/\$ Word concat
83		fzoss2 11817	. . . . . . . 8 concat ..^ ..^ concat
84	82, 83	syl 16	. . . . . . 7 Word $/\$ Word ..^ ..^ concat
85	84	sselda 3504	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^ concat
86		revfv 12694	. . . . . 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 6298	. . . . . . . 8 Word $/\$ Word ..^reverse ..^
92	91	eleq2d 2537	. . . . . . 7 Word $/\$ Word ..^reverse ..^
93	92	biimpar 485	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^reverse
94		ccatval1 12554	. . . . . 6 reverse Word $/\$ reverse Word $/\$ ..^reverse reverse concat reverse reverse
95	88, 89, 93, 94	syl3anc 1228	. . . . 5 Word $/\$ Word $/\$ ..^ reverse concat reverse reverse
96	75, 87, 95	3eqtr4d 2518	. . . 4 Word $/\$ Word $/\$ ..^ reverse concat reverse concat reverse
97	8	oveq1d 6297	. . . . . . . . . . . 12 Word $/\$ Word concat
98	55, 54, 57	addsubd 9947	. . . . . . . . . . . 12 Word $/\$ Word
99	97, 98	eqtrd 2508	. . . . . . . . . . 11 Word $/\$ Word concat
100	99	oveq1d 6297	. . . . . . . . . 10 Word $/\$ Word concat
101	100	adantr 465	. . . . . . . . 9 Word $/\$ Word $/\$ ..^ concat
102	9	nn0zd 10960	. . . . . . . . . . . . 13 Word
103		peano2zm 10902	. . . . . . . . . . . . 13
104	102, 103	syl 16	. . . . . . . . . . . 12 Word
105	104	zcnd 10963	. . . . . . . . . . 11 Word
106	105	ad2antrr 725	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
107		elfzoelz 11793	. . . . . . . . . . . 12 ..^
108	107	zcnd 10963	. . . . . . . . . . 11 ..^
109	108	adantl 466	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
110	12	ad2antlr 726	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
111	106, 109, 110	subsub3d 9956	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
112	101, 111	eqtr4d 2511	. . . . . . . 8 Word $/\$ Word $/\$ ..^ concat
113	90	oveq2d 6298	. . . . . . . . . 10 Word $/\$ Word reverse
114	113	oveq2d 6298	. . . . . . . . 9 Word $/\$ Word reverse
115	114	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ reverse
116	112, 115	eqtr4d 2511	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat reverse
117	116	fveq2d 5868	. . . . . 6 Word $/\$ Word $/\$ ..^ concat reverse
118		simpll 753	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
119		simplr 754	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
120		zaddcl 10899	. . . . . . . . . . . 12 $/\$
121	37, 102, 120	syl2anr 478	. . . . . . . . . . 11 Word $/\$ Word
122		peano2zm 10902	. . . . . . . . . . 11
123	121, 122	syl 16	. . . . . . . . . 10 Word $/\$ Word
124	123	adantr 465	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
125		fzoval 11794	. . . . . . . . . . . 12 ..^
126	121, 125	syl 16	. . . . . . . . . . 11 Word $/\$ Word ..^
127	126	eleq2d 2537	. . . . . . . . . 10 Word $/\$ Word ..^
128	127	biimpa 484	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
129		fzrev2i 11740	. . . . . . . . 9 $/\$
130	124, 128, 129	syl2anc 661	. . . . . . . 8 Word $/\$ Word $/\$ ..^
131	53	oveq1d 6297	. . . . . . . . 9 Word $/\$ Word concat
132	131	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ concat
133	102	adantr 465	. . . . . . . . . . 11 Word $/\$ Word
134		fzoval 11794	. . . . . . . . . . 11 ..^
135	133, 134	syl 16	. . . . . . . . . 10 Word $/\$ Word ..^
136	123	zcnd 10963	. . . . . . . . . . . 12 Word $/\$ Word
137	136	subidd 9914	. . . . . . . . . . 11 Word $/\$ Word
138		addcl 9570	. . . . . . . . . . . . . 14 $/\$
139	12, 10, 138	syl2anr 478	. . . . . . . . . . . . 13 Word $/\$ Word
140	139, 57, 54	sub32d 9958	. . . . . . . . . . . 12 Word $/\$ Word
141		pncan2 9823	. . . . . . . . . . . . . 14 $/\$
142	12, 10, 141	syl2anr 478	. . . . . . . . . . . . 13 Word $/\$ Word
143	142	oveq1d 6297	. . . . . . . . . . . 12 Word $/\$ Word
144	140, 143	eqtrd 2508	. . . . . . . . . . 11 Word $/\$ Word
145	137, 144	oveq12d 6300	. . . . . . . . . 10 Word $/\$ Word
146	135, 145	eqtr4d 2511	. . . . . . . . 9 Word $/\$ Word ..^
147	146	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
148	130, 132, 147	3eltr4d 2570	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat ..^
149		ccatval1 12554	. . . . . . 7 Word $/\$ Word $/\$ concat ..^ concat concat concat
150	118, 119, 148, 149	syl3anc 1228	. . . . . 6 Word $/\$ Word $/\$ ..^ concat concat concat
151	29	ad2antlr 726	. . . . . . . . 9 Word $/\$ Word $/\$ ..^ reverse
152	151	oveq2d 6298	. . . . . . . 8 Word $/\$ Word $/\$ ..^ reverse
153		id 22	. . . . . . . . 9 ..^ ..^
154		fzosubel3 11841	. . . . . . . . 9 ..^ $/\$ ..^
155	153, 133, 154	syl2anr 478	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
156	152, 155	eqeltrd 2555	. . . . . . 7 Word $/\$ Word $/\$ ..^ reverse ..^
157		revfv 12694	. . . . . . 7 Word $/\$ reverse ..^ reverse reverse reverse
158	118, 156, 157	syl2anc 661	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse reverse reverse
159	117, 150, 158	3eqtr4d 2518	. . . . 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 11816	. . . . . . . . . 10 ..^ ..^
163		nn0uz 11112	. . . . . . . . . 10
164	162, 163	eleq2s 2575	. . . . . . . . 9 ..^ ..^
165	161, 164	syl 16	. . . . . . . 8 Word $/\$ Word ..^ ..^
166	15	oveq2d 6298	. . . . . . . 8 Word $/\$ Word ..^ concat ..^
167	165, 166	sseqtr4d 3541	. . . . . . 7 Word $/\$ Word ..^ ..^ concat
168	167	sselda 3504	. . . . . 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 6300	. . . . . . . 8 Word $/\$ Word reverse..^reverse reverse ..^
173	172	eleq2d 2537	. . . . . . 7 Word $/\$ Word reverse..^reverse reverse ..^
174	173	biimpar 485	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse..^reverse reverse
175		ccatval2 12555	. . . . . 6 reverse Word $/\$ reverse Word $/\$ reverse..^reverse reverse reverse concat reverse reverse reverse
176	170, 171, 174, 175	syl3anc 1228	. . . . 5 Word $/\$ Word $/\$ ..^ reverse concat reverse reverse reverse
177	159, 169, 176	3eqtr4d 2518	. . . 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 5976	1 Word $/\$ Word reverse concat reverse concat reverse

Colors of variables: wff setvar class

Syntax hints:

wi 4 $\/$ wo 368 $/\$ wa 369

wceq 1379

wcel 1767

wss 3476

wfn 5581

wf 5582

cfv 5586 (class class class)co 6282

cc 9486

cc0 9488

c1 9489

caddc 9491

cmin 9801

cn0 10791

cz 10860

cuz 11078

cfz 11668 ..^cfzo 11788

chash 12367 Word cword 12494 concat cconcat 12496 reversecreverse 12500

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-om 6679 df-1st 6781 df-2nd 6782 df-recs 7039 df-rdg 7073 df-1o 7127 df-oadd 7131 df-er 7308 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-card 8316 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-nn 10533 df-n0 10792 df-z 10861 df-uz 11079 df-fz 11669 df-fzo 11789 df-hash 12368 df-word 12502 df-concat 12504 df-reverse 12508

This theorem is referenced by: gsumwrev 16193 efginvrel2 16538

W3C validator