This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝐴 ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
2 nn0fz0 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐴 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
3 1 2 sylib ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
4 3 3ad2ant1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
5 eleq1 ⊢ ( 𝑁 = ( ♯ ‘ 𝐴 ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ↔ ( ♯ ‘ 𝐴 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) )
6 5 3ad2ant3 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝐴 ) ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ↔ ( ♯ ‘ 𝐴 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) )
7 4 6 mpbird ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝐴 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
8 eqid ⊢ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 )
9 8 pfxccatpfx1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( 𝐴 prefix 𝑁 ) )
10 7 9 syld3an3 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝐴 ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( 𝐴 prefix 𝑁 ) )
11 oveq2 ⊢ ( 𝑁 = ( ♯ ‘ 𝐴 ) → ( 𝐴 prefix 𝑁 ) = ( 𝐴 prefix ( ♯ ‘ 𝐴 ) ) )
12 11 3ad2ant3 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝐴 ) ) → ( 𝐴 prefix 𝑁 ) = ( 𝐴 prefix ( ♯ ‘ 𝐴 ) ) )
13 pfxid ⊢ ( 𝐴 ∈ Word 𝑉 → ( 𝐴 prefix ( ♯ ‘ 𝐴 ) ) = 𝐴 )
14 13 3ad2ant1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝐴 ) ) → ( 𝐴 prefix ( ♯ ‘ 𝐴 ) ) = 𝐴 )
15 10 12 14 3eqtrd ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝐴 ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = 𝐴 )