Step | Hyp | Ref
| Expression |
1 | | ccatcl 13212 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑆 ++ 𝑇) ∈ Word 𝐴) |
2 | | revcl 13361 |
. . . 4
⊢ ((𝑆 ++ 𝑇) ∈ Word 𝐴 → (reverse‘(𝑆 ++ 𝑇)) ∈ Word 𝐴) |
3 | | wrdf 13165 |
. . . 4
⊢
((reverse‘(𝑆
++ 𝑇)) ∈ Word 𝐴 → (reverse‘(𝑆 ++ 𝑇)):(0..^(#‘(reverse‘(𝑆 ++ 𝑇))))⟶𝐴) |
4 | | ffn 5958 |
. . . 4
⊢
((reverse‘(𝑆
++ 𝑇)):(0..^(#‘(reverse‘(𝑆 ++ 𝑇))))⟶𝐴 → (reverse‘(𝑆 ++ 𝑇)) Fn (0..^(#‘(reverse‘(𝑆 ++ 𝑇))))) |
5 | 1, 2, 3, 4 | 4syl 19 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) Fn (0..^(#‘(reverse‘(𝑆 ++ 𝑇))))) |
6 | | revlen 13362 |
. . . . . . 7
⊢ ((𝑆 ++ 𝑇) ∈ Word 𝐴 → (#‘(reverse‘(𝑆 ++ 𝑇))) = (#‘(𝑆 ++ 𝑇))) |
7 | 1, 6 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘(reverse‘(𝑆 ++ 𝑇))) = (#‘(𝑆 ++ 𝑇))) |
8 | | ccatlen 13213 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘(𝑆 ++ 𝑇)) = ((#‘𝑆) + (#‘𝑇))) |
9 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝑆 ∈ Word 𝐴 → (#‘𝑆) ∈
ℕ0) |
10 | 9 | nn0cnd 11230 |
. . . . . . . 8
⊢ (𝑆 ∈ Word 𝐴 → (#‘𝑆) ∈ ℂ) |
11 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝑇 ∈ Word 𝐴 → (#‘𝑇) ∈
ℕ0) |
12 | 11 | nn0cnd 11230 |
. . . . . . . 8
⊢ (𝑇 ∈ Word 𝐴 → (#‘𝑇) ∈ ℂ) |
13 | | addcom 10101 |
. . . . . . . 8
⊢
(((#‘𝑆) ∈
ℂ ∧ (#‘𝑇)
∈ ℂ) → ((#‘𝑆) + (#‘𝑇)) = ((#‘𝑇) + (#‘𝑆))) |
14 | 10, 12, 13 | syl2an 493 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘𝑆) + (#‘𝑇)) = ((#‘𝑇) + (#‘𝑆))) |
15 | 8, 14 | eqtrd 2644 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘(𝑆 ++ 𝑇)) = ((#‘𝑇) + (#‘𝑆))) |
16 | 7, 15 | eqtrd 2644 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘(reverse‘(𝑆 ++ 𝑇))) = ((#‘𝑇) + (#‘𝑆))) |
17 | 16 | oveq2d 6565 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(#‘(reverse‘(𝑆 ++ 𝑇)))) = (0..^((#‘𝑇) + (#‘𝑆)))) |
18 | 17 | fneq2d 5896 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((reverse‘(𝑆 ++ 𝑇)) Fn (0..^(#‘(reverse‘(𝑆 ++ 𝑇)))) ↔ (reverse‘(𝑆 ++ 𝑇)) Fn (0..^((#‘𝑇) + (#‘𝑆))))) |
19 | 5, 18 | mpbid 221 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) Fn (0..^((#‘𝑇) + (#‘𝑆)))) |
20 | | revcl 13361 |
. . . . 5
⊢ (𝑇 ∈ Word 𝐴 → (reverse‘𝑇) ∈ Word 𝐴) |
21 | | revcl 13361 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (reverse‘𝑆) ∈ Word 𝐴) |
22 | | ccatcl 13212 |
. . . . 5
⊢
(((reverse‘𝑇)
∈ Word 𝐴 ∧
(reverse‘𝑆) ∈
Word 𝐴) →
((reverse‘𝑇) ++
(reverse‘𝑆)) ∈
Word 𝐴) |
23 | 20, 21, 22 | syl2anr 494 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((reverse‘𝑇) ++ (reverse‘𝑆)) ∈ Word 𝐴) |
24 | | wrdf 13165 |
. . . 4
⊢
(((reverse‘𝑇)
++ (reverse‘𝑆))
∈ Word 𝐴 →
((reverse‘𝑇) ++
(reverse‘𝑆)):(0..^(#‘((reverse‘𝑇) ++ (reverse‘𝑆))))⟶𝐴) |
25 | | ffn 5958 |
. . . 4
⊢
(((reverse‘𝑇)
++ (reverse‘𝑆)):(0..^(#‘((reverse‘𝑇) ++ (reverse‘𝑆))))⟶𝐴 → ((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^(#‘((reverse‘𝑇) ++ (reverse‘𝑆))))) |
26 | 23, 24, 25 | 3syl 18 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^(#‘((reverse‘𝑇) ++ (reverse‘𝑆))))) |
27 | | ccatlen 13213 |
. . . . . . 7
⊢
(((reverse‘𝑇)
∈ Word 𝐴 ∧
(reverse‘𝑆) ∈
Word 𝐴) →
(#‘((reverse‘𝑇)
++ (reverse‘𝑆))) =
((#‘(reverse‘𝑇)) + (#‘(reverse‘𝑆)))) |
28 | 20, 21, 27 | syl2anr 494 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘((reverse‘𝑇) ++ (reverse‘𝑆))) =
((#‘(reverse‘𝑇)) + (#‘(reverse‘𝑆)))) |
29 | | revlen 13362 |
. . . . . . 7
⊢ (𝑇 ∈ Word 𝐴 → (#‘(reverse‘𝑇)) = (#‘𝑇)) |
30 | | revlen 13362 |
. . . . . . 7
⊢ (𝑆 ∈ Word 𝐴 → (#‘(reverse‘𝑆)) = (#‘𝑆)) |
31 | 29, 30 | oveqan12rd 6569 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘(reverse‘𝑇)) +
(#‘(reverse‘𝑆))) = ((#‘𝑇) + (#‘𝑆))) |
32 | 28, 31 | eqtrd 2644 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘((reverse‘𝑇) ++ (reverse‘𝑆))) = ((#‘𝑇) + (#‘𝑆))) |
33 | 32 | oveq2d 6565 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(#‘((reverse‘𝑇) ++ (reverse‘𝑆)))) = (0..^((#‘𝑇) + (#‘𝑆)))) |
34 | 33 | fneq2d 5896 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^(#‘((reverse‘𝑇) ++ (reverse‘𝑆)))) ↔
((reverse‘𝑇) ++
(reverse‘𝑆)) Fn
(0..^((#‘𝑇) +
(#‘𝑆))))) |
35 | 26, 34 | mpbid 221 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^((#‘𝑇) + (#‘𝑆)))) |
36 | | id 22 |
. . . 4
⊢ (𝑥 ∈ (0..^((#‘𝑇) + (#‘𝑆))) → 𝑥 ∈ (0..^((#‘𝑇) + (#‘𝑆)))) |
37 | 11 | nn0zd 11356 |
. . . . 5
⊢ (𝑇 ∈ Word 𝐴 → (#‘𝑇) ∈ ℤ) |
38 | 37 | adantl 481 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘𝑇) ∈ ℤ) |
39 | | fzospliti 12369 |
. . . 4
⊢ ((𝑥 ∈ (0..^((#‘𝑇) + (#‘𝑆))) ∧ (#‘𝑇) ∈ ℤ) → (𝑥 ∈ (0..^(#‘𝑇)) ∨ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))))) |
40 | 36, 38, 39 | syl2anr 494 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^((#‘𝑇) + (#‘𝑆)))) → (𝑥 ∈ (0..^(#‘𝑇)) ∨ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))))) |
41 | | simpll 786 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → 𝑆 ∈ Word 𝐴) |
42 | | simplr 788 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → 𝑇 ∈ Word 𝐴) |
43 | | fzoval 12340 |
. . . . . . . . . . . 12
⊢
((#‘𝑇) ∈
ℤ → (0..^(#‘𝑇)) = (0...((#‘𝑇) − 1))) |
44 | 38, 43 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(#‘𝑇)) = (0...((#‘𝑇) − 1))) |
45 | 44 | eleq2d 2673 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 ∈ (0..^(#‘𝑇)) ↔ 𝑥 ∈ (0...((#‘𝑇) − 1)))) |
46 | 45 | biimpa 500 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → 𝑥 ∈ (0...((#‘𝑇) − 1))) |
47 | | fznn0sub2 12315 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0...((#‘𝑇) − 1)) →
(((#‘𝑇) − 1)
− 𝑥) ∈
(0...((#‘𝑇) −
1))) |
48 | 46, 47 | syl 17 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (((#‘𝑇) − 1) − 𝑥) ∈ (0...((#‘𝑇) − 1))) |
49 | 44 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (0..^(#‘𝑇)) = (0...((#‘𝑇) − 1))) |
50 | 48, 49 | eleqtrrd 2691 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (((#‘𝑇) − 1) − 𝑥) ∈ (0..^(#‘𝑇))) |
51 | | ccatval3 13216 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ (((#‘𝑇) − 1) − 𝑥) ∈ (0..^(#‘𝑇))) → ((𝑆 ++ 𝑇)‘((((#‘𝑇) − 1) − 𝑥) + (#‘𝑆))) = (𝑇‘(((#‘𝑇) − 1) − 𝑥))) |
52 | 41, 42, 50, 51 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((𝑆 ++ 𝑇)‘((((#‘𝑇) − 1) − 𝑥) + (#‘𝑆))) = (𝑇‘(((#‘𝑇) − 1) − 𝑥))) |
53 | 15 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘(𝑆 ++ 𝑇)) − 1) = (((#‘𝑇) + (#‘𝑆)) − 1)) |
54 | 12 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘𝑇) ∈ ℂ) |
55 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘𝑆) ∈ ℂ) |
56 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → 1 ∈ ℂ) |
57 | 54, 55, 56 | addsubd 10292 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((#‘𝑇) + (#‘𝑆)) − 1) = (((#‘𝑇) − 1) + (#‘𝑆))) |
58 | 53, 57 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘(𝑆 ++ 𝑇)) − 1) = (((#‘𝑇) − 1) + (#‘𝑆))) |
59 | 58 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((#‘𝑇) − 1) + (#‘𝑆)) − 𝑥)) |
60 | 59 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((#‘𝑇) − 1) + (#‘𝑆)) − 𝑥)) |
61 | | peano2zm 11297 |
. . . . . . . . . . . 12
⊢
((#‘𝑇) ∈
ℤ → ((#‘𝑇)
− 1) ∈ ℤ) |
62 | 37, 61 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ Word 𝐴 → ((#‘𝑇) − 1) ∈
ℤ) |
63 | 62 | zcnd 11359 |
. . . . . . . . . 10
⊢ (𝑇 ∈ Word 𝐴 → ((#‘𝑇) − 1) ∈
ℂ) |
64 | 63 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((#‘𝑇) − 1) ∈
ℂ) |
65 | 10 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (#‘𝑆) ∈ ℂ) |
66 | | elfzoelz 12339 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0..^(#‘𝑇)) → 𝑥 ∈ ℤ) |
67 | 66 | zcnd 11359 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0..^(#‘𝑇)) → 𝑥 ∈ ℂ) |
68 | 67 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → 𝑥 ∈ ℂ) |
69 | 64, 65, 68 | addsubd 10292 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((((#‘𝑇) − 1) + (#‘𝑆)) − 𝑥) = ((((#‘𝑇) − 1) − 𝑥) + (#‘𝑆))) |
70 | 60, 69 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((#‘𝑇) − 1) − 𝑥) + (#‘𝑆))) |
71 | 70 | fveq2d 6107 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((𝑆 ++ 𝑇)‘(((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = ((𝑆 ++ 𝑇)‘((((#‘𝑇) − 1) − 𝑥) + (#‘𝑆)))) |
72 | | revfv 13363 |
. . . . . . 7
⊢ ((𝑇 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((reverse‘𝑇)‘𝑥) = (𝑇‘(((#‘𝑇) − 1) − 𝑥))) |
73 | 72 | adantll 746 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((reverse‘𝑇)‘𝑥) = (𝑇‘(((#‘𝑇) − 1) − 𝑥))) |
74 | 52, 71, 73 | 3eqtr4d 2654 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((𝑆 ++ 𝑇)‘(((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = ((reverse‘𝑇)‘𝑥)) |
75 | 1 | adantr 480 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (𝑆 ++ 𝑇) ∈ Word 𝐴) |
76 | | uzid 11578 |
. . . . . . . . . . 11
⊢
((#‘𝑇) ∈
ℤ → (#‘𝑇)
∈ (ℤ≥‘(#‘𝑇))) |
77 | 38, 76 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘𝑇) ∈
(ℤ≥‘(#‘𝑇))) |
78 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘𝑆) ∈
ℕ0) |
79 | | uzaddcl 11620 |
. . . . . . . . . 10
⊢
(((#‘𝑇) ∈
(ℤ≥‘(#‘𝑇)) ∧ (#‘𝑆) ∈ ℕ0) →
((#‘𝑇) +
(#‘𝑆)) ∈
(ℤ≥‘(#‘𝑇))) |
80 | 77, 78, 79 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘𝑇) + (#‘𝑆)) ∈
(ℤ≥‘(#‘𝑇))) |
81 | 15, 80 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘(𝑆 ++ 𝑇)) ∈
(ℤ≥‘(#‘𝑇))) |
82 | | fzoss2 12365 |
. . . . . . . 8
⊢
((#‘(𝑆 ++
𝑇)) ∈
(ℤ≥‘(#‘𝑇)) → (0..^(#‘𝑇)) ⊆ (0..^(#‘(𝑆 ++ 𝑇)))) |
83 | 81, 82 | syl 17 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(#‘𝑇)) ⊆ (0..^(#‘(𝑆 ++ 𝑇)))) |
84 | 83 | sselda 3568 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → 𝑥 ∈ (0..^(#‘(𝑆 ++ 𝑇)))) |
85 | | revfv 13363 |
. . . . . 6
⊢ (((𝑆 ++ 𝑇) ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘(𝑆 ++ 𝑇)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = ((𝑆 ++ 𝑇)‘(((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
86 | 75, 84, 85 | syl2anc 691 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = ((𝑆 ++ 𝑇)‘(((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
87 | 20 | ad2antlr 759 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (reverse‘𝑇) ∈ Word 𝐴) |
88 | 21 | ad2antrr 758 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (reverse‘𝑆) ∈ Word 𝐴) |
89 | 29 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘(reverse‘𝑇)) = (#‘𝑇)) |
90 | 89 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(#‘(reverse‘𝑇))) = (0..^(#‘𝑇))) |
91 | 90 | eleq2d 2673 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 ∈ (0..^(#‘(reverse‘𝑇))) ↔ 𝑥 ∈ (0..^(#‘𝑇)))) |
92 | 91 | biimpar 501 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → 𝑥 ∈ (0..^(#‘(reverse‘𝑇)))) |
93 | | ccatval1 13214 |
. . . . . 6
⊢
(((reverse‘𝑇)
∈ Word 𝐴 ∧
(reverse‘𝑆) ∈
Word 𝐴 ∧ 𝑥 ∈
(0..^(#‘(reverse‘𝑇)))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑇)‘𝑥)) |
94 | 87, 88, 92, 93 | syl3anc 1318 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑇)‘𝑥)) |
95 | 74, 86, 94 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥)) |
96 | 8 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘(𝑆 ++ 𝑇)) − 1) = (((#‘𝑆) + (#‘𝑇)) − 1)) |
97 | 55, 54, 56 | addsubd 10292 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((#‘𝑆) + (#‘𝑇)) − 1) = (((#‘𝑆) − 1) + (#‘𝑇))) |
98 | 96, 97 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘(𝑆 ++ 𝑇)) − 1) = (((#‘𝑆) − 1) + (#‘𝑇))) |
99 | 98 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((#‘𝑆) − 1) + (#‘𝑇)) − 𝑥)) |
100 | 99 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((#‘𝑆) − 1) + (#‘𝑇)) − 𝑥)) |
101 | 9 | nn0zd 11356 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Word 𝐴 → (#‘𝑆) ∈ ℤ) |
102 | | peano2zm 11297 |
. . . . . . . . . . . . 13
⊢
((#‘𝑆) ∈
ℤ → ((#‘𝑆)
− 1) ∈ ℤ) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐴 → ((#‘𝑆) − 1) ∈
ℤ) |
104 | 103 | zcnd 11359 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝐴 → ((#‘𝑆) − 1) ∈
ℂ) |
105 | 104 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → ((#‘𝑆) − 1) ∈
ℂ) |
106 | | elfzoelz 12339 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))) → 𝑥 ∈ ℤ) |
107 | 106 | zcnd 11359 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))) → 𝑥 ∈ ℂ) |
108 | 107 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → 𝑥 ∈ ℂ) |
109 | 12 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (#‘𝑇) ∈ ℂ) |
110 | 105, 108,
109 | subsub3d 10301 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (((#‘𝑆) − 1) − (𝑥 − (#‘𝑇))) = ((((#‘𝑆) − 1) + (#‘𝑇)) − 𝑥)) |
111 | 100, 110 | eqtr4d 2647 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = (((#‘𝑆) − 1) − (𝑥 − (#‘𝑇)))) |
112 | 89 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 − (#‘(reverse‘𝑇))) = (𝑥 − (#‘𝑇))) |
113 | 112 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((#‘𝑆) − 1) − (𝑥 − (#‘(reverse‘𝑇)))) = (((#‘𝑆) − 1) − (𝑥 − (#‘𝑇)))) |
114 | 113 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (((#‘𝑆) − 1) − (𝑥 − (#‘(reverse‘𝑇)))) = (((#‘𝑆) − 1) − (𝑥 − (#‘𝑇)))) |
115 | 111, 114 | eqtr4d 2647 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = (((#‘𝑆) − 1) − (𝑥 − (#‘(reverse‘𝑇))))) |
116 | 115 | fveq2d 6107 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (𝑆‘(((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = (𝑆‘(((#‘𝑆) − 1) − (𝑥 − (#‘(reverse‘𝑇)))))) |
117 | | simpll 786 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → 𝑆 ∈ Word 𝐴) |
118 | | simplr 788 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → 𝑇 ∈ Word 𝐴) |
119 | | zaddcl 11294 |
. . . . . . . . . . . 12
⊢
(((#‘𝑇) ∈
ℤ ∧ (#‘𝑆)
∈ ℤ) → ((#‘𝑇) + (#‘𝑆)) ∈ ℤ) |
120 | 37, 101, 119 | syl2anr 494 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘𝑇) + (#‘𝑆)) ∈ ℤ) |
121 | | peano2zm 11297 |
. . . . . . . . . . 11
⊢
(((#‘𝑇) +
(#‘𝑆)) ∈ ℤ
→ (((#‘𝑇) +
(#‘𝑆)) − 1)
∈ ℤ) |
122 | 120, 121 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((#‘𝑇) + (#‘𝑆)) − 1) ∈
ℤ) |
123 | 122 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (((#‘𝑇) + (#‘𝑆)) − 1) ∈
ℤ) |
124 | | fzoval 12340 |
. . . . . . . . . . . 12
⊢
(((#‘𝑇) +
(#‘𝑆)) ∈ ℤ
→ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))) = ((#‘𝑇)...(((#‘𝑇) + (#‘𝑆)) − 1))) |
125 | 120, 124 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))) = ((#‘𝑇)...(((#‘𝑇) + (#‘𝑆)) − 1))) |
126 | 125 | eleq2d 2673 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))) ↔ 𝑥 ∈ ((#‘𝑇)...(((#‘𝑇) + (#‘𝑆)) − 1)))) |
127 | 126 | biimpa 500 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → 𝑥 ∈ ((#‘𝑇)...(((#‘𝑇) + (#‘𝑆)) − 1))) |
128 | | fzrev2i 12275 |
. . . . . . . . 9
⊢
(((((#‘𝑇) +
(#‘𝑆)) − 1)
∈ ℤ ∧ 𝑥
∈ ((#‘𝑇)...(((#‘𝑇) + (#‘𝑆)) − 1))) → ((((#‘𝑇) + (#‘𝑆)) − 1) − 𝑥) ∈ (((((#‘𝑇) + (#‘𝑆)) − 1) − (((#‘𝑇) + (#‘𝑆)) − 1))...((((#‘𝑇) + (#‘𝑆)) − 1) − (#‘𝑇)))) |
129 | 123, 127,
128 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → ((((#‘𝑇) + (#‘𝑆)) − 1) − 𝑥) ∈ (((((#‘𝑇) + (#‘𝑆)) − 1) − (((#‘𝑇) + (#‘𝑆)) − 1))...((((#‘𝑇) + (#‘𝑆)) − 1) − (#‘𝑇)))) |
130 | 53 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((#‘𝑇) + (#‘𝑆)) − 1) − 𝑥)) |
131 | 130 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((#‘𝑇) + (#‘𝑆)) − 1) − 𝑥)) |
132 | 101 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘𝑆) ∈ ℤ) |
133 | | fzoval 12340 |
. . . . . . . . . . 11
⊢
((#‘𝑆) ∈
ℤ → (0..^(#‘𝑆)) = (0...((#‘𝑆) − 1))) |
134 | 132, 133 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(#‘𝑆)) = (0...((#‘𝑆) − 1))) |
135 | 122 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((#‘𝑇) + (#‘𝑆)) − 1) ∈
ℂ) |
136 | 135 | subidd 10259 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((((#‘𝑇) + (#‘𝑆)) − 1) − (((#‘𝑇) + (#‘𝑆)) − 1)) = 0) |
137 | | addcl 9897 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑇) ∈
ℂ ∧ (#‘𝑆)
∈ ℂ) → ((#‘𝑇) + (#‘𝑆)) ∈ ℂ) |
138 | 12, 10, 137 | syl2anr 494 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘𝑇) + (#‘𝑆)) ∈ ℂ) |
139 | 138, 56, 54 | sub32d 10303 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((((#‘𝑇) + (#‘𝑆)) − 1) − (#‘𝑇)) = ((((#‘𝑇) + (#‘𝑆)) − (#‘𝑇)) − 1)) |
140 | | pncan2 10167 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑇) ∈
ℂ ∧ (#‘𝑆)
∈ ℂ) → (((#‘𝑇) + (#‘𝑆)) − (#‘𝑇)) = (#‘𝑆)) |
141 | 12, 10, 140 | syl2anr 494 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((#‘𝑇) + (#‘𝑆)) − (#‘𝑇)) = (#‘𝑆)) |
142 | 141 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((((#‘𝑇) + (#‘𝑆)) − (#‘𝑇)) − 1) = ((#‘𝑆) − 1)) |
143 | 139, 142 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((((#‘𝑇) + (#‘𝑆)) − 1) − (#‘𝑇)) = ((#‘𝑆) − 1)) |
144 | 136, 143 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((((#‘𝑇) + (#‘𝑆)) − 1) − (((#‘𝑇) + (#‘𝑆)) − 1))...((((#‘𝑇) + (#‘𝑆)) − 1) − (#‘𝑇))) = (0...((#‘𝑆) − 1))) |
145 | 134, 144 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(#‘𝑆)) = (((((#‘𝑇) + (#‘𝑆)) − 1) − (((#‘𝑇) + (#‘𝑆)) − 1))...((((#‘𝑇) + (#‘𝑆)) − 1) − (#‘𝑇)))) |
146 | 145 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (0..^(#‘𝑆)) = (((((#‘𝑇) + (#‘𝑆)) − 1) − (((#‘𝑇) + (#‘𝑆)) − 1))...((((#‘𝑇) + (#‘𝑆)) − 1) − (#‘𝑇)))) |
147 | 129, 131,
146 | 3eltr4d 2703 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥) ∈ (0..^(#‘𝑆))) |
148 | | ccatval1 13214 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ (((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥) ∈ (0..^(#‘𝑆))) → ((𝑆 ++ 𝑇)‘(((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = (𝑆‘(((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
149 | 117, 118,
147, 148 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → ((𝑆 ++ 𝑇)‘(((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = (𝑆‘(((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
150 | 29 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (#‘(reverse‘𝑇)) = (#‘𝑇)) |
151 | 150 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (𝑥 − (#‘(reverse‘𝑇))) = (𝑥 − (#‘𝑇))) |
152 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))) → 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) |
153 | | fzosubel3 12396 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))) ∧ (#‘𝑆) ∈ ℤ) → (𝑥 − (#‘𝑇)) ∈ (0..^(#‘𝑆))) |
154 | 152, 132,
153 | syl2anr 494 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (𝑥 − (#‘𝑇)) ∈ (0..^(#‘𝑆))) |
155 | 151, 154 | eqeltrd 2688 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (𝑥 − (#‘(reverse‘𝑇))) ∈ (0..^(#‘𝑆))) |
156 | | revfv 13363 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑥 − (#‘(reverse‘𝑇))) ∈ (0..^(#‘𝑆))) → ((reverse‘𝑆)‘(𝑥 − (#‘(reverse‘𝑇)))) = (𝑆‘(((#‘𝑆) − 1) − (𝑥 − (#‘(reverse‘𝑇)))))) |
157 | 117, 155,
156 | syl2anc 691 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → ((reverse‘𝑆)‘(𝑥 − (#‘(reverse‘𝑇)))) = (𝑆‘(((#‘𝑆) − 1) − (𝑥 − (#‘(reverse‘𝑇)))))) |
158 | 116, 149,
157 | 3eqtr4d 2654 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → ((𝑆 ++ 𝑇)‘(((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = ((reverse‘𝑆)‘(𝑥 − (#‘(reverse‘𝑇))))) |
159 | 1 | adantr 480 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (𝑆 ++ 𝑇) ∈ Word 𝐴) |
160 | 11 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (#‘𝑇) ∈
ℕ0) |
161 | | fzoss1 12364 |
. . . . . . . . . 10
⊢
((#‘𝑇) ∈
(ℤ≥‘0) → ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))) ⊆ (0..^((#‘𝑇) + (#‘𝑆)))) |
162 | | nn0uz 11598 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
163 | 161, 162 | eleq2s 2706 |
. . . . . . . . 9
⊢
((#‘𝑇) ∈
ℕ0 → ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))) ⊆ (0..^((#‘𝑇) + (#‘𝑆)))) |
164 | 160, 163 | syl 17 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))) ⊆ (0..^((#‘𝑇) + (#‘𝑆)))) |
165 | 15 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(#‘(𝑆 ++ 𝑇))) = (0..^((#‘𝑇) + (#‘𝑆)))) |
166 | 164, 165 | sseqtr4d 3605 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))) ⊆ (0..^(#‘(𝑆 ++ 𝑇)))) |
167 | 166 | sselda 3568 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → 𝑥 ∈ (0..^(#‘(𝑆 ++ 𝑇)))) |
168 | 159, 167,
85 | syl2anc 691 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = ((𝑆 ++ 𝑇)‘(((#‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
169 | 20 | ad2antlr 759 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (reverse‘𝑇) ∈ Word 𝐴) |
170 | 21 | ad2antrr 758 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (reverse‘𝑆) ∈ Word 𝐴) |
171 | 89, 31 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((#‘(reverse‘𝑇))..^((#‘(reverse‘𝑇)) +
(#‘(reverse‘𝑆)))) = ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) |
172 | 171 | eleq2d 2673 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 ∈ ((#‘(reverse‘𝑇))..^((#‘(reverse‘𝑇)) +
(#‘(reverse‘𝑆)))) ↔ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))))) |
173 | 172 | biimpar 501 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → 𝑥 ∈ ((#‘(reverse‘𝑇))..^((#‘(reverse‘𝑇)) +
(#‘(reverse‘𝑆))))) |
174 | | ccatval2 13215 |
. . . . . 6
⊢
(((reverse‘𝑇)
∈ Word 𝐴 ∧
(reverse‘𝑆) ∈
Word 𝐴 ∧ 𝑥 ∈
((#‘(reverse‘𝑇))..^((#‘(reverse‘𝑇)) +
(#‘(reverse‘𝑆))))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑆)‘(𝑥 − (#‘(reverse‘𝑇))))) |
175 | 169, 170,
173, 174 | syl3anc 1318 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑆)‘(𝑥 − (#‘(reverse‘𝑇))))) |
176 | 158, 168,
175 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥)) |
177 | 95, 176 | jaodan 822 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ (𝑥 ∈ (0..^(#‘𝑇)) ∨ 𝑥 ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑆))))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥)) |
178 | 40, 177 | syldan 486 |
. 2
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^((#‘𝑇) + (#‘𝑆)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥)) |
179 | 19, 35, 178 | eqfnfvd 6222 |
1
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) = ((reverse‘𝑇) ++ (reverse‘𝑆))) |