This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wrdeqs1cat

Description: Decompose a nonempty word by separating off the first symbol. (Contributed by Stefan O'Rear, 25-Aug-2015) (Revised by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 12-Oct-2022)

Ref Expression
Assertion wrdeqs1cat ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ) → 𝑊 = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ++ ( 𝑊 substr ⟨ 1 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ) → 𝑊 ∈ Word 𝐴 )
2 wrdfin ⊢ ( 𝑊 ∈ Word 𝐴 → 𝑊 ∈ Fin )
3 1elfz0hash ⊢ ( ( 𝑊 ∈ Fin ∧ 𝑊 ≠ ∅ ) → 1 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
4 2 3 sylan ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ) → 1 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
5 lennncl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
6 5 nnnn0d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
7 eluzfz2 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
8 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
9 7 8 eleq2s ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
10 6 9 syl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
11 ccatpfx ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 1 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 1 ) ++ ( 𝑊 substr ⟨ 1 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) )
12 1 4 10 11 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 prefix 1 ) ++ ( 𝑊 substr ⟨ 1 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) )
13 pfx1 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 prefix 1 ) = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )
14 13 oveq1d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 prefix 1 ) ++ ( 𝑊 substr ⟨ 1 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ++ ( 𝑊 substr ⟨ 1 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
15 pfxid ⊢ ( 𝑊 ∈ Word 𝐴 → ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
16 15 adantr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
17 12 14 16 3eqtr3rd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ) → 𝑊 = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ++ ( 𝑊 substr ⟨ 1 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )