Metamath Proof Explorer

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 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ 0 < A → A ++ B ⁡ 0 = A ⁡ 0

Proof

Step Hyp Ref Expression
1 lencl ⊢ A ∈ Word V → A ∈ ℕ 0
2 elnnnn0b ⊢ A ∈ ℕ ↔ A ∈ ℕ 0 ∧ 0 < A
3 2 biimpri ⊢ A ∈ ℕ 0 ∧ 0 < A → A ∈ ℕ
4 1 3 sylan ⊢ A ∈ Word V ∧ 0 < A → A ∈ ℕ
5 lbfzo0 ⊢ 0 ∈ 0 ..^ A ↔ A ∈ ℕ
6 4 5 sylibr ⊢ A ∈ Word V ∧ 0 < A → 0 ∈ 0 ..^ A
7 6 3adant2 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ 0 < A → 0 ∈ 0 ..^ A
8 ccatval1 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ 0 ∈ 0 ..^ A → A ++ B ⁡ 0 = A ⁡ 0
9 7 8 syld3an3 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ 0 < A → A ++ B ⁡ 0 = A ⁡ 0