Step | Hyp | Ref
| Expression |
1 | | wrdfn 13319 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐴 → 𝑊 Fn (0..^(#‘𝑊))) |
2 | 1 | ad2antrr 762 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑊))) → 𝑊 Fn (0..^(#‘𝑊))) |
3 | | lencl 13324 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝐴 → (#‘𝑊) ∈
ℕ0) |
4 | 3 | nn0zd 11480 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝐴 → (#‘𝑊) ∈ ℤ) |
5 | | fzoval 12471 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) ∈
ℤ → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐴 → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
7 | 6 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
8 | 7 | eleq2d 2687 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^(#‘𝑊)) ↔ 𝑥 ∈ (0...((#‘𝑊) − 1)))) |
9 | 8 | biimpa 501 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑊))) → 𝑥 ∈ (0...((#‘𝑊) − 1))) |
10 | | fznn0sub2 12446 |
. . . . . . . 8
⊢ (𝑥 ∈ (0...((#‘𝑊) − 1)) →
(((#‘𝑊) − 1)
− 𝑥) ∈
(0...((#‘𝑊) −
1))) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (((#‘𝑊) − 1) − 𝑥) ∈ (0...((#‘𝑊) − 1))) |
12 | 7 | adantr 481 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
13 | 11, 12 | eleqtrrd 2704 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (((#‘𝑊) − 1) − 𝑥) ∈ (0..^(#‘𝑊))) |
14 | | fvco2 6273 |
. . . . . 6
⊢ ((𝑊 Fn (0..^(#‘𝑊)) ∧ (((#‘𝑊) − 1) − 𝑥) ∈ (0..^(#‘𝑊))) → ((𝐹 ∘ 𝑊)‘(((#‘𝑊) − 1) − 𝑥)) = (𝐹‘(𝑊‘(((#‘𝑊) − 1) − 𝑥)))) |
15 | 2, 13, 14 | syl2anc 693 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((𝐹 ∘ 𝑊)‘(((#‘𝑊) − 1) − 𝑥)) = (𝐹‘(𝑊‘(((#‘𝑊) − 1) − 𝑥)))) |
16 | | lenco 13578 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘(𝐹 ∘ 𝑊)) = (#‘𝑊)) |
17 | 16 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → ((#‘(𝐹 ∘ 𝑊)) − 1) = ((#‘𝑊) − 1)) |
18 | 17 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (((#‘(𝐹 ∘ 𝑊)) − 1) − 𝑥) = (((#‘𝑊) − 1) − 𝑥)) |
19 | 18 | adantr 481 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (((#‘(𝐹 ∘ 𝑊)) − 1) − 𝑥) = (((#‘𝑊) − 1) − 𝑥)) |
20 | 19 | fveq2d 6195 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((𝐹 ∘ 𝑊)‘(((#‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)) = ((𝐹 ∘ 𝑊)‘(((#‘𝑊) − 1) − 𝑥))) |
21 | | revfv 13512 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘𝑥) = (𝑊‘(((#‘𝑊) − 1) − 𝑥))) |
22 | 21 | adantlr 751 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘𝑥) = (𝑊‘(((#‘𝑊) − 1) − 𝑥))) |
23 | 22 | fveq2d 6195 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (𝐹‘((reverse‘𝑊)‘𝑥)) = (𝐹‘(𝑊‘(((#‘𝑊) − 1) − 𝑥)))) |
24 | 15, 20, 23 | 3eqtr4d 2666 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((𝐹 ∘ 𝑊)‘(((#‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)) = (𝐹‘((reverse‘𝑊)‘𝑥))) |
25 | 24 | mpteq2dva 4744 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^(#‘𝑊)) ↦ ((𝐹 ∘ 𝑊)‘(((#‘(𝐹 ∘ 𝑊)) − 1) − 𝑥))) = (𝑥 ∈ (0..^(#‘𝑊)) ↦ (𝐹‘((reverse‘𝑊)‘𝑥)))) |
26 | 16 | oveq2d 6666 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0..^(#‘(𝐹 ∘ 𝑊))) = (0..^(#‘𝑊))) |
27 | 26 | mpteq1d 4738 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑊))) ↦ ((𝐹 ∘ 𝑊)‘(((#‘(𝐹 ∘ 𝑊)) − 1) − 𝑥))) = (𝑥 ∈ (0..^(#‘𝑊)) ↦ ((𝐹 ∘ 𝑊)‘(((#‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)))) |
28 | | revlen 13511 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 → (#‘(reverse‘𝑊)) = (#‘𝑊)) |
29 | 28 | adantr 481 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘(reverse‘𝑊)) = (#‘𝑊)) |
30 | 29 | oveq2d 6666 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0..^(#‘(reverse‘𝑊))) = (0..^(#‘𝑊))) |
31 | 30 | mpteq1d 4738 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^(#‘(reverse‘𝑊))) ↦ (𝐹‘((reverse‘𝑊)‘𝑥))) = (𝑥 ∈ (0..^(#‘𝑊)) ↦ (𝐹‘((reverse‘𝑊)‘𝑥)))) |
32 | 25, 27, 31 | 3eqtr4rd 2667 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^(#‘(reverse‘𝑊))) ↦ (𝐹‘((reverse‘𝑊)‘𝑥))) = (𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑊))) ↦ ((𝐹 ∘ 𝑊)‘(((#‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)))) |
33 | | simpr 477 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴⟶𝐵) |
34 | | revcl 13510 |
. . . . 5
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊) ∈ Word 𝐴) |
35 | | wrdf 13310 |
. . . . 5
⊢
((reverse‘𝑊)
∈ Word 𝐴 →
(reverse‘𝑊):(0..^(#‘(reverse‘𝑊)))⟶𝐴) |
36 | 34, 35 | syl 17 |
. . . 4
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊):(0..^(#‘(reverse‘𝑊)))⟶𝐴) |
37 | 36 | adantr 481 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (reverse‘𝑊):(0..^(#‘(reverse‘𝑊)))⟶𝐴) |
38 | | fcompt 6400 |
. . 3
⊢ ((𝐹:𝐴⟶𝐵 ∧ (reverse‘𝑊):(0..^(#‘(reverse‘𝑊)))⟶𝐴) → (𝐹 ∘ (reverse‘𝑊)) = (𝑥 ∈ (0..^(#‘(reverse‘𝑊))) ↦ (𝐹‘((reverse‘𝑊)‘𝑥)))) |
39 | 33, 37, 38 | syl2anc 693 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (reverse‘𝑊)) = (𝑥 ∈ (0..^(#‘(reverse‘𝑊))) ↦ (𝐹‘((reverse‘𝑊)‘𝑥)))) |
40 | | ffun 6048 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
41 | 40 | adantl 482 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → Fun 𝐹) |
42 | | simpl 473 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑊 ∈ Word 𝐴) |
43 | | cofunexg 7130 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝑊 ∈ Word 𝐴) → (𝐹 ∘ 𝑊) ∈ V) |
44 | 41, 42, 43 | syl2anc 693 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ V) |
45 | | revval 13509 |
. . 3
⊢ ((𝐹 ∘ 𝑊) ∈ V → (reverse‘(𝐹 ∘ 𝑊)) = (𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑊))) ↦ ((𝐹 ∘ 𝑊)‘(((#‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)))) |
46 | 44, 45 | syl 17 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (reverse‘(𝐹 ∘ 𝑊)) = (𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑊))) ↦ ((𝐹 ∘ 𝑊)‘(((#‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)))) |
47 | 32, 39, 46 | 3eqtr4d 2666 |
1
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (reverse‘𝑊)) = (reverse‘(𝐹 ∘ 𝑊))) |