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

Metamath Proof Explorer

Theorem pfxccatpfx1

Description: A prefix of a concatenation being a prefix of the first concatenated word. (Contributed by AV, 10-May-2020)

Ref Expression
Hypothesis swrdccatin2.l 
|- L = ( # ` A )
Assertion pfxccatpfx1 
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( ( A ++ B ) prefix N ) = ( A prefix N ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l 
 |-  L = ( # ` A )
2 3simpa 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( A e. Word V /\ B e. Word V ) )
3 elfznn0 
 |-  ( N e. ( 0 ... L ) -> N e. NN0 )
4 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
5 3 4 syl 
 |-  ( N e. ( 0 ... L ) -> 0 e. ( 0 ... N ) )
6 1 oveq2i 
 |-  ( 0 ... L ) = ( 0 ... ( # ` A ) )
7 6 eleq2i 
 |-  ( N e. ( 0 ... L ) <-> N e. ( 0 ... ( # ` A ) ) )
8 7 biimpi 
 |-  ( N e. ( 0 ... L ) -> N e. ( 0 ... ( # ` A ) ) )
9 5 8 jca 
 |-  ( N e. ( 0 ... L ) -> ( 0 e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) )
10 9 3ad2ant3 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( 0 e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) )
11 swrdccatin1 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( 0 e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( ( A ++ B ) substr <. 0 , N >. ) = ( A substr <. 0 , N >. ) ) )
12 2 10 11 sylc 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( ( A ++ B ) substr <. 0 , N >. ) = ( A substr <. 0 , N >. ) )
13 ccatcl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) e. Word V )
14 13 3adant3 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( A ++ B ) e. Word V )
15 3 3ad2ant3 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> N e. NN0 )
16 14 15 jca 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( ( A ++ B ) e. Word V /\ N e. NN0 ) )
17 pfxval 
 |-  ( ( ( A ++ B ) e. Word V /\ N e. NN0 ) -> ( ( A ++ B ) prefix N ) = ( ( A ++ B ) substr <. 0 , N >. ) )
18 16 17 syl 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( ( A ++ B ) prefix N ) = ( ( A ++ B ) substr <. 0 , N >. ) )
19 pfxval 
 |-  ( ( A e. Word V /\ N e. NN0 ) -> ( A prefix N ) = ( A substr <. 0 , N >. ) )
20 3 19 sylan2 
 |-  ( ( A e. Word V /\ N e. ( 0 ... L ) ) -> ( A prefix N ) = ( A substr <. 0 , N >. ) )
21 20 3adant2 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( A prefix N ) = ( A substr <. 0 , N >. ) )
22 12 18 21 3eqtr4d 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( ( A ++ B ) prefix N ) = ( A prefix N ) )