revccat - Metamath Proof Explorer

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

Theorem revccat 12525

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 12393	. . . 4 Word $/\$ Word concat Word
2		revcl 12520	. . . 4 concat Word reverse concat Word
3		wrdf 12359	. . . 4 reverse concat Word reverse concat ..^reverse concat
4		ffn 5668	. . . 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 12521	. . . . . . 7 concat Word reverse concat concat
7	1, 6	syl 16	. . . . . 6 Word $/\$ Word reverse concat concat
8		ccatlen 12394	. . . . . . 7 Word $/\$ Word concat
9		lencl 12368	. . . . . . . . 9 Word
10	9	nn0cnd 10750	. . . . . . . 8 Word
11		lencl 12368	. . . . . . . . 9 Word
12	11	nn0cnd 10750	. . . . . . . 8 Word
13		addcom 9667	. . . . . . . 8 $/\$
14	10, 12, 13	syl2an 477	. . . . . . 7 Word $/\$ Word
15	8, 14	eqtrd 2495	. . . . . 6 Word $/\$ Word concat
16	7, 15	eqtrd 2495	. . . . 5 Word $/\$ Word reverse concat
17	16	oveq2d 6217	. . . 4 Word $/\$ Word ..^reverse concat ..^
18	17	fneq2d 5611	. . 3 Word $/\$ Word reverse concat ..^reverse concat reverse concat ..^
19	5, 18	mpbid 210	. 2 Word $/\$ Word reverse concat ..^
20		revcl 12520	. . . . 5 Word reverse Word
21		revcl 12520	. . . . 5 Word reverse Word
22		ccatcl 12393	. . . . 5 reverse Word $/\$ reverse Word reverse concat reverse Word
23	20, 21, 22	syl2anr 478	. . . 4 Word $/\$ Word reverse concat reverse Word
24		wrdf 12359	. . . 4 reverse concat reverse Word reverse concat reverse..^reverse concat reverse
25		ffn 5668	. . . 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 12394	. . . . . . 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 12521	. . . . . . 7 Word reverse
30		revlen 12521	. . . . . . 7 Word reverse
31	29, 30	oveqan12rd 6221	. . . . . 6 Word $/\$ Word reverse reverse
32	28, 31	eqtrd 2495	. . . . 5 Word $/\$ Word reverse concat reverse
33	32	oveq2d 6217	. . . 4 Word $/\$ Word ..^reverse concat reverse ..^
34	33	fneq2d 5611	. . 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 10857	. . . . 5 Word
38	37	adantl 466	. . . 4 Word $/\$ Word
39		fzospliti 11699	. . . 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 11672	. . . . . . . . . . . 12 ..^
44	38, 43	syl 16	. . . . . . . . . . 11 Word $/\$ Word ..^
45	44	eleq2d 2524	. . . . . . . . . 10 Word $/\$ Word ..^
46	45	biimpa 484	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
47		fznn0sub2 11606	. . . . . . . . 9
48	46, 47	syl 16	. . . . . . . 8 Word $/\$ Word $/\$ ..^
49	44	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
50	48, 49	eleqtrrd 2545	. . . . . . 7 Word $/\$ Word $/\$ ..^ ..^
51		ccatval3 12397	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat
52	41, 42, 50, 51	syl3anc 1219	. . . . . 6 Word $/\$ Word $/\$ ..^ concat
53	15	oveq1d 6216	. . . . . . . . . . 11 Word $/\$ Word concat
54	12	adantl 466	. . . . . . . . . . . 12 Word $/\$ Word
55	10	adantr 465	. . . . . . . . . . . 12 Word $/\$ Word
56		ax-1cn 9452	. . . . . . . . . . . . 13
57	56	a1i 11	. . . . . . . . . . . 12 Word $/\$ Word
58	54, 55, 57	addsubd 9852	. . . . . . . . . . 11 Word $/\$ Word
59	53, 58	eqtrd 2495	. . . . . . . . . 10 Word $/\$ Word concat
60	59	oveq1d 6216	. . . . . . . . 9 Word $/\$ Word concat
61	60	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ concat
62		peano2zm 10800	. . . . . . . . . . . 12
63	37, 62	syl 16	. . . . . . . . . . 11 Word
64	63	zcnd 10860	. . . . . . . . . 10 Word
65	64	ad2antlr 726	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
66	10	ad2antrr 725	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
67		elfzoelz 11671	. . . . . . . . . . 11 ..^
68	67	zcnd 10860	. . . . . . . . . 10 ..^
69	68	adantl 466	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
70	65, 66, 69	addsubd 9852	. . . . . . . 8 Word $/\$ Word $/\$ ..^
71	61, 70	eqtrd 2495	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat
72	71	fveq2d 5804	. . . . . 6 Word $/\$ Word $/\$ ..^ concat concat concat
73		revfv 12522	. . . . . . 7 Word $/\$ ..^ reverse
74	73	adantll 713	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse
75	52, 72, 74	3eqtr4d 2505	. . . . 5 Word $/\$ Word $/\$ ..^ concat concat reverse
76	1	adantr 465	. . . . . 6 Word $/\$ Word $/\$ ..^ concat Word
77		uzid 10987	. . . . . . . . . . 11
78	38, 77	syl 16	. . . . . . . . . 10 Word $/\$ Word
79	9	adantr 465	. . . . . . . . . 10 Word $/\$ Word
80		uzaddcl 11023	. . . . . . . . . 10 $/\$
81	78, 79, 80	syl2anc 661	. . . . . . . . 9 Word $/\$ Word
82	15, 81	eqeltrd 2542	. . . . . . . 8 Word $/\$ Word concat
83		fzoss2 11695	. . . . . . . 8 concat ..^ ..^ concat
84	82, 83	syl 16	. . . . . . 7 Word $/\$ Word ..^ ..^ concat
85	84	sselda 3465	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^ concat
86		revfv 12522	. . . . . 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 6217	. . . . . . . 8 Word $/\$ Word ..^reverse ..^
92	91	eleq2d 2524	. . . . . . 7 Word $/\$ Word ..^reverse ..^
93	92	biimpar 485	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^reverse
94		ccatval1 12395	. . . . . 6 reverse Word $/\$ reverse Word $/\$ ..^reverse reverse concat reverse reverse
95	88, 89, 93, 94	syl3anc 1219	. . . . 5 Word $/\$ Word $/\$ ..^ reverse concat reverse reverse
96	75, 87, 95	3eqtr4d 2505	. . . 4 Word $/\$ Word $/\$ ..^ reverse concat reverse concat reverse
97	8	oveq1d 6216	. . . . . . . . . . . 12 Word $/\$ Word concat
98	55, 54, 57	addsubd 9852	. . . . . . . . . . . 12 Word $/\$ Word
99	97, 98	eqtrd 2495	. . . . . . . . . . 11 Word $/\$ Word concat
100	99	oveq1d 6216	. . . . . . . . . 10 Word $/\$ Word concat
101	100	adantr 465	. . . . . . . . 9 Word $/\$ Word $/\$ ..^ concat
102	9	nn0zd 10857	. . . . . . . . . . . . 13 Word
103		peano2zm 10800	. . . . . . . . . . . . 13
104	102, 103	syl 16	. . . . . . . . . . . 12 Word
105	104	zcnd 10860	. . . . . . . . . . 11 Word
106	105	ad2antrr 725	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
107		elfzoelz 11671	. . . . . . . . . . . 12 ..^
108	107	zcnd 10860	. . . . . . . . . . 11 ..^
109	108	adantl 466	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
110	12	ad2antlr 726	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
111	106, 109, 110	subsub3d 9861	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
112	101, 111	eqtr4d 2498	. . . . . . . 8 Word $/\$ Word $/\$ ..^ concat
113	90	oveq2d 6217	. . . . . . . . . 10 Word $/\$ Word reverse
114	113	oveq2d 6217	. . . . . . . . 9 Word $/\$ Word reverse
115	114	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ reverse
116	112, 115	eqtr4d 2498	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat reverse
117	116	fveq2d 5804	. . . . . 6 Word $/\$ Word $/\$ ..^ concat reverse
118		simpll 753	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
119		simplr 754	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
120		zaddcl 10797	. . . . . . . . . . . 12 $/\$
121	37, 102, 120	syl2anr 478	. . . . . . . . . . 11 Word $/\$ Word
122		peano2zm 10800	. . . . . . . . . . 11
123	121, 122	syl 16	. . . . . . . . . 10 Word $/\$ Word
124	123	adantr 465	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
125		fzoval 11672	. . . . . . . . . . . 12 ..^
126	121, 125	syl 16	. . . . . . . . . . 11 Word $/\$ Word ..^
127	126	eleq2d 2524	. . . . . . . . . 10 Word $/\$ Word ..^
128	127	biimpa 484	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
129		fzrev2i 11639	. . . . . . . . 9 $/\$
130	124, 128, 129	syl2anc 661	. . . . . . . 8 Word $/\$ Word $/\$ ..^
131	53	oveq1d 6216	. . . . . . . . 9 Word $/\$ Word concat
132	131	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ concat
133	102	adantr 465	. . . . . . . . . . 11 Word $/\$ Word
134		fzoval 11672	. . . . . . . . . . 11 ..^
135	133, 134	syl 16	. . . . . . . . . 10 Word $/\$ Word ..^
136	123	zcnd 10860	. . . . . . . . . . . 12 Word $/\$ Word
137	136	subidd 9819	. . . . . . . . . . 11 Word $/\$ Word
138		addcl 9476	. . . . . . . . . . . . . 14 $/\$
139	12, 10, 138	syl2anr 478	. . . . . . . . . . . . 13 Word $/\$ Word
140	139, 57, 54	sub32d 9863	. . . . . . . . . . . 12 Word $/\$ Word
141		pncan2 9729	. . . . . . . . . . . . . 14 $/\$
142	12, 10, 141	syl2anr 478	. . . . . . . . . . . . 13 Word $/\$ Word
143	142	oveq1d 6216	. . . . . . . . . . . 12 Word $/\$ Word
144	140, 143	eqtrd 2495	. . . . . . . . . . 11 Word $/\$ Word
145	137, 144	oveq12d 6219	. . . . . . . . . 10 Word $/\$ Word
146	135, 145	eqtr4d 2498	. . . . . . . . 9 Word $/\$ Word ..^
147	146	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
148	130, 132, 147	3eltr4d 2557	. . . . . . 7 Word $/\$ Word $/\$ ..^ concat ..^
149		ccatval1 12395	. . . . . . 7 Word $/\$ Word $/\$ concat ..^ concat concat concat
150	118, 119, 148, 149	syl3anc 1219	. . . . . 6 Word $/\$ Word $/\$ ..^ concat concat concat
151	29	ad2antlr 726	. . . . . . . . 9 Word $/\$ Word $/\$ ..^ reverse
152	151	oveq2d 6217	. . . . . . . 8 Word $/\$ Word $/\$ ..^ reverse
153		id 22	. . . . . . . . 9 ..^ ..^
154		fzosubel3 11719	. . . . . . . . 9 ..^ $/\$ ..^
155	153, 133, 154	syl2anr 478	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
156	152, 155	eqeltrd 2542	. . . . . . 7 Word $/\$ Word $/\$ ..^ reverse ..^
157		revfv 12522	. . . . . . 7 Word $/\$ reverse ..^ reverse reverse reverse
158	118, 156, 157	syl2anc 661	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse reverse reverse
159	117, 150, 158	3eqtr4d 2505	. . . . 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 11694	. . . . . . . . . 10 ..^ ..^
163		nn0uz 11007	. . . . . . . . . 10
164	162, 163	eleq2s 2562	. . . . . . . . 9 ..^ ..^
165	161, 164	syl 16	. . . . . . . 8 Word $/\$ Word ..^ ..^
166	15	oveq2d 6217	. . . . . . . 8 Word $/\$ Word ..^ concat ..^
167	165, 166	sseqtr4d 3502	. . . . . . 7 Word $/\$ Word ..^ ..^ concat
168	167	sselda 3465	. . . . . 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 6219	. . . . . . . 8 Word $/\$ Word reverse..^reverse reverse ..^
173	172	eleq2d 2524	. . . . . . 7 Word $/\$ Word reverse..^reverse reverse ..^
174	173	biimpar 485	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse..^reverse reverse
175		ccatval2 12396	. . . . . 6 reverse Word $/\$ reverse Word $/\$ reverse..^reverse reverse reverse concat reverse reverse reverse
176	170, 171, 174, 175	syl3anc 1219	. . . . 5 Word $/\$ Word $/\$ ..^ reverse concat reverse reverse reverse
177	159, 169, 176	3eqtr4d 2505	. . . 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 5910	1 Word $/\$ Word reverse concat reverse concat reverse

