revccat

Description: Antiautomorphic property of the reversal operation. (Contributed by Stefan O'Rear, 27-Aug-2015)

		Ref	Expression
	Assertion	revccat	$⊢ (S \in Word A \land T \in Word A) \to reverse (S ++ T) = reverse (T) ++ reverse (S)$

Proof

Step	Hyp	Ref	Expression
1		ccatcl	$⊢ (S \in Word A \land T \in Word A) \to S ++ T \in Word A$
2		revcl	$⊢ S ++ T \in Word A \to reverse (S ++ T) \in Word A$
3		wrdfn	$⊢ reverse (S ++ T) \in Word A \to reverse (S ++ T) Fn (0 ..^\|reverse (S ++ T)\|)$
4	1 2 3	3syl	$⊢ (S \in Word A \land T \in Word A) \to reverse (S ++ T) Fn (0 ..^\|reverse (S ++ T)\|)$
5		revlen	$⊢ S ++ T \in Word A \to \|reverse (S ++ T)\| = \|S ++ T\|$
6	1 5	syl	$⊢ (S \in Word A \land T \in Word A) \to \|reverse (S ++ T)\| = \|S ++ T\|$
7		ccatlen	$⊢ (S \in Word A \land T \in Word A) \to \|S ++ T\| = \|S\| + \|T\|$
8		lencl	$⊢ S \in Word A \to \|S\| \in ℕ_{0}$
9	8	nn0cnd	$⊢ S \in Word A \to \|S\| \in ℂ$
10		lencl	$⊢ T \in Word A \to \|T\| \in ℕ_{0}$
11	10	nn0cnd	$⊢ T \in Word A \to \|T\| \in ℂ$
12		addcom	$⊢ (\|S\| \in ℂ \land \|T\| \in ℂ) \to \|S\| + \|T\| = \|T\| + \|S\|$
13	9 11 12	syl2an	$⊢ (S \in Word A \land T \in Word A) \to \|S\| + \|T\| = \|T\| + \|S\|$
14	6 7 13	3eqtrd	$⊢ (S \in Word A \land T \in Word A) \to \|reverse (S ++ T)\| = \|T\| + \|S\|$
15	14	oveq2d	$⊢ (S \in Word A \land T \in Word A) \to (0 ..^\|reverse (S ++ T)\|) = (0 ..^\|T\| + \|S\|)$
16	15	fneq2d	$⊢ (S \in Word A \land T \in Word A) \to (reverse (S ++ T) Fn (0 ..^\|reverse (S ++ T)\|) \leftrightarrow reverse (S ++ T) Fn (0 ..^\|T\| + \|S\|))$
17	4 16	mpbid	$⊢ (S \in Word A \land T \in Word A) \to reverse (S ++ T) Fn (0 ..^\|T\| + \|S\|)$
18		revcl	$⊢ T \in Word A \to reverse (T) \in Word A$
19		revcl	$⊢ S \in Word A \to reverse (S) \in Word A$
20		ccatcl	$⊢ (reverse (T) \in Word A \land reverse (S) \in Word A) \to reverse (T) ++ reverse (S) \in Word A$
21	18 19 20	syl2anr	$⊢ (S \in Word A \land T \in Word A) \to reverse (T) ++ reverse (S) \in Word A$
22		wrdfn	$⊢ reverse (T) ++ reverse (S) \in Word A \to (reverse (T) ++ reverse (S)) Fn (0 ..^\|reverse (T) ++ reverse (S)\|)$
23	21 22	syl	$⊢ (S \in Word A \land T \in Word A) \to (reverse (T) ++ reverse (S)) Fn (0 ..^\|reverse (T) ++ reverse (S)\|)$
24		ccatlen	$⊢ (reverse (T) \in Word A \land reverse (S) \in Word A) \to \|reverse (T) ++ reverse (S)\| = \|reverse (T)\| + \|reverse (S)\|$
25	18 19 24	syl2anr	$⊢ (S \in Word A \land T \in Word A) \to \|reverse (T) ++ reverse (S)\| = \|reverse (T)\| + \|reverse (S)\|$
26		revlen	$⊢ T \in Word A \to \|reverse (T)\| = \|T\|$
27		revlen	$⊢ S \in Word A \to \|reverse (S)\| = \|S\|$
28	26 27	oveqan12rd	$⊢ (S \in Word A \land T \in Word A) \to \|reverse (T)\| + \|reverse (S)\| = \|T\| + \|S\|$
29	25 28	eqtrd	$⊢ (S \in Word A \land T \in Word A) \to \|reverse (T) ++ reverse (S)\| = \|T\| + \|S\|$
30	29	oveq2d	$⊢ (S \in Word A \land T \in Word A) \to (0 ..^\|reverse (T) ++ reverse (S)\|) = (0 ..^\|T\| + \|S\|)$
31	30	fneq2d	$⊢ (S \in Word A \land T \in Word A) \to ((reverse (T) ++ reverse (S)) Fn (0 ..^\|reverse (T) ++ reverse (S)\|) \leftrightarrow (reverse (T) ++ reverse (S)) Fn (0 ..^\|T\| + \|S\|))$
32	23 31	mpbid	$⊢ (S \in Word A \land T \in Word A) \to (reverse (T) ++ reverse (S)) Fn (0 ..^\|T\| + \|S\|)$
33		id	$⊢ x \in (0 ..^\|T\| + \|S\|) \to x \in (0 ..^\|T\| + \|S\|)$
34	10	nn0zd	$⊢ T \in Word A \to \|T\| \in ℤ$
35	34	adantl	$⊢ (S \in Word A \land T \in Word A) \to \|T\| \in ℤ$
36		fzospliti	$⊢ (x \in (0 ..^\|T\| + \|S\|) \land \|T\| \in ℤ) \to (x \in (0 ..^\|T\|) \lor x \in (\|T\| ..^\|T\| + \|S\|))$
37	33 35 36	syl2anr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\| + \|S\|)) \to (x \in (0 ..^\|T\|) \lor x \in (\|T\| ..^\|T\| + \|S\|))$
38		simpll	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to S \in Word A$
39		simplr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to T \in Word A$
40		fzoval	$⊢ \|T\| \in ℤ \to (0 ..^\|T\|) = (0 \dots \|T\| - 1)$
41	34 40	syl	$⊢ T \in Word A \to (0 ..^\|T\|) = (0 \dots \|T\| - 1)$
42	41	adantl	$⊢ (S \in Word A \land T \in Word A) \to (0 ..^\|T\|) = (0 \dots \|T\| - 1)$
43	42	eleq2d	$⊢ (S \in Word A \land T \in Word A) \to (x \in (0 ..^\|T\|) \leftrightarrow x \in (0 \dots \|T\| - 1))$
44	43	biimpa	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to x \in (0 \dots \|T\| - 1)$
45		fznn0sub2	$⊢ x \in (0 \dots \|T\| - 1) \to \|T\| - 1 - x \in (0 \dots \|T\| - 1)$
46	44 45	syl	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to \|T\| - 1 - x \in (0 \dots \|T\| - 1)$
47	41	ad2antlr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to (0 ..^\|T\|) = (0 \dots \|T\| - 1)$
48	46 47	eleqtrrd	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to \|T\| - 1 - x \in (0 ..^\|T\|)$
49		ccatval3	$⊢ (S \in Word A \land T \in Word A \land \|T\| - 1 - x \in (0 ..^\|T\|)) \to (S ++ T) ((\|T\| - 1) - x + \|S\|) = T (\|T\| - 1 - x)$
50	38 39 48 49	syl3anc	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to (S ++ T) ((\|T\| - 1) - x + \|S\|) = T (\|T\| - 1 - x)$
51	7 13	eqtrd	$⊢ (S \in Word A \land T \in Word A) \to \|S ++ T\| = \|T\| + \|S\|$
52	51	oveq1d	$⊢ (S \in Word A \land T \in Word A) \to \|S ++ T\| - 1 = \|T\| + \|S\| - 1$
53	11	adantl	$⊢ (S \in Word A \land T \in Word A) \to \|T\| \in ℂ$
54	9	adantr	$⊢ (S \in Word A \land T \in Word A) \to \|S\| \in ℂ$
55		1cnd	$⊢ (S \in Word A \land T \in Word A) \to 1 \in ℂ$
56	53 54 55	addsubd	$⊢ (S \in Word A \land T \in Word A) \to \|T\| + \|S\| - 1 = \|T\| - 1 + \|S\|$
57	52 56	eqtrd	$⊢ (S \in Word A \land T \in Word A) \to \|S ++ T\| - 1 = \|T\| - 1 + \|S\|$
58	57	oveq1d	$⊢ (S \in Word A \land T \in Word A) \to \|S ++ T\| - 1 - x = (\|T\| - 1) + \|S\| - x$
59	58	adantr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to \|S ++ T\| - 1 - x = (\|T\| - 1) + \|S\| - x$
60		peano2zm	$⊢ \|T\| \in ℤ \to \|T\| - 1 \in ℤ$
61	34 60	syl	$⊢ T \in Word A \to \|T\| - 1 \in ℤ$
62	61	zcnd	$⊢ T \in Word A \to \|T\| - 1 \in ℂ$
63	62	ad2antlr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to \|T\| - 1 \in ℂ$
64	9	ad2antrr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to \|S\| \in ℂ$
65		elfzoelz	$⊢ x \in (0 ..^\|T\|) \to x \in ℤ$
66	65	zcnd	$⊢ x \in (0 ..^\|T\|) \to x \in ℂ$
67	66	adantl	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to x \in ℂ$
68	63 64 67	addsubd	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to (\|T\| - 1) + \|S\| - x = (\|T\| - 1) - x + \|S\|$
69	59 68	eqtrd	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to \|S ++ T\| - 1 - x = (\|T\| - 1) - x + \|S\|$
70	69	fveq2d	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to (S ++ T) (\|S ++ T\| - 1 - x) = (S ++ T) ((\|T\| - 1) - x + \|S\|)$
71		revfv	$⊢ (T \in Word A \land x \in (0 ..^\|T\|)) \to reverse (T) (x) = T (\|T\| - 1 - x)$
72	71	adantll	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to reverse (T) (x) = T (\|T\| - 1 - x)$
73	50 70 72	3eqtr4d	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to (S ++ T) (\|S ++ T\| - 1 - x) = reverse (T) (x)$
74	34	uzidd	$⊢ T \in Word A \to \|T\| \in ℤ_{\geq \|T\|}$
75		uzaddcl	$⊢ (\|T\| \in ℤ_{\geq \|T\|} \land \|S\| \in ℕ_{0}) \to \|T\| + \|S\| \in ℤ_{\geq \|T\|}$
76	74 8 75	syl2anr	$⊢ (S \in Word A \land T \in Word A) \to \|T\| + \|S\| \in ℤ_{\geq \|T\|}$
77	51 76	eqeltrd	$⊢ (S \in Word A \land T \in Word A) \to \|S ++ T\| \in ℤ_{\geq \|T\|}$
78		fzoss2	$⊢ \|S ++ T\| \in ℤ_{\geq \|T\|} \to (0 ..^\|T\|) \subseteq (0 ..^\|S ++ T\|)$
79	77 78	syl	$⊢ (S \in Word A \land T \in Word A) \to (0 ..^\|T\|) \subseteq (0 ..^\|S ++ T\|)$
80	79	sselda	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to x \in (0 ..^\|S ++ T\|)$
81		revfv	$⊢ (S ++ T \in Word A \land x \in (0 ..^\|S ++ T\|)) \to reverse (S ++ T) (x) = (S ++ T) (\|S ++ T\| - 1 - x)$
82	1 80 81	syl2an2r	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to reverse (S ++ T) (x) = (S ++ T) (\|S ++ T\| - 1 - x)$
83	18	ad2antlr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to reverse (T) \in Word A$
84	19	ad2antrr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to reverse (S) \in Word A$
85	26	adantl	$⊢ (S \in Word A \land T \in Word A) \to \|reverse (T)\| = \|T\|$
86	85	oveq2d	$⊢ (S \in Word A \land T \in Word A) \to (0 ..^\|reverse (T)\|) = (0 ..^\|T\|)$
87	86	eleq2d	$⊢ (S \in Word A \land T \in Word A) \to (x \in (0 ..^\|reverse (T)\|) \leftrightarrow x \in (0 ..^\|T\|))$
88	87	biimpar	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to x \in (0 ..^\|reverse (T)\|)$
89		ccatval1	$⊢ (reverse (T) \in Word A \land reverse (S) \in Word A \land x \in (0 ..^\|reverse (T)\|)) \to (reverse (T) ++ reverse (S)) (x) = reverse (T) (x)$
90	83 84 88 89	syl3anc	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to (reverse (T) ++ reverse (S)) (x) = reverse (T) (x)$
91	73 82 90	3eqtr4d	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\|)) \to reverse (S ++ T) (x) = (reverse (T) ++ reverse (S)) (x)$
92	8	nn0zd	$⊢ S \in Word A \to \|S\| \in ℤ$
93		peano2zm	$⊢ \|S\| \in ℤ \to \|S\| - 1 \in ℤ$
94	92 93	syl	$⊢ S \in Word A \to \|S\| - 1 \in ℤ$
95	94	zcnd	$⊢ S \in Word A \to \|S\| - 1 \in ℂ$
96	95	ad2antrr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to \|S\| - 1 \in ℂ$
97		elfzoelz	$⊢ x \in (\|T\| ..^\|T\| + \|S\|) \to x \in ℤ$
98	97	zcnd	$⊢ x \in (\|T\| ..^\|T\| + \|S\|) \to x \in ℂ$
99	98	adantl	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to x \in ℂ$
100	11	ad2antlr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to \|T\| \in ℂ$
101	96 99 100	subsub3d	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to \|S\| - 1 - (x - \|T\|) = (\|S\| - 1) + \|T\| - x$
102	26	oveq2d	$⊢ T \in Word A \to x - \|reverse (T)\| = x - \|T\|$
103	102	oveq2d	$⊢ T \in Word A \to \|S\| - 1 - (x - \|reverse (T)\|) = \|S\| - 1 - (x - \|T\|)$
104	103	ad2antlr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to \|S\| - 1 - (x - \|reverse (T)\|) = \|S\| - 1 - (x - \|T\|)$
105	7	oveq1d	$⊢ (S \in Word A \land T \in Word A) \to \|S ++ T\| - 1 = \|S\| + \|T\| - 1$
106	54 53 55	addsubd	$⊢ (S \in Word A \land T \in Word A) \to \|S\| + \|T\| - 1 = \|S\| - 1 + \|T\|$
107	105 106	eqtrd	$⊢ (S \in Word A \land T \in Word A) \to \|S ++ T\| - 1 = \|S\| - 1 + \|T\|$
108	107	oveq1d	$⊢ (S \in Word A \land T \in Word A) \to \|S ++ T\| - 1 - x = (\|S\| - 1) + \|T\| - x$
109	108	adantr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to \|S ++ T\| - 1 - x = (\|S\| - 1) + \|T\| - x$
110	101 104 109	3eqtr4rd	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to \|S ++ T\| - 1 - x = \|S\| - 1 - (x - \|reverse (T)\|)$
111	110	fveq2d	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to S (\|S ++ T\| - 1 - x) = S (\|S\| - 1 - (x - \|reverse (T)\|))$
112		simpll	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to S \in Word A$
113		simplr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to T \in Word A$
114		zaddcl	$⊢ (\|T\| \in ℤ \land \|S\| \in ℤ) \to \|T\| + \|S\| \in ℤ$
115	34 92 114	syl2anr	$⊢ (S \in Word A \land T \in Word A) \to \|T\| + \|S\| \in ℤ$
116		peano2zm	$⊢ \|T\| + \|S\| \in ℤ \to \|T\| + \|S\| - 1 \in ℤ$
117	115 116	syl	$⊢ (S \in Word A \land T \in Word A) \to \|T\| + \|S\| - 1 \in ℤ$
118		fzoval	$⊢ \|T\| + \|S\| \in ℤ \to (\|T\| ..^\|T\| + \|S\|) = (\|T\| \dots \|T\| + \|S\| - 1)$
119	115 118	syl	$⊢ (S \in Word A \land T \in Word A) \to (\|T\| ..^\|T\| + \|S\|) = (\|T\| \dots \|T\| + \|S\| - 1)$
120	119	eleq2d	$⊢ (S \in Word A \land T \in Word A) \to (x \in (\|T\| ..^\|T\| + \|S\|) \leftrightarrow x \in (\|T\| \dots \|T\| + \|S\| - 1))$
121	120	biimpa	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to x \in (\|T\| \dots \|T\| + \|S\| - 1)$
122		fzrev2i	$⊢ (\|T\| + \|S\| - 1 \in ℤ \land x \in (\|T\| \dots \|T\| + \|S\| - 1)) \to (\|T\| + \|S\|) - 1 - x \in ((\|T\| + \|S\|) - 1 - (\|T\| + \|S\| - 1) \dots (\|T\| + \|S\|) - 1 - \|T\|)$
123	117 121 122	syl2an2r	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to (\|T\| + \|S\|) - 1 - x \in ((\|T\| + \|S\|) - 1 - (\|T\| + \|S\| - 1) \dots (\|T\| + \|S\|) - 1 - \|T\|)$
124	52	oveq1d	$⊢ (S \in Word A \land T \in Word A) \to \|S ++ T\| - 1 - x = (\|T\| + \|S\|) - 1 - x$
125	124	adantr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to \|S ++ T\| - 1 - x = (\|T\| + \|S\|) - 1 - x$
126	92	adantr	$⊢ (S \in Word A \land T \in Word A) \to \|S\| \in ℤ$
127		fzoval	$⊢ \|S\| \in ℤ \to (0 ..^\|S\|) = (0 \dots \|S\| - 1)$
128	126 127	syl	$⊢ (S \in Word A \land T \in Word A) \to (0 ..^\|S\|) = (0 \dots \|S\| - 1)$
129	117	zcnd	$⊢ (S \in Word A \land T \in Word A) \to \|T\| + \|S\| - 1 \in ℂ$
130	129	subidd	$⊢ (S \in Word A \land T \in Word A) \to (\|T\| + \|S\|) - 1 - (\|T\| + \|S\| - 1) = 0$
131		addcl	$⊢ (\|T\| \in ℂ \land \|S\| \in ℂ) \to \|T\| + \|S\| \in ℂ$
132	11 9 131	syl2anr	$⊢ (S \in Word A \land T \in Word A) \to \|T\| + \|S\| \in ℂ$
133	132 55 53	sub32d	$⊢ (S \in Word A \land T \in Word A) \to (\|T\| + \|S\|) - 1 - \|T\| = (\|T\| + \|S\|) - \|T\| - 1$
134		pncan2	$⊢ (\|T\| \in ℂ \land \|S\| \in ℂ) \to \|T\| + \|S\| - \|T\| = \|S\|$
135	11 9 134	syl2anr	$⊢ (S \in Word A \land T \in Word A) \to \|T\| + \|S\| - \|T\| = \|S\|$
136	135	oveq1d	$⊢ (S \in Word A \land T \in Word A) \to (\|T\| + \|S\|) - \|T\| - 1 = \|S\| - 1$
137	133 136	eqtrd	$⊢ (S \in Word A \land T \in Word A) \to (\|T\| + \|S\|) - 1 - \|T\| = \|S\| - 1$
138	130 137	oveq12d	$⊢ (S \in Word A \land T \in Word A) \to ((\|T\| + \|S\|) - 1 - (\|T\| + \|S\| - 1) \dots (\|T\| + \|S\|) - 1 - \|T\|) = (0 \dots \|S\| - 1)$
139	128 138	eqtr4d	$⊢ (S \in Word A \land T \in Word A) \to (0 ..^\|S\|) = ((\|T\| + \|S\|) - 1 - (\|T\| + \|S\| - 1) \dots (\|T\| + \|S\|) - 1 - \|T\|)$
140	139	adantr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to (0 ..^\|S\|) = ((\|T\| + \|S\|) - 1 - (\|T\| + \|S\| - 1) \dots (\|T\| + \|S\|) - 1 - \|T\|)$
141	123 125 140	3eltr4d	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to \|S ++ T\| - 1 - x \in (0 ..^\|S\|)$
142		ccatval1	$⊢ (S \in Word A \land T \in Word A \land \|S ++ T\| - 1 - x \in (0 ..^\|S\|)) \to (S ++ T) (\|S ++ T\| - 1 - x) = S (\|S ++ T\| - 1 - x)$
143	112 113 141 142	syl3anc	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to (S ++ T) (\|S ++ T\| - 1 - x) = S (\|S ++ T\| - 1 - x)$
144		simpl	$⊢ (S \in Word A \land T \in Word A) \to S \in Word A$
145	102	ad2antlr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to x - \|reverse (T)\| = x - \|T\|$
146		id	$⊢ x \in (\|T\| ..^\|T\| + \|S\|) \to x \in (\|T\| ..^\|T\| + \|S\|)$
147		fzosubel3	$⊢ (x \in (\|T\| ..^\|T\| + \|S\|) \land \|S\| \in ℤ) \to x - \|T\| \in (0 ..^\|S\|)$
148	146 126 147	syl2anr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to x - \|T\| \in (0 ..^\|S\|)$
149	145 148	eqeltrd	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to x - \|reverse (T)\| \in (0 ..^\|S\|)$
150		revfv	$⊢ (S \in Word A \land x - \|reverse (T)\| \in (0 ..^\|S\|)) \to reverse (S) (x - \|reverse (T)\|) = S (\|S\| - 1 - (x - \|reverse (T)\|))$
151	144 149 150	syl2an2r	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to reverse (S) (x - \|reverse (T)\|) = S (\|S\| - 1 - (x - \|reverse (T)\|))$
152	111 143 151	3eqtr4d	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to (S ++ T) (\|S ++ T\| - 1 - x) = reverse (S) (x - \|reverse (T)\|)$
153		fzoss1	$⊢ \|T\| \in ℤ_{\geq 0} \to (\|T\| ..^\|T\| + \|S\|) \subseteq (0 ..^\|T\| + \|S\|)$
154		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
155	153 154	eleq2s	$⊢ \|T\| \in ℕ_{0} \to (\|T\| ..^\|T\| + \|S\|) \subseteq (0 ..^\|T\| + \|S\|)$
156	10 155	syl	$⊢ T \in Word A \to (\|T\| ..^\|T\| + \|S\|) \subseteq (0 ..^\|T\| + \|S\|)$
157	156	adantl	$⊢ (S \in Word A \land T \in Word A) \to (\|T\| ..^\|T\| + \|S\|) \subseteq (0 ..^\|T\| + \|S\|)$
158	51	oveq2d	$⊢ (S \in Word A \land T \in Word A) \to (0 ..^\|S ++ T\|) = (0 ..^\|T\| + \|S\|)$
159	157 158	sseqtrrd	$⊢ (S \in Word A \land T \in Word A) \to (\|T\| ..^\|T\| + \|S\|) \subseteq (0 ..^\|S ++ T\|)$
160	159	sselda	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to x \in (0 ..^\|S ++ T\|)$
161	1 160 81	syl2an2r	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to reverse (S ++ T) (x) = (S ++ T) (\|S ++ T\| - 1 - x)$
162	18	ad2antlr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to reverse (T) \in Word A$
163	19	ad2antrr	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to reverse (S) \in Word A$
164	85 28	oveq12d	$⊢ (S \in Word A \land T \in Word A) \to (\|reverse (T)\| ..^\|reverse (T)\| + \|reverse (S)\|) = (\|T\| ..^\|T\| + \|S\|)$
165	164	eleq2d	$⊢ (S \in Word A \land T \in Word A) \to (x \in (\|reverse (T)\| ..^\|reverse (T)\| + \|reverse (S)\|) \leftrightarrow x \in (\|T\| ..^\|T\| + \|S\|))$
166	165	biimpar	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to x \in (\|reverse (T)\| ..^\|reverse (T)\| + \|reverse (S)\|)$
167		ccatval2	$⊢ (reverse (T) \in Word A \land reverse (S) \in Word A \land x \in (\|reverse (T)\| ..^\|reverse (T)\| + \|reverse (S)\|)) \to (reverse (T) ++ reverse (S)) (x) = reverse (S) (x - \|reverse (T)\|)$
168	162 163 166 167	syl3anc	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to (reverse (T) ++ reverse (S)) (x) = reverse (S) (x - \|reverse (T)\|)$
169	152 161 168	3eqtr4d	$⊢ ((S \in Word A \land T \in Word A) \land x \in (\|T\| ..^\|T\| + \|S\|)) \to reverse (S ++ T) (x) = (reverse (T) ++ reverse (S)) (x)$
170	91 169	jaodan	$⊢ ((S \in Word A \land T \in Word A) \land (x \in (0 ..^\|T\|) \lor x \in (\|T\| ..^\|T\| + \|S\|))) \to reverse (S ++ T) (x) = (reverse (T) ++ reverse (S)) (x)$
171	37 170	syldan	$⊢ ((S \in Word A \land T \in Word A) \land x \in (0 ..^\|T\| + \|S\|)) \to reverse (S ++ T) (x) = (reverse (T) ++ reverse (S)) (x)$
172	17 32 171	eqfnfvd	$⊢ (S \in Word A \land T \in Word A) \to reverse (S ++ T) = reverse (T) ++ reverse (S)$

Metamath Proof Explorer

Theorem revccat

Proof