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 𝑁 ) = 𝐴 )