![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > swrdfv | Structured version Visualization version GIF version |
Description: A symbol in an extracted subword, indexed using the subword's indices. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
Ref | Expression |
---|---|
swrdfv | ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) ∧ 𝑋 ∈ (0..^(𝐿 − 𝐹))) → ((𝑆 substr 〈𝐹, 𝐿〉)‘𝑋) = (𝑆‘(𝑋 + 𝐹))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | swrdval2 13674 | . . 3 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 substr 〈𝐹, 𝐿〉) = (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹)))) | |
2 | 1 | fveq1d 6417 | . 2 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → ((𝑆 substr 〈𝐹, 𝐿〉)‘𝑋) = ((𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹)))‘𝑋)) |
3 | fvoveq1 6905 | . . 3 ⊢ (𝑥 = 𝑋 → (𝑆‘(𝑥 + 𝐹)) = (𝑆‘(𝑋 + 𝐹))) | |
4 | eqid 2803 | . . 3 ⊢ (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))) = (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))) | |
5 | fvex 6428 | . . 3 ⊢ (𝑆‘(𝑋 + 𝐹)) ∈ V | |
6 | 3, 4, 5 | fvmpt 6511 | . 2 ⊢ (𝑋 ∈ (0..^(𝐿 − 𝐹)) → ((𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹)))‘𝑋) = (𝑆‘(𝑋 + 𝐹))) |
7 | 2, 6 | sylan9eq 2857 | 1 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) ∧ 𝑋 ∈ (0..^(𝐿 − 𝐹))) → ((𝑆 substr 〈𝐹, 𝐿〉)‘𝑋) = (𝑆‘(𝑋 + 𝐹))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 〈cop 4378 ↦ cmpt 4926 ‘cfv 6105 (class class class)co 6882 0cc0 10228 + caddc 10231 − cmin 10560 ...cfz 12584 ..^cfzo 12724 ♯chash 13374 Word cword 13538 substr csubstr 13668 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2379 ax-ext 2781 ax-rep 4968 ax-sep 4979 ax-nul 4987 ax-pow 5039 ax-pr 5101 ax-un 7187 ax-cnex 10284 ax-resscn 10285 ax-1cn 10286 ax-icn 10287 ax-addcl 10288 ax-addrcl 10289 ax-mulcl 10290 ax-mulrcl 10291 ax-mulcom 10292 ax-addass 10293 ax-mulass 10294 ax-distr 10295 ax-i2m1 10296 ax-1ne0 10297 ax-1rid 10298 ax-rnegex 10299 ax-rrecex 10300 ax-cnre 10301 ax-pre-lttri 10302 ax-pre-lttrn 10303 ax-pre-ltadd 10304 ax-pre-mulgt0 10305 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2593 df-eu 2611 df-clab 2790 df-cleq 2796 df-clel 2799 df-nfc 2934 df-ne 2976 df-nel 3079 df-ral 3098 df-rex 3099 df-reu 3100 df-rab 3102 df-v 3391 df-sbc 3638 df-csb 3733 df-dif 3776 df-un 3778 df-in 3780 df-ss 3787 df-pss 3789 df-nul 4120 df-if 4282 df-pw 4355 df-sn 4373 df-pr 4375 df-tp 4377 df-op 4379 df-uni 4633 df-int 4672 df-iun 4716 df-br 4848 df-opab 4910 df-mpt 4927 df-tr 4950 df-id 5224 df-eprel 5229 df-po 5237 df-so 5238 df-fr 5275 df-we 5277 df-xp 5322 df-rel 5323 df-cnv 5324 df-co 5325 df-dm 5326 df-rn 5327 df-res 5328 df-ima 5329 df-pred 5902 df-ord 5948 df-on 5949 df-lim 5950 df-suc 5951 df-iota 6068 df-fun 6107 df-fn 6108 df-f 6109 df-f1 6110 df-fo 6111 df-f1o 6112 df-fv 6113 df-riota 6843 df-ov 6885 df-oprab 6886 df-mpt2 6887 df-om 7304 df-1st 7405 df-2nd 7406 df-wrecs 7649 df-recs 7711 df-rdg 7749 df-1o 7803 df-er 7986 df-en 8200 df-dom 8201 df-sdom 8202 df-fin 8203 df-card 9055 df-pnf 10369 df-mnf 10370 df-xr 10371 df-ltxr 10372 df-le 10373 df-sub 10562 df-neg 10563 df-nn 11317 df-n0 11585 df-z 11671 df-uz 11935 df-fz 12585 df-fzo 12725 df-hash 13375 df-word 13539 df-substr 13669 |
This theorem is referenced by: swrdfv0 13679 swrdidOLD 13683 swrd0fvOLD 13696 swrdfv2 13703 swrds1 13709 ccatswrd 13714 swrdccat2 13716 pfxfv 13729 ccatpfx 13748 swrdswrd 13752 swrdccatin1 13789 swrdccatin2 13794 pfxccatin12lem2 13796 swrdccatin12lem2OLD 13797 swrdccatin12lem3 13798 splfv1OLD 13837 cshwidxmod 13892 swrdco 13926 |
Copyright terms: Public domain | W3C validator |