Step | Hyp | Ref
| Expression |
1 | | wrdfn 14231 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐴 → 𝑊 Fn (0..^(♯‘𝑊))) |
2 | 1 | ad2antrr 723 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → 𝑊 Fn (0..^(♯‘𝑊))) |
3 | | lencl 14236 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝐴 → (♯‘𝑊) ∈
ℕ0) |
4 | 3 | nn0zd 12424 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝐴 → (♯‘𝑊) ∈ ℤ) |
5 | | fzoval 13388 |
. . . . . . . . . . . 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 2824 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^(♯‘𝑊)) ↔ 𝑥 ∈ (0...((♯‘𝑊) − 1)))) |
9 | 8 | biimpa 477 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → 𝑥 ∈ (0...((♯‘𝑊) − 1))) |
10 | | fznn0sub2 13363 |
. . . . . . . 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 2842 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (((♯‘𝑊) − 1) − 𝑥) ∈
(0..^(♯‘𝑊))) |
14 | | fvco2 6865 |
. . . . . 6
⊢ ((𝑊 Fn (0..^(♯‘𝑊)) ∧ (((♯‘𝑊) − 1) − 𝑥) ∈
(0..^(♯‘𝑊)))
→ ((𝐹 ∘ 𝑊)‘(((♯‘𝑊) − 1) − 𝑥)) = (𝐹‘(𝑊‘(((♯‘𝑊) − 1) − 𝑥)))) |
15 | 2, 13, 14 | syl2anc 584 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((𝐹 ∘ 𝑊)‘(((♯‘𝑊) − 1) − 𝑥)) = (𝐹‘(𝑊‘(((♯‘𝑊) − 1) − 𝑥)))) |
16 | | lenco 14545 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑊)) = (♯‘𝑊)) |
17 | 16 | oveq1d 7290 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → ((♯‘(𝐹 ∘ 𝑊)) − 1) = ((♯‘𝑊) − 1)) |
18 | 17 | oveq1d 7290 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥) = (((♯‘𝑊) − 1) − 𝑥)) |
19 | 18 | adantr 481 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥) = (((♯‘𝑊) − 1) − 𝑥)) |
20 | 19 | fveq2d 6778 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)) = ((𝐹 ∘ 𝑊)‘(((♯‘𝑊) − 1) − 𝑥))) |
21 | | revfv 14476 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘𝑥) = (𝑊‘(((♯‘𝑊) − 1) − 𝑥))) |
22 | 21 | adantlr 712 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘𝑥) = (𝑊‘(((♯‘𝑊) − 1) − 𝑥))) |
23 | 22 | fveq2d 6778 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (𝐹‘((reverse‘𝑊)‘𝑥)) = (𝐹‘(𝑊‘(((♯‘𝑊) − 1) − 𝑥)))) |
24 | 15, 20, 23 | 3eqtr4d 2788 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)) = (𝐹‘((reverse‘𝑊)‘𝑥))) |
25 | 24 | mpteq2dva 5174 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥))) = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ (𝐹‘((reverse‘𝑊)‘𝑥)))) |
26 | 16 | oveq2d 7291 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0..^(♯‘(𝐹 ∘ 𝑊))) = (0..^(♯‘𝑊))) |
27 | 26 | mpteq1d 5169 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑊))) ↦ ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥))) = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)))) |
28 | | revlen 14475 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 → (♯‘(reverse‘𝑊)) = (♯‘𝑊)) |
29 | 28 | adantr 481 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(reverse‘𝑊)) = (♯‘𝑊)) |
30 | 29 | oveq2d 7291 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) →
(0..^(♯‘(reverse‘𝑊))) = (0..^(♯‘𝑊))) |
31 | 30 | mpteq1d 5169 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈
(0..^(♯‘(reverse‘𝑊))) ↦ (𝐹‘((reverse‘𝑊)‘𝑥))) = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ (𝐹‘((reverse‘𝑊)‘𝑥)))) |
32 | 25, 27, 31 | 3eqtr4rd 2789 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈
(0..^(♯‘(reverse‘𝑊))) ↦ (𝐹‘((reverse‘𝑊)‘𝑥))) = (𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑊))) ↦ ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)))) |
33 | | simpr 485 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴⟶𝐵) |
34 | | revcl 14474 |
. . . . 5
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊) ∈ Word 𝐴) |
35 | | wrdf 14222 |
. . . . 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 7005 |
. . 3
⊢ ((𝐹:𝐴⟶𝐵 ∧ (reverse‘𝑊):(0..^(♯‘(reverse‘𝑊)))⟶𝐴) → (𝐹 ∘ (reverse‘𝑊)) = (𝑥 ∈
(0..^(♯‘(reverse‘𝑊))) ↦ (𝐹‘((reverse‘𝑊)‘𝑥)))) |
39 | 33, 37, 38 | syl2anc 584 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (reverse‘𝑊)) = (𝑥 ∈
(0..^(♯‘(reverse‘𝑊))) ↦ (𝐹‘((reverse‘𝑊)‘𝑥)))) |
40 | | ffun 6603 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
41 | | simpl 483 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑊 ∈ Word 𝐴) |
42 | | cofunexg 7791 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝑊 ∈ Word 𝐴) → (𝐹 ∘ 𝑊) ∈ V) |
43 | 40, 41, 42 | syl2an2 683 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ V) |
44 | | revval 14473 |
. . 3
⊢ ((𝐹 ∘ 𝑊) ∈ V → (reverse‘(𝐹 ∘ 𝑊)) = (𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑊))) ↦ ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)))) |
45 | 43, 44 | syl 17 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (reverse‘(𝐹 ∘ 𝑊)) = (𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑊))) ↦ ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)))) |
46 | 32, 39, 45 | 3eqtr4d 2788 |
1
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (reverse‘𝑊)) = (reverse‘(𝐹 ∘ 𝑊))) |