Step | Hyp | Ref
| Expression |
1 | | ffn 5958 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
2 | 1 | 3ad2ant3 1077 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝐹 Fn 𝐴) |
3 | | swrdvalfn 13278 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
4 | 3 | 3expb 1258 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊)))) → (𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
5 | 4 | 3adant3 1074 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
6 | | swrdrn 13281 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ 𝐴) |
7 | 6 | 3expb 1258 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊)))) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ 𝐴) |
8 | 7 | 3adant3 1074 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ 𝐴) |
9 | | fnco 5913 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ (𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀)) ∧ ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ 𝐴) → (𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉)) Fn (0..^(𝑁 − 𝑀))) |
10 | 2, 5, 8, 9 | syl3anc 1318 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉)) Fn (0..^(𝑁 − 𝑀))) |
11 | | wrdco 13428 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) |
12 | 11 | 3adant2 1073 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) |
13 | | simp2l 1080 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝑀 ∈ (0...𝑁)) |
14 | | lenco 13429 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘(𝐹 ∘ 𝑊)) = (#‘𝑊)) |
15 | 14 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘𝑊) = (#‘(𝐹 ∘ 𝑊))) |
16 | 15 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0...(#‘𝑊)) = (0...(#‘(𝐹 ∘ 𝑊)))) |
17 | 16 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑁 ∈ (0...(#‘𝑊)) ↔ 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊))))) |
18 | 17 | biimpd 218 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑁 ∈ (0...(#‘𝑊)) → 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊))))) |
19 | 18 | expcom 450 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → (𝑊 ∈ Word 𝐴 → (𝑁 ∈ (0...(#‘𝑊)) → 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊)))))) |
20 | 19 | com13 86 |
. . . . . 6
⊢ (𝑁 ∈ (0...(#‘𝑊)) → (𝑊 ∈ Word 𝐴 → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊)))))) |
21 | 20 | adantl 481 |
. . . . 5
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝑊 ∈ Word 𝐴 → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊)))))) |
22 | 21 | com12 32 |
. . . 4
⊢ (𝑊 ∈ Word 𝐴 → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊)))))) |
23 | 22 | 3imp 1249 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊)))) |
24 | | swrdvalfn 13278 |
. . 3
⊢ (((𝐹 ∘ 𝑊) ∈ Word 𝐵 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊)))) → ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
25 | 12, 13, 23, 24 | syl3anc 1318 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
26 | | 3anass 1035 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ↔ (𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))))) |
27 | 26 | biimpri 217 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊)))) → (𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊)))) |
28 | 27 | 3adant3 1074 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊)))) |
29 | | swrdfv 13276 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖) = (𝑊‘(𝑖 + 𝑀))) |
30 | 29 | fveq2d 6107 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖)) = (𝐹‘(𝑊‘(𝑖 + 𝑀)))) |
31 | 28, 30 | sylan 487 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖)) = (𝐹‘(𝑊‘(𝑖 + 𝑀)))) |
32 | | wrdfn 13174 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐴 → 𝑊 Fn (0..^(#‘𝑊))) |
33 | 32 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝑊 Fn (0..^(#‘𝑊))) |
34 | 33 | adantr 480 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → 𝑊 Fn (0..^(#‘𝑊))) |
35 | | elfzodifsumelfzo 12401 |
. . . . . . 7
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝑖 ∈ (0..^(𝑁 − 𝑀)) → (𝑖 + 𝑀) ∈ (0..^(#‘𝑊)))) |
36 | 35 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝑖 ∈ (0..^(𝑁 − 𝑀)) → (𝑖 + 𝑀) ∈ (0..^(#‘𝑊)))) |
37 | 36 | imp 444 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝑖 + 𝑀) ∈ (0..^(#‘𝑊))) |
38 | | fvco2 6183 |
. . . . 5
⊢ ((𝑊 Fn (0..^(#‘𝑊)) ∧ (𝑖 + 𝑀) ∈ (0..^(#‘𝑊))) → ((𝐹 ∘ 𝑊)‘(𝑖 + 𝑀)) = (𝐹‘(𝑊‘(𝑖 + 𝑀)))) |
39 | 34, 37, 38 | syl2anc 691 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝐹 ∘ 𝑊)‘(𝑖 + 𝑀)) = (𝐹‘(𝑊‘(𝑖 + 𝑀)))) |
40 | 31, 39 | eqtr4d 2647 |
. . 3
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖)) = ((𝐹 ∘ 𝑊)‘(𝑖 + 𝑀))) |
41 | | fvco2 6183 |
. . . 4
⊢ (((𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀)) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉))‘𝑖) = (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖))) |
42 | 5, 41 | sylan 487 |
. . 3
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉))‘𝑖) = (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖))) |
43 | 14 | ancoms 468 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (#‘(𝐹 ∘ 𝑊)) = (#‘𝑊)) |
44 | 43 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (#‘𝑊) = (#‘(𝐹 ∘ 𝑊))) |
45 | 44 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (0...(#‘𝑊)) = (0...(#‘(𝐹 ∘ 𝑊)))) |
46 | 45 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (𝑁 ∈ (0...(#‘𝑊)) ↔ 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊))))) |
47 | 46 | biimpd 218 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (𝑁 ∈ (0...(#‘𝑊)) → 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊))))) |
48 | 47 | ex 449 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → (𝑊 ∈ Word 𝐴 → (𝑁 ∈ (0...(#‘𝑊)) → 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊)))))) |
49 | 48 | com13 86 |
. . . . . . . 8
⊢ (𝑁 ∈ (0...(#‘𝑊)) → (𝑊 ∈ Word 𝐴 → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊)))))) |
50 | 49 | adantl 481 |
. . . . . . 7
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝑊 ∈ Word 𝐴 → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊)))))) |
51 | 50 | com12 32 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊)))))) |
52 | 51 | 3imp 1249 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊)))) |
53 | 12, 13, 52 | 3jca 1235 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑊) ∈ Word 𝐵 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊))))) |
54 | | swrdfv 13276 |
. . . 4
⊢ ((((𝐹 ∘ 𝑊) ∈ Word 𝐵 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘(𝐹 ∘ 𝑊)))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)‘𝑖) = ((𝐹 ∘ 𝑊)‘(𝑖 + 𝑀))) |
55 | 53, 54 | sylan 487 |
. . 3
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)‘𝑖) = ((𝐹 ∘ 𝑊)‘(𝑖 + 𝑀))) |
56 | 40, 42, 55 | 3eqtr4d 2654 |
. 2
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉))‘𝑖) = (((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)‘𝑖)) |
57 | 10, 25, 56 | eqfnfvd 6222 |
1
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉)) = ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)) |