Step | Hyp | Ref
| Expression |
1 | | ccatcl 13594 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑆 ++ 𝑇) ∈ Word 𝐴) |
2 | | revcl 13841 |
. . . 4
⊢ ((𝑆 ++ 𝑇) ∈ Word 𝐴 → (reverse‘(𝑆 ++ 𝑇)) ∈ Word 𝐴) |
3 | | wrdf 13539 |
. . . 4
⊢
((reverse‘(𝑆
++ 𝑇)) ∈ Word 𝐴 → (reverse‘(𝑆 ++ 𝑇)):(0..^(♯‘(reverse‘(𝑆 ++ 𝑇))))⟶𝐴) |
4 | | ffn 6256 |
. . . 4
⊢
((reverse‘(𝑆
++ 𝑇)):(0..^(♯‘(reverse‘(𝑆 ++ 𝑇))))⟶𝐴 → (reverse‘(𝑆 ++ 𝑇)) Fn
(0..^(♯‘(reverse‘(𝑆 ++ 𝑇))))) |
5 | 1, 2, 3, 4 | 4syl 19 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) Fn
(0..^(♯‘(reverse‘(𝑆 ++ 𝑇))))) |
6 | | revlen 13842 |
. . . . . . 7
⊢ ((𝑆 ++ 𝑇) ∈ Word 𝐴 → (♯‘(reverse‘(𝑆 ++ 𝑇))) = (♯‘(𝑆 ++ 𝑇))) |
7 | 1, 6 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(♯‘(reverse‘(𝑆 ++ 𝑇))) = (♯‘(𝑆 ++ 𝑇))) |
8 | | ccatlen 13595 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇))) |
9 | | lencl 13553 |
. . . . . . . . 9
⊢ (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈
ℕ0) |
10 | 9 | nn0cnd 11642 |
. . . . . . . 8
⊢ (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈ ℂ) |
11 | | lencl 13553 |
. . . . . . . . 9
⊢ (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈
ℕ0) |
12 | 11 | nn0cnd 11642 |
. . . . . . . 8
⊢ (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈ ℂ) |
13 | | addcom 10512 |
. . . . . . . 8
⊢
(((♯‘𝑆)
∈ ℂ ∧ (♯‘𝑇) ∈ ℂ) →
((♯‘𝑆) +
(♯‘𝑇)) =
((♯‘𝑇) +
(♯‘𝑆))) |
14 | 10, 12, 13 | syl2an 590 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑆) + (♯‘𝑇)) = ((♯‘𝑇) + (♯‘𝑆))) |
15 | 8, 14 | eqtrd 2833 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑇) + (♯‘𝑆))) |
16 | 7, 15 | eqtrd 2833 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(♯‘(reverse‘(𝑆 ++ 𝑇))) = ((♯‘𝑇) + (♯‘𝑆))) |
17 | 16 | oveq2d 6894 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(0..^(♯‘(reverse‘(𝑆 ++ 𝑇)))) = (0..^((♯‘𝑇) + (♯‘𝑆)))) |
18 | 17 | fneq2d 6193 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((reverse‘(𝑆 ++ 𝑇)) Fn
(0..^(♯‘(reverse‘(𝑆 ++ 𝑇)))) ↔ (reverse‘(𝑆 ++ 𝑇)) Fn (0..^((♯‘𝑇) + (♯‘𝑆))))) |
19 | 5, 18 | mpbid 224 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) Fn (0..^((♯‘𝑇) + (♯‘𝑆)))) |
20 | | revcl 13841 |
. . . . 5
⊢ (𝑇 ∈ Word 𝐴 → (reverse‘𝑇) ∈ Word 𝐴) |
21 | | revcl 13841 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (reverse‘𝑆) ∈ Word 𝐴) |
22 | | ccatcl 13594 |
. . . . 5
⊢
(((reverse‘𝑇)
∈ Word 𝐴 ∧
(reverse‘𝑆) ∈
Word 𝐴) →
((reverse‘𝑇) ++
(reverse‘𝑆)) ∈
Word 𝐴) |
23 | 20, 21, 22 | syl2anr 591 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((reverse‘𝑇) ++ (reverse‘𝑆)) ∈ Word 𝐴) |
24 | | wrdf 13539 |
. . . 4
⊢
(((reverse‘𝑇)
++ (reverse‘𝑆))
∈ Word 𝐴 →
((reverse‘𝑇) ++
(reverse‘𝑆)):(0..^(♯‘((reverse‘𝑇) ++ (reverse‘𝑆))))⟶𝐴) |
25 | | ffn 6256 |
. . . 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 13595 |
. . . . . . 7
⊢
(((reverse‘𝑇)
∈ Word 𝐴 ∧
(reverse‘𝑆) ∈
Word 𝐴) →
(♯‘((reverse‘𝑇) ++ (reverse‘𝑆))) = ((♯‘(reverse‘𝑇)) +
(♯‘(reverse‘𝑆)))) |
28 | 20, 21, 27 | syl2anr 591 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(♯‘((reverse‘𝑇) ++ (reverse‘𝑆))) = ((♯‘(reverse‘𝑇)) +
(♯‘(reverse‘𝑆)))) |
29 | | revlen 13842 |
. . . . . . 7
⊢ (𝑇 ∈ Word 𝐴 → (♯‘(reverse‘𝑇)) = (♯‘𝑇)) |
30 | | revlen 13842 |
. . . . . . 7
⊢ (𝑆 ∈ Word 𝐴 → (♯‘(reverse‘𝑆)) = (♯‘𝑆)) |
31 | 29, 30 | oveqan12rd 6898 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
((♯‘(reverse‘𝑇)) + (♯‘(reverse‘𝑆))) = ((♯‘𝑇) + (♯‘𝑆))) |
32 | 28, 31 | eqtrd 2833 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(♯‘((reverse‘𝑇) ++ (reverse‘𝑆))) = ((♯‘𝑇) + (♯‘𝑆))) |
33 | 32 | oveq2d 6894 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(0..^(♯‘((reverse‘𝑇) ++ (reverse‘𝑆)))) = (0..^((♯‘𝑇) + (♯‘𝑆)))) |
34 | 33 | fneq2d 6193 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((reverse‘𝑇) ++ (reverse‘𝑆)) Fn
(0..^(♯‘((reverse‘𝑇) ++ (reverse‘𝑆)))) ↔ ((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^((♯‘𝑇) + (♯‘𝑆))))) |
35 | 26, 34 | mpbid 224 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^((♯‘𝑇) + (♯‘𝑆)))) |
36 | | id 22 |
. . . 4
⊢ (𝑥 ∈
(0..^((♯‘𝑇) +
(♯‘𝑆))) →
𝑥 ∈
(0..^((♯‘𝑇) +
(♯‘𝑆)))) |
37 | 11 | nn0zd 11770 |
. . . . 5
⊢ (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈ ℤ) |
38 | 37 | adantl 474 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘𝑇) ∈ ℤ) |
39 | | fzospliti 12755 |
. . . 4
⊢ ((𝑥 ∈
(0..^((♯‘𝑇) +
(♯‘𝑆))) ∧
(♯‘𝑇) ∈
ℤ) → (𝑥 ∈
(0..^(♯‘𝑇))
∨ 𝑥 ∈
((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))))) |
40 | 36, 38, 39 | syl2anr 591 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑥 ∈ (0..^(♯‘𝑇)) ∨ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))))) |
41 | | simpll 784 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑆 ∈ Word 𝐴) |
42 | | simplr 786 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑇 ∈ Word 𝐴) |
43 | | fzoval 12726 |
. . . . . . . . . . . 12
⊢
((♯‘𝑇)
∈ ℤ → (0..^(♯‘𝑇)) = (0...((♯‘𝑇) − 1))) |
44 | 38, 43 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(♯‘𝑇)) = (0...((♯‘𝑇) − 1))) |
45 | 44 | eleq2d 2864 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑥 ∈ (0...((♯‘𝑇) − 1)))) |
46 | 45 | biimpa 469 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0...((♯‘𝑇) − 1))) |
47 | | fznn0sub2 12701 |
. . . . . . . . 9
⊢ (𝑥 ∈
(0...((♯‘𝑇)
− 1)) → (((♯‘𝑇) − 1) − 𝑥) ∈ (0...((♯‘𝑇) − 1))) |
48 | 46, 47 | syl 17 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((♯‘𝑇) − 1) − 𝑥) ∈
(0...((♯‘𝑇)
− 1))) |
49 | 44 | adantr 473 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (0..^(♯‘𝑇)) = (0...((♯‘𝑇) − 1))) |
50 | 48, 49 | eleqtrrd 2881 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((♯‘𝑇) − 1) − 𝑥) ∈
(0..^(♯‘𝑇))) |
51 | | ccatval3 13599 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ (((♯‘𝑇) − 1) − 𝑥) ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆))) = (𝑇‘(((♯‘𝑇) − 1) − 𝑥))) |
52 | 41, 42, 50, 51 | syl3anc 1491 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆))) = (𝑇‘(((♯‘𝑇) − 1) − 𝑥))) |
53 | 15 | oveq1d 6893 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘(𝑆 ++ 𝑇)) − 1) = (((♯‘𝑇) + (♯‘𝑆)) − 1)) |
54 | 12 | adantl 474 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘𝑇) ∈ ℂ) |
55 | 10 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘𝑆) ∈ ℂ) |
56 | | 1cnd 10323 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → 1 ∈ ℂ) |
57 | 54, 55, 56 | addsubd 10705 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘𝑇) + (♯‘𝑆)) − 1) = (((♯‘𝑇) − 1) +
(♯‘𝑆))) |
58 | 53, 57 | eqtrd 2833 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘(𝑆 ++ 𝑇)) − 1) = (((♯‘𝑇) − 1) +
(♯‘𝑆))) |
59 | 58 | oveq1d 6893 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) − 1) + (♯‘𝑆)) − 𝑥)) |
60 | 59 | adantr 473 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) − 1) + (♯‘𝑆)) − 𝑥)) |
61 | | peano2zm 11710 |
. . . . . . . . . . . 12
⊢
((♯‘𝑇)
∈ ℤ → ((♯‘𝑇) − 1) ∈
ℤ) |
62 | 37, 61 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ Word 𝐴 → ((♯‘𝑇) − 1) ∈
ℤ) |
63 | 62 | zcnd 11773 |
. . . . . . . . . 10
⊢ (𝑇 ∈ Word 𝐴 → ((♯‘𝑇) − 1) ∈
ℂ) |
64 | 63 | ad2antlr 719 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((♯‘𝑇) − 1) ∈
ℂ) |
65 | 10 | ad2antrr 718 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (♯‘𝑆) ∈ ℂ) |
66 | | elfzoelz 12725 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 ∈
ℤ) |
67 | 66 | zcnd 11773 |
. . . . . . . . . 10
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 ∈
ℂ) |
68 | 67 | adantl 474 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ ℂ) |
69 | 64, 65, 68 | addsubd 10705 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((((♯‘𝑇) − 1) +
(♯‘𝑆)) −
𝑥) =
((((♯‘𝑇)
− 1) − 𝑥) +
(♯‘𝑆))) |
70 | 60, 69 | eqtrd 2833 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆))) |
71 | 70 | fveq2d 6415 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = ((𝑆 ++ 𝑇)‘((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆)))) |
72 | | revfv 13843 |
. . . . . . 7
⊢ ((𝑇 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((reverse‘𝑇)‘𝑥) = (𝑇‘(((♯‘𝑇) − 1) − 𝑥))) |
73 | 72 | adantll 706 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((reverse‘𝑇)‘𝑥) = (𝑇‘(((♯‘𝑇) − 1) − 𝑥))) |
74 | 52, 71, 73 | 3eqtr4d 2843 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = ((reverse‘𝑇)‘𝑥)) |
75 | 1 | adantr 473 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑆 ++ 𝑇) ∈ Word 𝐴) |
76 | | uzid 11945 |
. . . . . . . . . . 11
⊢
((♯‘𝑇)
∈ ℤ → (♯‘𝑇) ∈
(ℤ≥‘(♯‘𝑇))) |
77 | 38, 76 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘𝑇) ∈
(ℤ≥‘(♯‘𝑇))) |
78 | 9 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘𝑆) ∈
ℕ0) |
79 | | uzaddcl 11988 |
. . . . . . . . . 10
⊢
(((♯‘𝑇)
∈ (ℤ≥‘(♯‘𝑇)) ∧ (♯‘𝑆) ∈ ℕ0) →
((♯‘𝑇) +
(♯‘𝑆)) ∈
(ℤ≥‘(♯‘𝑇))) |
80 | 77, 78, 79 | syl2anc 580 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑇) + (♯‘𝑆)) ∈
(ℤ≥‘(♯‘𝑇))) |
81 | 15, 80 | eqeltrd 2878 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘(𝑆 ++ 𝑇)) ∈
(ℤ≥‘(♯‘𝑇))) |
82 | | fzoss2 12751 |
. . . . . . . 8
⊢
((♯‘(𝑆
++ 𝑇)) ∈
(ℤ≥‘(♯‘𝑇)) → (0..^(♯‘𝑇)) ⊆
(0..^(♯‘(𝑆 ++
𝑇)))) |
83 | 81, 82 | syl 17 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(♯‘𝑇)) ⊆
(0..^(♯‘(𝑆 ++
𝑇)))) |
84 | 83 | sselda 3798 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^(♯‘(𝑆 ++ 𝑇)))) |
85 | | revfv 13843 |
. . . . . 6
⊢ (((𝑆 ++ 𝑇) ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘(𝑆 ++ 𝑇)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
86 | 75, 84, 85 | syl2anc 580 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
87 | 20 | ad2antlr 719 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (reverse‘𝑇) ∈ Word 𝐴) |
88 | 21 | ad2antrr 718 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (reverse‘𝑆) ∈ Word 𝐴) |
89 | 29 | adantl 474 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘(reverse‘𝑇)) = (♯‘𝑇)) |
90 | 89 | oveq2d 6894 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
(0..^(♯‘(reverse‘𝑇))) = (0..^(♯‘𝑇))) |
91 | 90 | eleq2d 2864 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 ∈
(0..^(♯‘(reverse‘𝑇))) ↔ 𝑥 ∈ (0..^(♯‘𝑇)))) |
92 | 91 | biimpar 470 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈
(0..^(♯‘(reverse‘𝑇)))) |
93 | | ccatval1 13597 |
. . . . . 6
⊢
(((reverse‘𝑇)
∈ Word 𝐴 ∧
(reverse‘𝑆) ∈
Word 𝐴 ∧ 𝑥 ∈
(0..^(♯‘(reverse‘𝑇)))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑇)‘𝑥)) |
94 | 87, 88, 92, 93 | syl3anc 1491 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑇)‘𝑥)) |
95 | 74, 86, 94 | 3eqtr4d 2843 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥)) |
96 | 8 | oveq1d 6893 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘(𝑆 ++ 𝑇)) − 1) = (((♯‘𝑆) + (♯‘𝑇)) − 1)) |
97 | 55, 54, 56 | addsubd 10705 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘𝑆) + (♯‘𝑇)) − 1) = (((♯‘𝑆) − 1) +
(♯‘𝑇))) |
98 | 96, 97 | eqtrd 2833 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘(𝑆 ++ 𝑇)) − 1) = (((♯‘𝑆) − 1) +
(♯‘𝑇))) |
99 | 98 | oveq1d 6893 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑆) − 1) + (♯‘𝑇)) − 𝑥)) |
100 | 99 | adantr 473 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑆) − 1) + (♯‘𝑇)) − 𝑥)) |
101 | 9 | nn0zd 11770 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈ ℤ) |
102 | | peano2zm 11710 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑆)
∈ ℤ → ((♯‘𝑆) − 1) ∈
ℤ) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐴 → ((♯‘𝑆) − 1) ∈
ℤ) |
104 | 103 | zcnd 11773 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝐴 → ((♯‘𝑆) − 1) ∈
ℂ) |
105 | 104 | ad2antrr 718 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((♯‘𝑆) − 1) ∈
ℂ) |
106 | | elfzoelz 12725 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) → 𝑥 ∈ ℤ) |
107 | 106 | zcnd 11773 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) → 𝑥 ∈ ℂ) |
108 | 107 | adantl 474 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑥 ∈ ℂ) |
109 | 12 | ad2antlr 719 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (♯‘𝑇) ∈ ℂ) |
110 | 105, 108,
109 | subsub3d 10714 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘𝑆) − 1) − (𝑥 − (♯‘𝑇))) = ((((♯‘𝑆) − 1) +
(♯‘𝑇)) −
𝑥)) |
111 | 100, 110 | eqtr4d 2836 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = (((♯‘𝑆) − 1) − (𝑥 − (♯‘𝑇)))) |
112 | 89 | oveq2d 6894 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 − (♯‘(reverse‘𝑇))) = (𝑥 − (♯‘𝑇))) |
113 | 112 | oveq2d 6894 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇)))) = (((♯‘𝑆) − 1) − (𝑥 − (♯‘𝑇)))) |
114 | 113 | adantr 473 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘𝑆) − 1) − (𝑥 −
(♯‘(reverse‘𝑇)))) = (((♯‘𝑆) − 1) − (𝑥 − (♯‘𝑇)))) |
115 | 111, 114 | eqtr4d 2836 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = (((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇))))) |
116 | 115 | fveq2d 6415 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑆‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = (𝑆‘(((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇)))))) |
117 | | simpll 784 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑆 ∈ Word 𝐴) |
118 | | simplr 786 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑇 ∈ Word 𝐴) |
119 | | zaddcl 11707 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑇)
∈ ℤ ∧ (♯‘𝑆) ∈ ℤ) →
((♯‘𝑇) +
(♯‘𝑆)) ∈
ℤ) |
120 | 37, 101, 119 | syl2anr 591 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑇) + (♯‘𝑆)) ∈ ℤ) |
121 | | peano2zm 11710 |
. . . . . . . . . . 11
⊢
(((♯‘𝑇)
+ (♯‘𝑆)) ∈
ℤ → (((♯‘𝑇) + (♯‘𝑆)) − 1) ∈
ℤ) |
122 | 120, 121 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘𝑇) + (♯‘𝑆)) − 1) ∈
ℤ) |
123 | 122 | adantr 473 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘𝑇) + (♯‘𝑆)) − 1) ∈
ℤ) |
124 | | fzoval 12726 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑇)
+ (♯‘𝑆)) ∈
ℤ → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) = ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1))) |
125 | 120, 124 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) = ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1))) |
126 | 125 | eleq2d 2864 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ↔ 𝑥 ∈ ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1)))) |
127 | 126 | biimpa 469 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑥 ∈ ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1))) |
128 | | fzrev2i 12659 |
. . . . . . . . 9
⊢
(((((♯‘𝑇) + (♯‘𝑆)) − 1) ∈ ℤ ∧ 𝑥 ∈ ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1))) →
((((♯‘𝑇) +
(♯‘𝑆)) −
1) − 𝑥) ∈
(((((♯‘𝑇) +
(♯‘𝑆)) −
1) − (((♯‘𝑇) + (♯‘𝑆)) − 1))...((((♯‘𝑇) + (♯‘𝑆)) − 1) −
(♯‘𝑇)))) |
129 | 123, 127,
128 | syl2anc 580 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − 𝑥) ∈
(((((♯‘𝑇) +
(♯‘𝑆)) −
1) − (((♯‘𝑇) + (♯‘𝑆)) − 1))...((((♯‘𝑇) + (♯‘𝑆)) − 1) −
(♯‘𝑇)))) |
130 | 53 | oveq1d 6893 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) + (♯‘𝑆)) − 1) − 𝑥)) |
131 | 130 | adantr 473 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) + (♯‘𝑆)) − 1) − 𝑥)) |
132 | 101 | adantr 473 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘𝑆) ∈ ℤ) |
133 | | fzoval 12726 |
. . . . . . . . . . 11
⊢
((♯‘𝑆)
∈ ℤ → (0..^(♯‘𝑆)) = (0...((♯‘𝑆) − 1))) |
134 | 132, 133 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(♯‘𝑆)) = (0...((♯‘𝑆) − 1))) |
135 | 122 | zcnd 11773 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘𝑇) + (♯‘𝑆)) − 1) ∈
ℂ) |
136 | 135 | subidd 10672 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − (((♯‘𝑇) + (♯‘𝑆)) − 1)) =
0) |
137 | | addcl 10306 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝑇)
∈ ℂ ∧ (♯‘𝑆) ∈ ℂ) →
((♯‘𝑇) +
(♯‘𝑆)) ∈
ℂ) |
138 | 12, 10, 137 | syl2anr 591 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑇) + (♯‘𝑆)) ∈ ℂ) |
139 | 138, 56, 54 | sub32d 10716 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − (♯‘𝑇)) = ((((♯‘𝑇) + (♯‘𝑆)) − (♯‘𝑇)) − 1)) |
140 | | pncan2 10579 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝑇)
∈ ℂ ∧ (♯‘𝑆) ∈ ℂ) →
(((♯‘𝑇) +
(♯‘𝑆)) −
(♯‘𝑇)) =
(♯‘𝑆)) |
141 | 12, 10, 140 | syl2anr 591 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((♯‘𝑇) + (♯‘𝑆)) − (♯‘𝑇)) = (♯‘𝑆)) |
142 | 141 | oveq1d 6893 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((((♯‘𝑇) + (♯‘𝑆)) − (♯‘𝑇)) − 1) = ((♯‘𝑆) − 1)) |
143 | 139, 142 | eqtrd 2833 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − (♯‘𝑇)) = ((♯‘𝑆) − 1)) |
144 | 136, 143 | oveq12d 6896 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (((((♯‘𝑇) + (♯‘𝑆)) − 1) −
(((♯‘𝑇) +
(♯‘𝑆)) −
1))...((((♯‘𝑇)
+ (♯‘𝑆))
− 1) − (♯‘𝑇))) = (0...((♯‘𝑆) − 1))) |
145 | 134, 144 | eqtr4d 2836 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(♯‘𝑆)) = (((((♯‘𝑇) + (♯‘𝑆)) − 1) −
(((♯‘𝑇) +
(♯‘𝑆)) −
1))...((((♯‘𝑇)
+ (♯‘𝑆))
− 1) − (♯‘𝑇)))) |
146 | 145 | adantr 473 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (0..^(♯‘𝑆)) = (((((♯‘𝑇) + (♯‘𝑆)) − 1) −
(((♯‘𝑇) +
(♯‘𝑆)) −
1))...((((♯‘𝑇)
+ (♯‘𝑆))
− 1) − (♯‘𝑇)))) |
147 | 129, 131,
146 | 3eltr4d 2893 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) ∈ (0..^(♯‘𝑆))) |
148 | | ccatval1 13597 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = (𝑆‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
149 | 117, 118,
147, 148 | syl3anc 1491 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = (𝑆‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
150 | 29 | ad2antlr 719 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) →
(♯‘(reverse‘𝑇)) = (♯‘𝑇)) |
151 | 150 | oveq2d 6894 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑥 − (♯‘(reverse‘𝑇))) = (𝑥 − (♯‘𝑇))) |
152 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) → 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) |
153 | | fzosubel3 12784 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ∧ (♯‘𝑆) ∈ ℤ) → (𝑥 − (♯‘𝑇)) ∈
(0..^(♯‘𝑆))) |
154 | 152, 132,
153 | syl2anr 591 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑥 − (♯‘𝑇)) ∈ (0..^(♯‘𝑆))) |
155 | 151, 154 | eqeltrd 2878 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑥 − (♯‘(reverse‘𝑇))) ∈
(0..^(♯‘𝑆))) |
156 | | revfv 13843 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑥 − (♯‘(reverse‘𝑇))) ∈
(0..^(♯‘𝑆)))
→ ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇)))) = (𝑆‘(((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇)))))) |
157 | 117, 155,
156 | syl2anc 580 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇)))) = (𝑆‘(((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇)))))) |
158 | 116, 149,
157 | 3eqtr4d 2843 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇))))) |
159 | 1 | adantr 473 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑆 ++ 𝑇) ∈ Word 𝐴) |
160 | 11 | adantl 474 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (♯‘𝑇) ∈
ℕ0) |
161 | | fzoss1 12750 |
. . . . . . . . . 10
⊢
((♯‘𝑇)
∈ (ℤ≥‘0) → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆
(0..^((♯‘𝑇) +
(♯‘𝑆)))) |
162 | | nn0uz 11966 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
163 | 161, 162 | eleq2s 2896 |
. . . . . . . . 9
⊢
((♯‘𝑇)
∈ ℕ0 → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆ (0..^((♯‘𝑇) + (♯‘𝑆)))) |
164 | 160, 163 | syl 17 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆ (0..^((♯‘𝑇) + (♯‘𝑆)))) |
165 | 15 | oveq2d 6894 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (0..^(♯‘(𝑆 ++ 𝑇))) = (0..^((♯‘𝑇) + (♯‘𝑆)))) |
166 | 164, 165 | sseqtr4d 3838 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆ (0..^(♯‘(𝑆 ++ 𝑇)))) |
167 | 166 | sselda 3798 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑥 ∈ (0..^(♯‘(𝑆 ++ 𝑇)))) |
168 | 159, 167,
85 | syl2anc 580 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥))) |
169 | 20 | ad2antlr 719 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (reverse‘𝑇) ∈ Word 𝐴) |
170 | 21 | ad2antrr 718 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (reverse‘𝑆) ∈ Word 𝐴) |
171 | 89, 31 | oveq12d 6896 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) →
((♯‘(reverse‘𝑇))..^((♯‘(reverse‘𝑇)) +
(♯‘(reverse‘𝑆)))) = ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) |
172 | 171 | eleq2d 2864 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑥 ∈ ((♯‘(reverse‘𝑇))..^((♯‘(reverse‘𝑇)) +
(♯‘(reverse‘𝑆)))) ↔ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))))) |
173 | 172 | biimpar 470 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑥 ∈ ((♯‘(reverse‘𝑇))..^((♯‘(reverse‘𝑇)) +
(♯‘(reverse‘𝑆))))) |
174 | | ccatval2 13598 |
. . . . . 6
⊢
(((reverse‘𝑇)
∈ Word 𝐴 ∧
(reverse‘𝑆) ∈
Word 𝐴 ∧ 𝑥 ∈
((♯‘(reverse‘𝑇))..^((♯‘(reverse‘𝑇)) +
(♯‘(reverse‘𝑆))))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇))))) |
175 | 169, 170,
173, 174 | syl3anc 1491 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇))))) |
176 | 158, 168,
175 | 3eqtr4d 2843 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥)) |
177 | 95, 176 | jaodan 981 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ (𝑥 ∈ (0..^(♯‘𝑇)) ∨ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥)) |
178 | 40, 177 | syldan 586 |
. 2
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^((♯‘𝑇) + (♯‘𝑆)))) →
((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥)) |
179 | 19, 35, 178 | eqfnfvd 6540 |
1
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) = ((reverse‘𝑇) ++ (reverse‘𝑆))) |