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 ⊢ W ∈ Word A ∧ W ≠ ∅ → W = ⟨“ W ⁡ 0 ”⟩ ++ W substr 1 W

Proof

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