| Step | Hyp | Ref
| Expression |
| 1 | | ffn 6736 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
| 2 | 1 | 3ad2ant3 1136 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝐹 Fn 𝐴) |
| 3 | | swrdvalfn 14689 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
| 4 | 3 | 3expb 1121 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) → (𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
| 5 | 4 | 3adant3 1133 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
| 6 | | swrdrn 14690 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ 𝐴) |
| 7 | 6 | 3expb 1121 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ 𝐴) |
| 8 | 7 | 3adant3 1133 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ 𝐴) |
| 9 | | fnco 6686 |
. . 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 14870 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) |
| 12 | 11 | 3adant2 1132 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) |
| 13 | | simp2l 1200 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝑀 ∈ (0...𝑁)) |
| 14 | | lenco 14871 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑊)) = (♯‘𝑊)) |
| 15 | 14 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘𝑊) = (♯‘(𝐹 ∘ 𝑊))) |
| 16 | 15 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0...(♯‘𝑊)) = (0...(♯‘(𝐹 ∘ 𝑊)))) |
| 17 | 16 | eleq2d 2827 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊))))) |
| 18 | 17 | biimpd 229 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑁 ∈ (0...(♯‘𝑊)) → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊))))) |
| 19 | 18 | expcom 413 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → (𝑊 ∈ Word 𝐴 → (𝑁 ∈ (0...(♯‘𝑊)) → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))))) |
| 20 | 19 | com13 88 |
. . . . 5
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ (𝑊 ∈ Word 𝐴 → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))))) |
| 21 | 20 | adantl 481 |
. . . 4
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 ∈ Word 𝐴 → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))))) |
| 22 | 21 | 3imp21 1114 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))) |
| 23 | | swrdvalfn 14689 |
. . 3
⊢ (((𝐹 ∘ 𝑊) ∈ Word 𝐵 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))) → ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
| 24 | 12, 13, 22, 23 | syl3anc 1373 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
| 25 | | 3anass 1095 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ↔ (𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))))) |
| 26 | 25 | biimpri 228 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) → (𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) |
| 27 | 26 | 3adant3 1133 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) |
| 28 | | swrdfv 14686 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖) = (𝑊‘(𝑖 + 𝑀))) |
| 29 | 28 | fveq2d 6910 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖)) = (𝐹‘(𝑊‘(𝑖 + 𝑀)))) |
| 30 | 27, 29 | sylan 580 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖)) = (𝐹‘(𝑊‘(𝑖 + 𝑀)))) |
| 31 | | wrdfn 14566 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 → 𝑊 Fn (0..^(♯‘𝑊))) |
| 32 | 31 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝑊 Fn (0..^(♯‘𝑊))) |
| 33 | | elfzodifsumelfzo 13770 |
. . . . . . 7
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑖 ∈ (0..^(𝑁 − 𝑀)) → (𝑖 + 𝑀) ∈ (0..^(♯‘𝑊)))) |
| 34 | 33 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝑖 ∈ (0..^(𝑁 − 𝑀)) → (𝑖 + 𝑀) ∈ (0..^(♯‘𝑊)))) |
| 35 | 34 | imp 406 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝑖 + 𝑀) ∈ (0..^(♯‘𝑊))) |
| 36 | | fvco2 7006 |
. . . . 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 7006 |
. . . 4
⊢ (((𝑊 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀)) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉))‘𝑖) = (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖))) |
| 40 | 5, 39 | sylan 580 |
. . 3
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉))‘𝑖) = (𝐹‘((𝑊 substr 〈𝑀, 𝑁〉)‘𝑖))) |
| 41 | 14 | ancoms 458 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (♯‘(𝐹 ∘ 𝑊)) = (♯‘𝑊)) |
| 42 | 41 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (♯‘𝑊) = (♯‘(𝐹 ∘ 𝑊))) |
| 43 | 42 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (0...(♯‘𝑊)) = (0...(♯‘(𝐹 ∘ 𝑊)))) |
| 44 | 43 | eleq2d 2827 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊))))) |
| 45 | 44 | biimpd 229 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊 ∈ Word 𝐴) → (𝑁 ∈ (0...(♯‘𝑊)) → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊))))) |
| 46 | 45 | ex 412 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → (𝑊 ∈ Word 𝐴 → (𝑁 ∈ (0...(♯‘𝑊)) → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))))) |
| 47 | 46 | com13 88 |
. . . . . . 7
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ (𝑊 ∈ Word 𝐴 → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))))) |
| 48 | 47 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 ∈ Word 𝐴 → (𝐹:𝐴⟶𝐵 → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))))) |
| 49 | 48 | 3imp21 1114 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))) |
| 50 | 12, 13, 49 | 3jca 1129 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑊) ∈ Word 𝐵 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊))))) |
| 51 | | swrdfv 14686 |
. . . 4
⊢ ((((𝐹 ∘ 𝑊) ∈ Word 𝐵 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐹 ∘ 𝑊)))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)‘𝑖) = ((𝐹 ∘ 𝑊)‘(𝑖 + 𝑀))) |
| 52 | 50, 51 | sylan 580 |
. . 3
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)‘𝑖) = ((𝐹 ∘ 𝑊)‘(𝑖 + 𝑀))) |
| 53 | 38, 40, 52 | 3eqtr4d 2787 |
. 2
⊢ (((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉))‘𝑖) = (((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)‘𝑖)) |
| 54 | 10, 24, 53 | eqfnfvd 7054 |
1
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉)) = ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)) |