![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pfxfv | Structured version Visualization version GIF version |
Description: A symbol in a prefix of a word, indexed using the prefix' indices. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (Revised by AV, 3-May-2020.) |
Ref | Expression |
---|---|
pfxfv | ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘𝐼) = (𝑊‘𝐼)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfznn0 13571 | . . . . 5 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → 𝐿 ∈ ℕ0) | |
2 | pfxval 14600 | . . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑊 prefix 𝐿) = (𝑊 substr 〈0, 𝐿〉)) | |
3 | 1, 2 | sylan2 593 | . . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝑊 prefix 𝐿) = (𝑊 substr 〈0, 𝐿〉)) |
4 | 3 | 3adant3 1132 | . . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → (𝑊 prefix 𝐿) = (𝑊 substr 〈0, 𝐿〉)) |
5 | 4 | fveq1d 6875 | . 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘𝐼) = ((𝑊 substr 〈0, 𝐿〉)‘𝐼)) |
6 | simp1 1136 | . . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → 𝑊 ∈ Word 𝑉) | |
7 | 0elfz 13575 | . . . . 5 ⊢ (𝐿 ∈ ℕ0 → 0 ∈ (0...𝐿)) | |
8 | 1, 7 | syl 17 | . . . 4 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → 0 ∈ (0...𝐿)) |
9 | 8 | 3ad2ant2 1134 | . . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → 0 ∈ (0...𝐿)) |
10 | simp2 1137 | . . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → 𝐿 ∈ (0...(♯‘𝑊))) | |
11 | 1 | nn0cnd 12511 | . . . . . . . . . 10 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → 𝐿 ∈ ℂ) |
12 | 11 | subid1d 11537 | . . . . . . . . 9 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → (𝐿 − 0) = 𝐿) |
13 | 12 | eqcomd 2737 | . . . . . . . 8 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → 𝐿 = (𝐿 − 0)) |
14 | 13 | oveq2d 7404 | . . . . . . 7 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → (0..^𝐿) = (0..^(𝐿 − 0))) |
15 | 14 | eleq2d 2818 | . . . . . 6 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → (𝐼 ∈ (0..^𝐿) ↔ 𝐼 ∈ (0..^(𝐿 − 0)))) |
16 | 15 | biimpd 228 | . . . . 5 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → (𝐼 ∈ (0..^𝐿) → 𝐼 ∈ (0..^(𝐿 − 0)))) |
17 | 16 | a1i 11 | . . . 4 ⊢ (𝑊 ∈ Word 𝑉 → (𝐿 ∈ (0...(♯‘𝑊)) → (𝐼 ∈ (0..^𝐿) → 𝐼 ∈ (0..^(𝐿 − 0))))) |
18 | 17 | 3imp 1111 | . . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → 𝐼 ∈ (0..^(𝐿 − 0))) |
19 | swrdfv 14575 | . . 3 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 0 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) ∧ 𝐼 ∈ (0..^(𝐿 − 0))) → ((𝑊 substr 〈0, 𝐿〉)‘𝐼) = (𝑊‘(𝐼 + 0))) | |
20 | 6, 9, 10, 18, 19 | syl31anc 1373 | . 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → ((𝑊 substr 〈0, 𝐿〉)‘𝐼) = (𝑊‘(𝐼 + 0))) |
21 | elfzoelz 13609 | . . . . . 6 ⊢ (𝐼 ∈ (0..^𝐿) → 𝐼 ∈ ℤ) | |
22 | 21 | zcnd 12644 | . . . . 5 ⊢ (𝐼 ∈ (0..^𝐿) → 𝐼 ∈ ℂ) |
23 | 22 | addridd 11391 | . . . 4 ⊢ (𝐼 ∈ (0..^𝐿) → (𝐼 + 0) = 𝐼) |
24 | 23 | 3ad2ant3 1135 | . . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → (𝐼 + 0) = 𝐼) |
25 | 24 | fveq2d 6877 | . 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → (𝑊‘(𝐼 + 0)) = (𝑊‘𝐼)) |
26 | 5, 20, 25 | 3eqtrd 2775 | 1 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘𝐼) = (𝑊‘𝐼)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 〈cop 4623 ‘cfv 6527 (class class class)co 7388 0cc0 11087 + caddc 11090 − cmin 11421 ℕ0cn0 12449 ...cfz 13461 ..^cfzo 13604 ♯chash 14267 Word cword 14441 substr csubstr 14567 prefix cpfx 14597 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5273 ax-sep 5287 ax-nul 5294 ax-pow 5351 ax-pr 5415 ax-un 7703 ax-cnex 11143 ax-resscn 11144 ax-1cn 11145 ax-icn 11146 ax-addcl 11147 ax-addrcl 11148 ax-mulcl 11149 ax-mulrcl 11150 ax-mulcom 11151 ax-addass 11152 ax-mulass 11153 ax-distr 11154 ax-i2m1 11155 ax-1ne0 11156 ax-1rid 11157 ax-rnegex 11158 ax-rrecex 11159 ax-cnre 11160 ax-pre-lttri 11161 ax-pre-lttrn 11162 ax-pre-ltadd 11163 ax-pre-mulgt0 11164 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3375 df-rab 3429 df-v 3471 df-sbc 3769 df-csb 3885 df-dif 3942 df-un 3944 df-in 3946 df-ss 3956 df-pss 3958 df-nul 4314 df-if 4518 df-pw 4593 df-sn 4618 df-pr 4620 df-op 4624 df-uni 4897 df-int 4939 df-iun 4987 df-br 5137 df-opab 5199 df-mpt 5220 df-tr 5254 df-id 5562 df-eprel 5568 df-po 5576 df-so 5577 df-fr 5619 df-we 5621 df-xp 5670 df-rel 5671 df-cnv 5672 df-co 5673 df-dm 5674 df-rn 5675 df-res 5676 df-ima 5677 df-pred 6284 df-ord 6351 df-on 6352 df-lim 6353 df-suc 6354 df-iota 6479 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-riota 7344 df-ov 7391 df-oprab 7392 df-mpo 7393 df-om 7834 df-1st 7952 df-2nd 7953 df-frecs 8243 df-wrecs 8274 df-recs 8348 df-rdg 8387 df-1o 8443 df-er 8681 df-en 8918 df-dom 8919 df-sdom 8920 df-fin 8921 df-card 9911 df-pnf 11227 df-mnf 11228 df-xr 11229 df-ltxr 11230 df-le 11231 df-sub 11423 df-neg 11424 df-nn 12190 df-n0 12450 df-z 12536 df-uz 12800 df-fz 13462 df-fzo 13605 df-hash 14268 df-word 14442 df-substr 14568 df-pfx 14598 |
This theorem is referenced by: pfxid 14611 pfxfv0 14619 pfxtrcfv 14620 pfxfvlsw 14622 pfxeq 14623 ccatpfx 14628 pfxccatin12lem2 14658 splfv1 14682 repswpfx 14712 cshwidxmod 14730 pfx2 14875 wwlksm1edg 28946 wwlksnred 28957 clwwlkinwwlk 29104 clwwlkf 29111 wwlksubclwwlk 29122 dlwwlknondlwlknonf1olem1 29428 cycpmco2 32109 revpfxsfxrev 33872 |
Copyright terms: Public domain | W3C validator |