Colors of variables: wff setvar class

Syntax hints:

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

wceq 1370

wcel 1758

wss 3437

wfn 5522

wf 5523

cfv 5527 (class class class)co 6201

cc 9392

cc0 9394

c1 9395

caddc 9397

cmin 9707

cn0 10691

cz 10758

cuz 10973

cfz 11555 ..^cfzo 11666

chash 12221 Word cword 12340 concat cconcat 12342 reversecreverse 12346

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4512 ax-sep 4522 ax-nul 4530 ax-pow 4579 ax-pr 4640 ax-un 6483 ax-cnex 9450 ax-resscn 9451 ax-1cn 9452 ax-icn 9453 ax-addcl 9454 ax-addrcl 9455 ax-mulcl 9456 ax-mulrcl 9457 ax-mulcom 9458 ax-addass 9459 ax-mulass 9460 ax-distr 9461 ax-i2m1 9462 ax-1ne0 9463 ax-1rid 9464 ax-rnegex 9465 ax-rrecex 9466 ax-cnre 9467 ax-pre-lttri 9468 ax-pre-lttrn 9469 ax-pre-ltadd 9470 ax-pre-mulgt0 9471

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-nel 2651 df-ral 2804 df-rex 2805 df-reu 2806 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3747 df-if 3901 df-pw 3971 df-sn 3987 df-pr 3989 df-tp 3991 df-op 3993 df-uni 4201 df-int 4238 df-iun 4282 df-br 4402 df-opab 4460 df-mpt 4461 df-tr 4495 df-eprel 4741 df-id 4745 df-po 4750 df-so 4751 df-fr 4788 df-we 4790 df-ord 4831 df-on 4832 df-lim 4833 df-suc 4834 df-xp 4955 df-rel 4956 df-cnv 4957 df-co 4958 df-dm 4959 df-rn 4960 df-res 4961 df-ima 4962 df-iota 5490 df-fun 5529 df-fn 5530 df-f 5531 df-f1 5532 df-fo 5533 df-f1o 5534 df-fv 5535 df-riota 6162 df-ov 6204 df-oprab 6205 df-mpt2 6206 df-om 6588 df-1st 6688 df-2nd 6689 df-recs 6943 df-rdg 6977 df-1o 7031 df-oadd 7035 df-er 7212 df-en 7422 df-dom 7423 df-sdom 7424 df-fin 7425 df-card 8221 df-pnf 9532 df-mnf 9533 df-xr 9534 df-ltxr 9535 df-le 9536 df-sub 9709 df-neg 9710 df-nn 10435 df-n0 10692 df-z 10759 df-uz 10974 df-fz 11556 df-fzo 11667 df-hash 12222 df-word 12348 df-concat 12350 df-reverse 12354

This theorem is referenced by: gsumwrev 16001 efginvrel2 16346

W3C validator