Step | Hyp | Ref
| Expression |
1 | | ffn 6545 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
2 | 1 | 3ad2ant3 1137 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝐹 Fn 𝐴) |
3 | | swrdvalfn 14216 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
4 | 3 | 3expb 1122 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) → (𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
5 | 4 | 3adant3 1134 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
6 | | swrdrn 14217 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ 𝐴) |
7 | 6 | 3expb 1122 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ 𝐴) |
8 | 7 | 3adant3 1134 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ 𝐴) |
9 | | fnco 6494 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ (𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀)) ∧ ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ 𝐴) → (𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉)) Fn (0..^(𝑁 − 𝑀))) |
10 | 2, 5, 8, 9 | syl3anc 1373 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉)) Fn (0..^(𝑁 − 𝑀))) |
11 | | wrdco 14396 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) |
12 | 11 | 3adant2 1133 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) |
13 | | simp2l 1201 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝑀 ∈ (0...𝑁)) |
14 | | lenco 14397 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑊)) = (♯‘𝑊)) |
15 | 14 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘𝑊) = (♯‘(𝐹 ∘ 𝑊))) |
16 | 15 | oveq2d 7229 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0...(♯‘𝑊)) = (0...(♯‘(𝐹 ∘ 𝑊)))) |
17 | 16 | eleq2d 2823 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊))))) |
18 | 17 | biimpd 232 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑁 ∈ (0...(♯‘𝑊)) → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊))))) |
19 | 18 | expcom 417 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → (𝑊 ∈ Word 𝐴 → (𝑁 ∈ (0...(♯‘𝑊)) → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))))) |
20 | 19 | com13 88 |
. . . . 5
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ (𝑊 ∈ Word 𝐴 → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))))) |
21 | 20 | adantl 485 |
. . . 4
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 ∈ Word 𝐴 → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))))) |
22 | 21 | 3imp21 1116 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))) |
23 | | swrdvalfn 14216 |
. . 3
⊢ (((𝐹 ∘ 𝑊) ∈ Word 𝐵 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))) → ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
24 | 12, 13, 22, 23 | syl3anc 1373 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
25 | | 3anass 1097 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ↔ (𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))))) |
26 | 25 | biimpri 231 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) → (𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) |
27 | 26 | 3adant3 1134 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) |
28 | | swrdfv 14213 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖) = (𝑊‘(𝑖 + 𝑀))) |
29 | 28 | fveq2d 6721 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖)) = (𝐹‘(𝑊‘(𝑖 + 𝑀)))) |
30 | 27, 29 | sylan 583 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖)) = (𝐹‘(𝑊‘(𝑖 + 𝑀)))) |
31 | | wrdfn 14083 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 → 𝑊 Fn (0..^(♯‘𝑊))) |
32 | 31 | 3ad2ant1 1135 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝑊 Fn (0..^(♯‘𝑊))) |
33 | | elfzodifsumelfzo 13308 |
. . . . . . 7
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑖 ∈ (0..^(𝑁 − 𝑀)) → (𝑖 + 𝑀) ∈ (0..^(♯‘𝑊)))) |
34 | 33 | 3ad2ant2 1136 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝑖 ∈ (0..^(𝑁 − 𝑀)) → (𝑖 + 𝑀) ∈ (0..^(♯‘𝑊)))) |
35 | 34 | imp 410 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝑖 + 𝑀) ∈ (0..^(♯‘𝑊))) |
36 | | fvco2 6808 |
. . . . 5
⊢ ((𝑊 Fn (0..^(♯‘𝑊)) ∧ (𝑖 + 𝑀) ∈ (0..^(♯‘𝑊))) → ((𝐹 ∘ 𝑊)‘(𝑖 + 𝑀)) = (𝐹‘(𝑊‘(𝑖 + 𝑀)))) |
37 | 32, 35, 36 | syl2an2r 685 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝐹 ∘ 𝑊)‘(𝑖 + 𝑀)) = (𝐹‘(𝑊‘(𝑖 + 𝑀)))) |
38 | 30, 37 | eqtr4d 2780 |
. . 3
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖)) = ((𝐹 ∘ 𝑊)‘(𝑖 + 𝑀))) |
39 | | fvco2 6808 |
. . . 4
⊢ (((𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀)) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉))‘𝑖) = (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖))) |
40 | 5, 39 | sylan 583 |
. . 3
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉))‘𝑖) = (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖))) |
41 | 14 | ancoms 462 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (♯‘(𝐹 ∘ 𝑊)) = (♯‘𝑊)) |
42 | 41 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (♯‘𝑊) = (♯‘(𝐹 ∘ 𝑊))) |
43 | 42 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (0...(♯‘𝑊)) = (0...(♯‘(𝐹 ∘ 𝑊)))) |
44 | 43 | eleq2d 2823 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊))))) |
45 | 44 | biimpd 232 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (𝑁 ∈ (0...(♯‘𝑊)) → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊))))) |
46 | 45 | ex 416 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → (𝑊 ∈ Word 𝐴 → (𝑁 ∈ (0...(♯‘𝑊)) → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))))) |
47 | 46 | com13 88 |
. . . . . . 7
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ (𝑊 ∈ Word 𝐴 → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))))) |
48 | 47 | adantl 485 |
. . . . . 6
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 ∈ Word 𝐴 → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))))) |
49 | 48 | 3imp21 1116 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))) |
50 | 12, 13, 49 | 3jca 1130 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑊) ∈ Word 𝐵 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊))))) |
51 | | swrdfv 14213 |
. . . 4
⊢ ((((𝐹 ∘ 𝑊) ∈ Word 𝐵 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)‘𝑖) = ((𝐹 ∘ 𝑊)‘(𝑖 + 𝑀))) |
52 | 50, 51 | sylan 583 |
. . 3
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)‘𝑖) = ((𝐹 ∘ 𝑊)‘(𝑖 + 𝑀))) |
53 | 38, 40, 52 | 3eqtr4d 2787 |
. 2
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉))‘𝑖) = (((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)‘𝑖)) |
54 | 10, 24, 53 | eqfnfvd 6855 |
1
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉)) = ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)) |