Step | Hyp | Ref
| Expression |
1 | | ccatcl 14134 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑆 ++ 𝑇) ∈ Word 𝐴) |
2 | | revcl 14331 |
. . . 4
⊢ ((𝑆 ++ 𝑇) ∈ Word 𝐴 → (reverse‘(𝑆 ++ 𝑇)) ∈ Word 𝐴) |
3 | | wrdfn 14088 |
. . . 4
⊢
((reverse‘(𝑆
++ 𝑇)) ∈ Word 𝐴 → (reverse‘(𝑆 ++ 𝑇)) Fn
(0..^(♯‘(reverse‘(𝑆 ++ 𝑇))))) |
4 | 1, 2, 3 | 3syl 18 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) Fn
(0..^(♯‘(reverse‘(𝑆 ++ 𝑇))))) |
5 | | revlen 14332 |
. . . . . . 7
⊢ ((𝑆 ++ 𝑇) ∈ Word 𝐴 → (♯‘(reverse‘(𝑆 ++ 𝑇))) = (♯‘(𝑆 ++ 𝑇))) |
6 | 1, 5 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(♯‘(reverse‘(𝑆 ++ 𝑇))) = (♯‘(𝑆 ++ 𝑇))) |
7 | | ccatlen 14135 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇))) |
8 | | lencl 14093 |
. . . . . . . 8
⊢ (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈
ℕ0) |
9 | 8 | nn0cnd 12157 |
. . . . . . 7
⊢ (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈ ℂ) |
10 | | lencl 14093 |
. . . . . . . 8
⊢ (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈
ℕ0) |
11 | 10 | nn0cnd 12157 |
. . . . . . 7
⊢ (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈ ℂ) |
12 | | addcom 11023 |
. . . . . . 7
⊢
(((♯‘𝑆)
∈ ℂ ∧ (♯‘𝑇) ∈ ℂ) →
((♯‘𝑆) +
(♯‘𝑇)) =
((♯‘𝑇) +
(♯‘𝑆))) |
13 | 9, 11, 12 | syl2an 599 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑆) + (♯‘𝑇)) = ((♯‘𝑇) + (♯‘𝑆))) |
14 | 6, 7, 13 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(♯‘(reverse‘(𝑆 ++ 𝑇))) = ((♯‘𝑇) + (♯‘𝑆))) |
15 | 14 | oveq2d 7234 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(0..^(♯‘(reverse‘(𝑆 ++ 𝑇)))) = (0..^((♯‘𝑇) + (♯‘𝑆)))) |
16 | 15 | fneq2d 6478 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((reverse‘(𝑆 ++ 𝑇)) Fn
(0..^(♯‘(reverse‘(𝑆 ++ 𝑇)))) ↔ (reverse‘(𝑆 ++ 𝑇)) Fn (0..^((♯‘𝑇) + (♯‘𝑆))))) |
17 | 4, 16 | mpbid 235 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) Fn (0..^((♯‘𝑇) + (♯‘𝑆)))) |
18 | | revcl 14331 |
. . . . 5
⊢ (𝑇 ∈ Word 𝐴 → (reverse‘𝑇) ∈ Word 𝐴) |
19 | | revcl 14331 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (reverse‘𝑆) ∈ Word 𝐴) |
20 | | ccatcl 14134 |
. . . . 5
⊢
(((reverse‘𝑇)
∈ Word 𝐴 ∧
(reverse‘𝑆) ∈
Word 𝐴) →
((reverse‘𝑇) ++
(reverse‘𝑆)) ∈
Word 𝐴) |
21 | 18, 19, 20 | syl2anr 600 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((reverse‘𝑇) ++ (reverse‘𝑆)) ∈ Word 𝐴) |
22 | | wrdfn 14088 |
. . . 4
⊢
(((reverse‘𝑇)
++ (reverse‘𝑆))
∈ Word 𝐴 →
((reverse‘𝑇) ++
(reverse‘𝑆)) Fn
(0..^(♯‘((reverse‘𝑇) ++ (reverse‘𝑆))))) |
23 | 21, 22 | syl 17 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((reverse‘𝑇) ++ (reverse‘𝑆)) Fn
(0..^(♯‘((reverse‘𝑇) ++ (reverse‘𝑆))))) |
24 | | ccatlen 14135 |
. . . . . . 7
⊢
(((reverse‘𝑇)
∈ Word 𝐴 ∧
(reverse‘𝑆) ∈
Word 𝐴) →
(♯‘((reverse‘𝑇) ++ (reverse‘𝑆))) = ((♯‘(reverse‘𝑇)) +
(♯‘(reverse‘𝑆)))) |
25 | 18, 19, 24 | syl2anr 600 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(♯‘((reverse‘𝑇) ++ (reverse‘𝑆))) = ((♯‘(reverse‘𝑇)) +
(♯‘(reverse‘𝑆)))) |
26 | | revlen 14332 |
. . . . . . 7
⊢ (𝑇 ∈ Word 𝐴 → (♯‘(reverse‘𝑇)) = (♯‘𝑇)) |
27 | | revlen 14332 |
. . . . . . 7
⊢ (𝑆 ∈ Word 𝐴 → (♯‘(reverse‘𝑆)) = (♯‘𝑆)) |
28 | 26, 27 | oveqan12rd 7238 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
((♯‘(reverse‘𝑇)) + (♯‘(reverse‘𝑆))) = ((♯‘𝑇) + (♯‘𝑆))) |
29 | 25, 28 | eqtrd 2777 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(♯‘((reverse‘𝑇) ++ (reverse‘𝑆))) = ((♯‘𝑇) + (♯‘𝑆))) |
30 | 29 | oveq2d 7234 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(0..^(♯‘((reverse‘𝑇) ++ (reverse‘𝑆)))) = (0..^((♯‘𝑇) + (♯‘𝑆)))) |
31 | 30 | fneq2d 6478 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((reverse‘𝑇) ++ (reverse‘𝑆)) Fn
(0..^(♯‘((reverse‘𝑇) ++ (reverse‘𝑆)))) ↔ ((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^((♯‘𝑇) + (♯‘𝑆))))) |
32 | 23, 31 | mpbid 235 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^((♯‘𝑇) + (♯‘𝑆)))) |
33 | | id 22 |
. . . 4
⊢ (𝑥 ∈
(0..^((♯‘𝑇) +
(♯‘𝑆))) →
𝑥 ∈
(0..^((♯‘𝑇) +
(♯‘𝑆)))) |
34 | 10 | nn0zd 12285 |
. . . . 5
⊢ (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈ ℤ) |
35 | 34 | adantl 485 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘𝑇) ∈ ℤ) |
36 | | fzospliti 13279 |
. . . 4
⊢ ((𝑥 ∈
(0..^((♯‘𝑇) +
(♯‘𝑆))) ∧
(♯‘𝑇) ∈
ℤ) → (𝑥 ∈
(0..^(♯‘𝑇))
∨ 𝑥 ∈
((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))))) |
37 | 33, 35, 36 | syl2anr 600 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑥 ∈ (0..^(♯‘𝑇)) ∨ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))))) |
38 | | simpll 767 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑆 ∈ Word 𝐴) |
39 | | simplr 769 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑇 ∈ Word 𝐴) |
40 | | fzoval 13249 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑇)
∈ ℤ → (0..^(♯‘𝑇)) = (0...((♯‘𝑇) − 1))) |
41 | 34, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ Word 𝐴 → (0..^(♯‘𝑇)) = (0...((♯‘𝑇) − 1))) |
42 | 41 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(♯‘𝑇)) = (0...((♯‘𝑇) − 1))) |
43 | 42 | eleq2d 2823 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑥 ∈ (0...((♯‘𝑇) − 1)))) |
44 | 43 | biimpa 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0...((♯‘𝑇) − 1))) |
45 | | fznn0sub2 13224 |
. . . . . . . . 9
⊢ (𝑥 ∈
(0...((♯‘𝑇)
− 1)) → (((♯‘𝑇) − 1) − 𝑥) ∈ (0...((♯‘𝑇) − 1))) |
46 | 44, 45 | syl 17 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((♯‘𝑇) − 1) − 𝑥) ∈
(0...((♯‘𝑇)
− 1))) |
47 | 41 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (0..^(♯‘𝑇)) = (0...((♯‘𝑇) − 1))) |
48 | 46, 47 | eleqtrrd 2841 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((♯‘𝑇) − 1) − 𝑥) ∈
(0..^(♯‘𝑇))) |
49 | | ccatval3 14141 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ (((♯‘𝑇) − 1) − 𝑥) ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆))) = (𝑇‘(((♯‘𝑇) − 1) − 𝑥))) |
50 | 38, 39, 48, 49 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆))) = (𝑇‘(((♯‘𝑇) − 1) − 𝑥))) |
51 | 7, 13 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑇) + (♯‘𝑆))) |
52 | 51 | oveq1d 7233 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘(𝑆 ++ 𝑇)) − 1) = (((♯‘𝑇) + (♯‘𝑆)) − 1)) |
53 | 11 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘𝑇) ∈ ℂ) |
54 | 9 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘𝑆) ∈ ℂ) |
55 | | 1cnd 10833 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → 1 ∈ ℂ) |
56 | 53, 54, 55 | addsubd 11215 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘𝑇) + (♯‘𝑆)) − 1) = (((♯‘𝑇) − 1) +
(♯‘𝑆))) |
57 | 52, 56 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘(𝑆 ++ 𝑇)) − 1) = (((♯‘𝑇) − 1) +
(♯‘𝑆))) |
58 | 57 | oveq1d 7233 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) − 1) + (♯‘𝑆)) − 𝑥)) |
59 | 58 | adantr 484 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) − 1) + (♯‘𝑆)) − 𝑥)) |
60 | | peano2zm 12225 |
. . . . . . . . . . . 12
⊢
((♯‘𝑇)
∈ ℤ → ((♯‘𝑇) − 1) ∈
ℤ) |
61 | 34, 60 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ Word 𝐴 → ((♯‘𝑇) − 1) ∈
ℤ) |
62 | 61 | zcnd 12288 |
. . . . . . . . . 10
⊢ (𝑇 ∈ Word 𝐴 → ((♯‘𝑇) − 1) ∈
ℂ) |
63 | 62 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((♯‘𝑇) − 1) ∈
ℂ) |
64 | 9 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (♯‘𝑆) ∈ ℂ) |
65 | | elfzoelz 13248 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 ∈
ℤ) |
66 | 65 | zcnd 12288 |
. . . . . . . . . 10
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 ∈
ℂ) |
67 | 66 | adantl 485 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ ℂ) |
68 | 63, 64, 67 | addsubd 11215 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((((♯‘𝑇) − 1) +
(♯‘𝑆)) −
𝑥) =
((((♯‘𝑇)
− 1) − 𝑥) +
(♯‘𝑆))) |
69 | 59, 68 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆))) |
70 | 69 | fveq2d 6726 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = ((𝑆 ++ 𝑇)‘((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆)))) |
71 | | revfv 14333 |
. . . . . . 7
⊢ ((𝑇 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((reverse‘𝑇)‘𝑥) = (𝑇‘(((♯‘𝑇) − 1) − 𝑥))) |
72 | 71 | adantll 714 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((reverse‘𝑇)‘𝑥) = (𝑇‘(((♯‘𝑇) − 1) − 𝑥))) |
73 | 50, 70, 72 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = ((reverse‘𝑇)‘𝑥)) |
74 | 34 | uzidd 12459 |
. . . . . . . . . 10
⊢ (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈
(ℤ≥‘(♯‘𝑇))) |
75 | | uzaddcl 12505 |
. . . . . . . . . 10
⊢
(((♯‘𝑇)
∈ (ℤ≥‘(♯‘𝑇)) ∧ (♯‘𝑆) ∈ ℕ0) →
((♯‘𝑇) +
(♯‘𝑆)) ∈
(ℤ≥‘(♯‘𝑇))) |
76 | 74, 8, 75 | syl2anr 600 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑇) + (♯‘𝑆)) ∈
(ℤ≥‘(♯‘𝑇))) |
77 | 51, 76 | eqeltrd 2838 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘(𝑆 ++ 𝑇)) ∈
(ℤ≥‘(♯‘𝑇))) |
78 | | fzoss2 13275 |
. . . . . . . 8
⊢
((♯‘(𝑆
++ 𝑇)) ∈
(ℤ≥‘(♯‘𝑇)) → (0..^(♯‘𝑇)) ⊆
(0..^(♯‘(𝑆 ++
𝑇)))) |
79 | 77, 78 | syl 17 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(♯‘𝑇)) ⊆
(0..^(♯‘(𝑆 ++
𝑇)))) |
80 | 79 | sselda 3906 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^(♯‘(𝑆 ++ 𝑇)))) |
81 | | revfv 14333 |
. . . . . 6
⊢ (((𝑆 ++ 𝑇) ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘(𝑆 ++ 𝑇)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
82 | 1, 80, 81 | syl2an2r 685 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
83 | 18 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (reverse‘𝑇) ∈ Word 𝐴) |
84 | 19 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (reverse‘𝑆) ∈ Word 𝐴) |
85 | 26 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘(reverse‘𝑇)) = (♯‘𝑇)) |
86 | 85 | oveq2d 7234 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(0..^(♯‘(reverse‘𝑇))) = (0..^(♯‘𝑇))) |
87 | 86 | eleq2d 2823 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 ∈
(0..^(♯‘(reverse‘𝑇))) ↔ 𝑥 ∈ (0..^(♯‘𝑇)))) |
88 | 87 | biimpar 481 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈
(0..^(♯‘(reverse‘𝑇)))) |
89 | | ccatval1 14138 |
. . . . . 6
⊢
(((reverse‘𝑇)
∈ Word 𝐴 ∧
(reverse‘𝑆) ∈
Word 𝐴 ∧ 𝑥 ∈
(0..^(♯‘(reverse‘𝑇)))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑇)‘𝑥)) |
90 | 83, 84, 88, 89 | syl3anc 1373 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑇)‘𝑥)) |
91 | 73, 82, 90 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥)) |
92 | 8 | nn0zd 12285 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈ ℤ) |
93 | | peano2zm 12225 |
. . . . . . . . . . . 12
⊢
((♯‘𝑆)
∈ ℤ → ((♯‘𝑆) − 1) ∈
ℤ) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝐴 → ((♯‘𝑆) − 1) ∈
ℤ) |
95 | 94 | zcnd 12288 |
. . . . . . . . . 10
⊢ (𝑆 ∈ Word 𝐴 → ((♯‘𝑆) − 1) ∈
ℂ) |
96 | 95 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((♯‘𝑆) − 1) ∈
ℂ) |
97 | | elfzoelz 13248 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) → 𝑥 ∈ ℤ) |
98 | 97 | zcnd 12288 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) → 𝑥 ∈ ℂ) |
99 | 98 | adantl 485 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑥 ∈ ℂ) |
100 | 11 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (♯‘𝑇) ∈ ℂ) |
101 | 96, 99, 100 | subsub3d 11224 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘𝑆) − 1) − (𝑥 − (♯‘𝑇))) = ((((♯‘𝑆) − 1) +
(♯‘𝑇)) −
𝑥)) |
102 | 26 | oveq2d 7234 |
. . . . . . . . . 10
⊢ (𝑇 ∈ Word 𝐴 → (𝑥 − (♯‘(reverse‘𝑇))) = (𝑥 − (♯‘𝑇))) |
103 | 102 | oveq2d 7234 |
. . . . . . . . 9
⊢ (𝑇 ∈ Word 𝐴 → (((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇)))) = (((♯‘𝑆) − 1) − (𝑥 − (♯‘𝑇)))) |
104 | 103 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘𝑆) − 1) − (𝑥 −
(♯‘(reverse‘𝑇)))) = (((♯‘𝑆) − 1) − (𝑥 − (♯‘𝑇)))) |
105 | 7 | oveq1d 7233 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘(𝑆 ++ 𝑇)) − 1) = (((♯‘𝑆) + (♯‘𝑇)) − 1)) |
106 | 54, 53, 55 | addsubd 11215 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘𝑆) + (♯‘𝑇)) − 1) = (((♯‘𝑆) − 1) +
(♯‘𝑇))) |
107 | 105, 106 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘(𝑆 ++ 𝑇)) − 1) = (((♯‘𝑆) − 1) +
(♯‘𝑇))) |
108 | 107 | oveq1d 7233 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑆) − 1) + (♯‘𝑇)) − 𝑥)) |
109 | 108 | adantr 484 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑆) − 1) + (♯‘𝑇)) − 𝑥)) |
110 | 101, 104,
109 | 3eqtr4rd 2788 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = (((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇))))) |
111 | 110 | fveq2d 6726 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑆‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = (𝑆‘(((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇)))))) |
112 | | simpll 767 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑆 ∈ Word 𝐴) |
113 | | simplr 769 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑇 ∈ Word 𝐴) |
114 | | zaddcl 12222 |
. . . . . . . . . . 11
⊢
(((♯‘𝑇)
∈ ℤ ∧ (♯‘𝑆) ∈ ℤ) →
((♯‘𝑇) +
(♯‘𝑆)) ∈
ℤ) |
115 | 34, 92, 114 | syl2anr 600 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑇) + (♯‘𝑆)) ∈ ℤ) |
116 | | peano2zm 12225 |
. . . . . . . . . 10
⊢
(((♯‘𝑇)
+ (♯‘𝑆)) ∈
ℤ → (((♯‘𝑇) + (♯‘𝑆)) − 1) ∈
ℤ) |
117 | 115, 116 | syl 17 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘𝑇) + (♯‘𝑆)) − 1) ∈
ℤ) |
118 | | fzoval 13249 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑇)
+ (♯‘𝑆)) ∈
ℤ → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) = ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1))) |
119 | 115, 118 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) = ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1))) |
120 | 119 | eleq2d 2823 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ↔ 𝑥 ∈ ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1)))) |
121 | 120 | biimpa 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑥 ∈ ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1))) |
122 | | fzrev2i 13182 |
. . . . . . . . 9
⊢
(((((♯‘𝑇) + (♯‘𝑆)) − 1) ∈ ℤ ∧ 𝑥 ∈ ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1))) →
((((♯‘𝑇) +
(♯‘𝑆)) −
1) − 𝑥) ∈
(((((♯‘𝑇) +
(♯‘𝑆)) −
1) − (((♯‘𝑇) + (♯‘𝑆)) − 1))...((((♯‘𝑇) + (♯‘𝑆)) − 1) −
(♯‘𝑇)))) |
123 | 117, 121,
122 | syl2an2r 685 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − 𝑥) ∈
(((((♯‘𝑇) +
(♯‘𝑆)) −
1) − (((♯‘𝑇) + (♯‘𝑆)) − 1))...((((♯‘𝑇) + (♯‘𝑆)) − 1) −
(♯‘𝑇)))) |
124 | 52 | oveq1d 7233 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) + (♯‘𝑆)) − 1) − 𝑥)) |
125 | 124 | adantr 484 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) + (♯‘𝑆)) − 1) − 𝑥)) |
126 | 92 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘𝑆) ∈ ℤ) |
127 | | fzoval 13249 |
. . . . . . . . . . 11
⊢
((♯‘𝑆)
∈ ℤ → (0..^(♯‘𝑆)) = (0...((♯‘𝑆) − 1))) |
128 | 126, 127 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(♯‘𝑆)) = (0...((♯‘𝑆) − 1))) |
129 | 117 | zcnd 12288 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘𝑇) + (♯‘𝑆)) − 1) ∈
ℂ) |
130 | 129 | subidd 11182 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − (((♯‘𝑇) + (♯‘𝑆)) − 1)) =
0) |
131 | | addcl 10816 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝑇)
∈ ℂ ∧ (♯‘𝑆) ∈ ℂ) →
((♯‘𝑇) +
(♯‘𝑆)) ∈
ℂ) |
132 | 11, 9, 131 | syl2anr 600 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑇) + (♯‘𝑆)) ∈ ℂ) |
133 | 132, 55, 53 | sub32d 11226 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − (♯‘𝑇)) = ((((♯‘𝑇) + (♯‘𝑆)) − (♯‘𝑇)) − 1)) |
134 | | pncan2 11090 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝑇)
∈ ℂ ∧ (♯‘𝑆) ∈ ℂ) →
(((♯‘𝑇) +
(♯‘𝑆)) −
(♯‘𝑇)) =
(♯‘𝑆)) |
135 | 11, 9, 134 | syl2anr 600 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘𝑇) + (♯‘𝑆)) − (♯‘𝑇)) = (♯‘𝑆)) |
136 | 135 | oveq1d 7233 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((((♯‘𝑇) + (♯‘𝑆)) − (♯‘𝑇)) − 1) = ((♯‘𝑆) − 1)) |
137 | 133, 136 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − (♯‘𝑇)) = ((♯‘𝑆) − 1)) |
138 | 130, 137 | oveq12d 7236 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((((♯‘𝑇) + (♯‘𝑆)) − 1) −
(((♯‘𝑇) +
(♯‘𝑆)) −
1))...((((♯‘𝑇)
+ (♯‘𝑆))
− 1) − (♯‘𝑇))) = (0...((♯‘𝑆) − 1))) |
139 | 128, 138 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(♯‘𝑆)) = (((((♯‘𝑇) + (♯‘𝑆)) − 1) −
(((♯‘𝑇) +
(♯‘𝑆)) −
1))...((((♯‘𝑇)
+ (♯‘𝑆))
− 1) − (♯‘𝑇)))) |
140 | 139 | adantr 484 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (0..^(♯‘𝑆)) = (((((♯‘𝑇) + (♯‘𝑆)) − 1) −
(((♯‘𝑇) +
(♯‘𝑆)) −
1))...((((♯‘𝑇)
+ (♯‘𝑆))
− 1) − (♯‘𝑇)))) |
141 | 123, 125,
140 | 3eltr4d 2853 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) ∈ (0..^(♯‘𝑆))) |
142 | | ccatval1 14138 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = (𝑆‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
143 | 112, 113,
141, 142 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = (𝑆‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
144 | | simpl 486 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → 𝑆 ∈ Word 𝐴) |
145 | 102 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑥 − (♯‘(reverse‘𝑇))) = (𝑥 − (♯‘𝑇))) |
146 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) → 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) |
147 | | fzosubel3 13308 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ∧ (♯‘𝑆) ∈ ℤ) → (𝑥 − (♯‘𝑇)) ∈
(0..^(♯‘𝑆))) |
148 | 146, 126,
147 | syl2anr 600 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑥 − (♯‘𝑇)) ∈ (0..^(♯‘𝑆))) |
149 | 145, 148 | eqeltrd 2838 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑥 − (♯‘(reverse‘𝑇))) ∈
(0..^(♯‘𝑆))) |
150 | | revfv 14333 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑥 − (♯‘(reverse‘𝑇))) ∈
(0..^(♯‘𝑆)))
→ ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇)))) = (𝑆‘(((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇)))))) |
151 | 144, 149,
150 | syl2an2r 685 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇)))) = (𝑆‘(((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇)))))) |
152 | 111, 143,
151 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇))))) |
153 | | fzoss1 13274 |
. . . . . . . . . . 11
⊢
((♯‘𝑇)
∈ (ℤ≥‘0) → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆
(0..^((♯‘𝑇) +
(♯‘𝑆)))) |
154 | | nn0uz 12481 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
155 | 153, 154 | eleq2s 2856 |
. . . . . . . . . 10
⊢
((♯‘𝑇)
∈ ℕ0 → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆ (0..^((♯‘𝑇) + (♯‘𝑆)))) |
156 | 10, 155 | syl 17 |
. . . . . . . . 9
⊢ (𝑇 ∈ Word 𝐴 → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆ (0..^((♯‘𝑇) + (♯‘𝑆)))) |
157 | 156 | adantl 485 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆ (0..^((♯‘𝑇) + (♯‘𝑆)))) |
158 | 51 | oveq2d 7234 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(♯‘(𝑆 ++ 𝑇))) = (0..^((♯‘𝑇) + (♯‘𝑆)))) |
159 | 157, 158 | sseqtrrd 3947 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆ (0..^(♯‘(𝑆 ++ 𝑇)))) |
160 | 159 | sselda 3906 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑥 ∈ (0..^(♯‘(𝑆 ++ 𝑇)))) |
161 | 1, 160, 81 | syl2an2r 685 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
162 | 18 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (reverse‘𝑇) ∈ Word 𝐴) |
163 | 19 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (reverse‘𝑆) ∈ Word 𝐴) |
164 | 85, 28 | oveq12d 7236 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
((♯‘(reverse‘𝑇))..^((♯‘(reverse‘𝑇)) +
(♯‘(reverse‘𝑆)))) = ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) |
165 | 164 | eleq2d 2823 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 ∈ ((♯‘(reverse‘𝑇))..^((♯‘(reverse‘𝑇)) +
(♯‘(reverse‘𝑆)))) ↔ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))))) |
166 | 165 | biimpar 481 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑥 ∈ ((♯‘(reverse‘𝑇))..^((♯‘(reverse‘𝑇)) +
(♯‘(reverse‘𝑆))))) |
167 | | ccatval2 14140 |
. . . . . 6
⊢
(((reverse‘𝑇)
∈ Word 𝐴 ∧
(reverse‘𝑆) ∈
Word 𝐴 ∧ 𝑥 ∈
((♯‘(reverse‘𝑇))..^((♯‘(reverse‘𝑇)) +
(♯‘(reverse‘𝑆))))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇))))) |
168 | 162, 163,
166, 167 | syl3anc 1373 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇))))) |
169 | 152, 161,
168 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥)) |
170 | 91, 169 | jaodan 958 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ (𝑥 ∈ (0..^(♯‘𝑇)) ∨ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥)) |
171 | 37, 170 | syldan 594 |
. 2
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^((♯‘𝑇) + (♯‘𝑆)))) →
((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥)) |
172 | 17, 32, 171 | eqfnfvd 6860 |
1
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) = ((reverse‘𝑇) ++ (reverse‘𝑆))) |