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 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )