![]() |
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 13573 | . . . . 5 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → 𝐿 ∈ ℕ0) | |
2 | pfxval 14602 | . . . . 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 6877 | . 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘𝐼) = ((𝑊 substr 〈0, 𝐿〉)‘𝐼)) |
6 | simp1 1136 | . . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → 𝑊 ∈ Word 𝑉) | |
7 | 0elfz 13577 | . . . . 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 12513 | . . . . . . . . . 10 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → 𝐿 ∈ ℂ) |
12 | 11 | subid1d 11539 | . . . . . . . . 9 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → (𝐿 − 0) = 𝐿) |
13 | 12 | eqcomd 2737 | . . . . . . . 8 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → 𝐿 = (𝐿 − 0)) |
14 | 13 | oveq2d 7406 | . . . . . . 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 14577 | . . 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 13611 | . . . . . 6 ⊢ (𝐼 ∈ (0..^𝐿) → 𝐼 ∈ ℤ) | |
22 | 21 | zcnd 12646 | . . . . 5 ⊢ (𝐼 ∈ (0..^𝐿) → 𝐼 ∈ ℂ) |
23 | 22 | addridd 11393 | . . . 4 ⊢ (𝐼 ∈ (0..^𝐿) → (𝐼 + 0) = 𝐼) |
24 | 23 | 3ad2ant3 1135 | . . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → (𝐼 + 0) = 𝐼) |
25 | 24 | fveq2d 6879 | . 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 4625 ‘cfv 6529 (class class class)co 7390 0cc0 11089 + caddc 11092 − cmin 11423 ℕ0cn0 12451 ...cfz 13463 ..^cfzo 13606 ♯chash 14269 Word cword 14443 substr csubstr 14569 prefix cpfx 14599 |
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 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7705 ax-cnex 11145 ax-resscn 11146 ax-1cn 11147 ax-icn 11148 ax-addcl 11149 ax-addrcl 11150 ax-mulcl 11151 ax-mulrcl 11152 ax-mulcom 11153 ax-addass 11154 ax-mulass 11155 ax-distr 11156 ax-i2m1 11157 ax-1ne0 11158 ax-1rid 11159 ax-rnegex 11160 ax-rrecex 11161 ax-cnre 11162 ax-pre-lttri 11163 ax-pre-lttrn 11164 ax-pre-ltadd 11165 ax-pre-mulgt0 11166 |
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 3376 df-rab 3430 df-v 3472 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-pss 3960 df-nul 4316 df-if 4520 df-pw 4595 df-sn 4620 df-pr 4622 df-op 4626 df-uni 4899 df-int 4941 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6286 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6531 df-fn 6532 df-f 6533 df-f1 6534 df-fo 6535 df-f1o 6536 df-fv 6537 df-riota 7346 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7836 df-1st 7954 df-2nd 7955 df-frecs 8245 df-wrecs 8276 df-recs 8350 df-rdg 8389 df-1o 8445 df-er 8683 df-en 8920 df-dom 8921 df-sdom 8922 df-fin 8923 df-card 9913 df-pnf 11229 df-mnf 11230 df-xr 11231 df-ltxr 11232 df-le 11233 df-sub 11425 df-neg 11426 df-nn 12192 df-n0 12452 df-z 12538 df-uz 12802 df-fz 13464 df-fzo 13607 df-hash 14270 df-word 14444 df-substr 14570 df-pfx 14600 |
This theorem is referenced by: pfxid 14613 pfxfv0 14621 pfxtrcfv 14622 pfxfvlsw 14624 pfxeq 14625 ccatpfx 14630 pfxccatin12lem2 14660 splfv1 14684 repswpfx 14714 cshwidxmod 14732 pfx2 14877 wwlksm1edg 28995 wwlksnred 29006 clwwlkinwwlk 29153 clwwlkf 29160 wwlksubclwwlk 29171 dlwwlknondlwlknonf1olem1 29477 cycpmco2 32158 revpfxsfxrev 33921 |
Copyright terms: Public domain | W3C validator |