Metamath Proof Explorer

Theorem pfxccatid

Description: A prefix of a concatenation of length of the first concatenated word is the first word itself. (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 10-May-2020)

Ref Expression
Assertion pfxccatid ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N = A → A ++ B prefix N = A

Proof

Step Hyp Ref Expression
1 lencl ⊢ A ∈ Word V → A ∈ ℕ 0
2 nn0fz0 ⊢ A ∈ ℕ 0 ↔ A ∈ 0 … A
3 1 2 sylib ⊢ A ∈ Word V → A ∈ 0 … A
4 3 3ad2ant1 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N = A → A ∈ 0 … A
5 eleq1 ⊢ N = A → N ∈ 0 … A ↔ A ∈ 0 … A
6 5 3ad2ant3 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N = A → N ∈ 0 … A ↔ A ∈ 0 … A
7 4 6 mpbird ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N = A → N ∈ 0 … A
8 eqid ⊢ A = A
9 8 pfxccatpfx1 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ 0 … A → A ++ B prefix N = A prefix N
10 7 9 syld3an3 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N = A → A ++ B prefix N = A prefix N
11 oveq2 ⊢ N = A → A prefix N = A prefix A
12 11 3ad2ant3 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N = A → A prefix N = A prefix A
13 pfxid ⊢ A ∈ Word V → A prefix A = A
14 13 3ad2ant1 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N = A → A prefix A = A
15 10 12 14 3eqtrd ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N = A → A ++ B prefix N = A