Theorem pfxtrcfv0

Description: The first symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018) (Revised by AV, 3-May-2020)

	Ref	Expression
Assertion	pfxtrcfv0	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑊 ∈ Word 𝑉 )
2		wrdlenge2n0	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑊 ≠ ∅ )
3		2z	⊢ 2 ∈ ℤ
4	3	a1i	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 2 ∈ ℤ )
5		lencl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
6	5	nn0zd	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
7	6	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
8		simpr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 2 ≤ ( ♯ ‘ 𝑊 ) )
9		eluz2	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) )
10	4 7 8 9	syl3anbrc	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) )
11		uz2m1nn	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ )
12	10 11	syl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ )
13		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ↔ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ )
14	12 13	sylibr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
15		pfxtrcfv	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
16	1 2 14 15	syl3anc	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )