Step | Hyp | Ref
| Expression |
1 | | wrdfn 13971 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐴 → 𝑊 Fn (0..^(♯‘𝑊))) |
2 | 1 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → 𝑊 Fn (0..^(♯‘𝑊))) |
3 | | lencl 13976 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝐴 → (♯‘𝑊) ∈
ℕ0) |
4 | 3 | nn0zd 12168 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝐴 → (♯‘𝑊) ∈ ℤ) |
5 | | fzoval 13132 |
. . . . . . . . . . . 12
⊢
((♯‘𝑊)
∈ ℤ → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐴 → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
7 | 6 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
8 | 7 | eleq2d 2818 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^(♯‘𝑊)) ↔ 𝑥 ∈ (0...((♯‘𝑊) − 1)))) |
9 | 8 | biimpa 480 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → 𝑥 ∈ (0...((♯‘𝑊) − 1))) |
10 | | fznn0sub2 13107 |
. . . . . . . 8
⊢ (𝑥 ∈
(0...((♯‘𝑊)
− 1)) → (((♯‘𝑊) − 1) − 𝑥) ∈ (0...((♯‘𝑊) − 1))) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (((♯‘𝑊) − 1) − 𝑥) ∈
(0...((♯‘𝑊)
− 1))) |
12 | 7 | adantr 484 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
13 | 11, 12 | eleqtrrd 2836 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (((♯‘𝑊) − 1) − 𝑥) ∈
(0..^(♯‘𝑊))) |
14 | | fvco2 6767 |
. . . . . 6
⊢ ((𝑊 Fn (0..^(♯‘𝑊)) ∧ (((♯‘𝑊) − 1) − 𝑥) ∈
(0..^(♯‘𝑊)))
→ ((𝐹 ∘ 𝑊)‘(((♯‘𝑊) − 1) − 𝑥)) = (𝐹‘(𝑊‘(((♯‘𝑊) − 1) − 𝑥)))) |
15 | 2, 13, 14 | syl2anc 587 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((𝐹 ∘ 𝑊)‘(((♯‘𝑊) − 1) − 𝑥)) = (𝐹‘(𝑊‘(((♯‘𝑊) − 1) − 𝑥)))) |
16 | | lenco 14285 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑊)) = (♯‘𝑊)) |
17 | 16 | oveq1d 7187 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → ((♯‘(𝐹 ∘ 𝑊)) − 1) = ((♯‘𝑊) − 1)) |
18 | 17 | oveq1d 7187 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥) = (((♯‘𝑊) − 1) − 𝑥)) |
19 | 18 | adantr 484 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥) = (((♯‘𝑊) − 1) − 𝑥)) |
20 | 19 | fveq2d 6680 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)) = ((𝐹 ∘ 𝑊)‘(((♯‘𝑊) − 1) − 𝑥))) |
21 | | revfv 14216 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘𝑥) = (𝑊‘(((♯‘𝑊) − 1) − 𝑥))) |
22 | 21 | adantlr 715 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘𝑥) = (𝑊‘(((♯‘𝑊) − 1) − 𝑥))) |
23 | 22 | fveq2d 6680 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (𝐹‘((reverse‘𝑊)‘𝑥)) = (𝐹‘(𝑊‘(((♯‘𝑊) − 1) − 𝑥)))) |
24 | 15, 20, 23 | 3eqtr4d 2783 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)) = (𝐹‘((reverse‘𝑊)‘𝑥))) |
25 | 24 | mpteq2dva 5125 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥))) = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ (𝐹‘((reverse‘𝑊)‘𝑥)))) |
26 | 16 | oveq2d 7188 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0..^(♯‘(𝐹 ∘ 𝑊))) = (0..^(♯‘𝑊))) |
27 | 26 | mpteq1d 5119 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑊))) ↦ ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥))) = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)))) |
28 | | revlen 14215 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 → (♯‘(reverse‘𝑊)) = (♯‘𝑊)) |
29 | 28 | adantr 484 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(reverse‘𝑊)) = (♯‘𝑊)) |
30 | 29 | oveq2d 7188 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) →
(0..^(♯‘(reverse‘𝑊))) = (0..^(♯‘𝑊))) |
31 | 30 | mpteq1d 5119 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈
(0..^(♯‘(reverse‘𝑊))) ↦ (𝐹‘((reverse‘𝑊)‘𝑥))) = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ (𝐹‘((reverse‘𝑊)‘𝑥)))) |
32 | 25, 27, 31 | 3eqtr4rd 2784 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈
(0..^(♯‘(reverse‘𝑊))) ↦ (𝐹‘((reverse‘𝑊)‘𝑥))) = (𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑊))) ↦ ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)))) |
33 | | simpr 488 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴⟶𝐵) |
34 | | revcl 14214 |
. . . . 5
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊) ∈ Word 𝐴) |
35 | | wrdf 13962 |
. . . . 5
⊢
((reverse‘𝑊)
∈ Word 𝐴 →
(reverse‘𝑊):(0..^(♯‘(reverse‘𝑊)))⟶𝐴) |
36 | 34, 35 | syl 17 |
. . . 4
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊):(0..^(♯‘(reverse‘𝑊)))⟶𝐴) |
37 | 36 | adantr 484 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (reverse‘𝑊):(0..^(♯‘(reverse‘𝑊)))⟶𝐴) |
38 | | fcompt 6907 |
. . 3
⊢ ((𝐹:𝐴⟶𝐵 ∧ (reverse‘𝑊):(0..^(♯‘(reverse‘𝑊)))⟶𝐴) → (𝐹 ∘ (reverse‘𝑊)) = (𝑥 ∈
(0..^(♯‘(reverse‘𝑊))) ↦ (𝐹‘((reverse‘𝑊)‘𝑥)))) |
39 | 33, 37, 38 | syl2anc 587 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (reverse‘𝑊)) = (𝑥 ∈
(0..^(♯‘(reverse‘𝑊))) ↦ (𝐹‘((reverse‘𝑊)‘𝑥)))) |
40 | | ffun 6507 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
41 | | simpl 486 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑊 ∈ Word 𝐴) |
42 | | cofunexg 7677 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝑊 ∈ Word 𝐴) → (𝐹 ∘ 𝑊) ∈ V) |
43 | 40, 41, 42 | syl2an2 686 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ V) |
44 | | revval 14213 |
. . 3
⊢ ((𝐹 ∘ 𝑊) ∈ V → (reverse‘(𝐹 ∘ 𝑊)) = (𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑊))) ↦ ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)))) |
45 | 43, 44 | syl 17 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (reverse‘(𝐹 ∘ 𝑊)) = (𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑊))) ↦ ((𝐹 ∘ 𝑊)‘(((♯‘(𝐹 ∘ 𝑊)) − 1) − 𝑥)))) |
46 | 32, 39, 45 | 3eqtr4d 2783 |
1
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (reverse‘𝑊)) = (reverse‘(𝐹 ∘ 𝑊))) |