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 e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( ( A ++ B ) prefix N ) = A )

Proof

Step	Hyp	Ref	Expression
1		lencl	|- ( A e. Word V -> ( # ` A ) e. NN0 )
2		nn0fz0	|- ( ( # ` A ) e. NN0 <-> ( # ` A ) e. ( 0 ... ( # ` A ) ) )
3	1 2	sylib	|- ( A e. Word V -> ( # ` A ) e. ( 0 ... ( # ` A ) ) )
4	3	3ad2ant1	|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( # ` A ) e. ( 0 ... ( # ` A ) ) )
5		eleq1	|- ( N = ( # ` A ) -> ( N e. ( 0 ... ( # ` A ) ) <-> ( # ` A ) e. ( 0 ... ( # ` A ) ) ) )
6	5	3ad2ant3	|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( N e. ( 0 ... ( # ` A ) ) <-> ( # ` A ) e. ( 0 ... ( # ` A ) ) ) )
7	4 6	mpbird	|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> N e. ( 0 ... ( # ` A ) ) )
8		eqid	|- ( # ` A ) = ( # ` A )
9	8	pfxccatpfx1	|- ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... ( # ` A ) ) ) -> ( ( A ++ B ) prefix N ) = ( A prefix N ) )
10	7 9	syld3an3	|- ( ( A e. Word V /\ B e. 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 e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( A prefix N ) = ( A prefix ( # ` A ) ) )
13		pfxid	|- ( A e. Word V -> ( A prefix ( # ` A ) ) = A )
14	13	3ad2ant1	|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( A prefix ( # ` A ) ) = A )
15	10 12 14	3eqtrd	|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( ( A ++ B ) prefix N ) = A )