Description: A prefix of a prefix with the same length is the original prefix. In other words, the operation "prefix of length N " is idempotent. (Contributed by AV, 5-Apr-2018) (Revised by AV, 8-May-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pfxpfxid | ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝑁 ) prefix 𝑁 ) = ( 𝑊 prefix 𝑁 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elfznn0 | ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℕ0 ) | |
| 2 | nn0fz0 | ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( 0 ... 𝑁 ) ) | |
| 3 | 1 2 | sylib | ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ( 0 ... 𝑁 ) ) |
| 4 | 3 | adantl | ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ( 0 ... 𝑁 ) ) |
| 5 | pfxpfx | ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑁 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑊 prefix 𝑁 ) prefix 𝑁 ) = ( 𝑊 prefix 𝑁 ) ) | |
| 6 | 4 5 | mpd3an3 | ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝑁 ) prefix 𝑁 ) = ( 𝑊 prefix 𝑁 ) ) |