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 
|- ( ( 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 )