Theorem ccatfv0

Description: The first symbol of a concatenation of two words is the first symbol of the first word if the first word is not empty. (Contributed by Alexander van der Vekens, 22-Sep-2018)

	Ref	Expression
Assertion	ccatfv0	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝐴 ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		lencl	⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
2		elnnnn0b	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 0 < ( ♯ ‘ 𝐴 ) ) )
3	2	biimpri	⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 0 < ( ♯ ‘ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
4	1 3	sylan	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
5		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ )
6	4 5	sylibr	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝐴 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
7	6	3adant2	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝐴 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
8		ccatval1	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )
9	7 8	syld3an3	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝐴 ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )