Metamath Proof Explorer

Theorem pfxccatpfx2

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

Ref Expression
Hypotheses swrdccatin2.l 
|- L = ( # ` A )
pfxccatpfx2.m 
|- M = ( # ` B )
Assertion pfxccatpfx2 
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) prefix N ) = ( A ++ ( B prefix ( N - L ) ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l 
 |-  L = ( # ` A )
2 pfxccatpfx2.m 
 |-  M = ( # ` B )
3 ccatcl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) e. Word V )
4 3 3adant3 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( A ++ B ) e. Word V )
5 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
6 1 5 eqeltrid 
 |-  ( A e. Word V -> L e. NN0 )
7 elfzuz 
 |-  ( N e. ( ( L + 1 ) ... ( L + M ) ) -> N e. ( ZZ>= ` ( L + 1 ) ) )
8 peano2nn0 
 |-  ( L e. NN0 -> ( L + 1 ) e. NN0 )
9 8 anim1i 
 |-  ( ( L e. NN0 /\ N e. ( ZZ>= ` ( L + 1 ) ) ) -> ( ( L + 1 ) e. NN0 /\ N e. ( ZZ>= ` ( L + 1 ) ) ) )
10 6 7 9 syl2an 
 |-  ( ( A e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( L + 1 ) e. NN0 /\ N e. ( ZZ>= ` ( L + 1 ) ) ) )
11 10 3adant2 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( L + 1 ) e. NN0 /\ N e. ( ZZ>= ` ( L + 1 ) ) ) )
12 eluznn0 
 |-  ( ( ( L + 1 ) e. NN0 /\ N e. ( ZZ>= ` ( L + 1 ) ) ) -> N e. NN0 )
13 11 12 syl 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> N e. NN0 )
14 pfxval 
 |-  ( ( ( A ++ B ) e. Word V /\ N e. NN0 ) -> ( ( A ++ B ) prefix N ) = ( ( A ++ B ) substr <. 0 , N >. ) )
15 4 13 14 syl2anc 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) prefix N ) = ( ( A ++ B ) substr <. 0 , N >. ) )
16 3simpa 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( A e. Word V /\ B e. Word V ) )
17 6 3ad2ant1 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> L e. NN0 )
18 0elfz 
 |-  ( L e. NN0 -> 0 e. ( 0 ... L ) )
19 17 18 syl 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> 0 e. ( 0 ... L ) )
20 5 nn0zd 
 |-  ( A e. Word V -> ( # ` A ) e. ZZ )
21 1 20 eqeltrid 
 |-  ( A e. Word V -> L e. ZZ )
22 21 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> L e. ZZ )
23 uzid 
 |-  ( L e. ZZ -> L e. ( ZZ>= ` L ) )
24 22 23 syl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> L e. ( ZZ>= ` L ) )
25 peano2uz 
 |-  ( L e. ( ZZ>= ` L ) -> ( L + 1 ) e. ( ZZ>= ` L ) )
26 fzss1 
 |-  ( ( L + 1 ) e. ( ZZ>= ` L ) -> ( ( L + 1 ) ... ( L + M ) ) C_ ( L ... ( L + M ) ) )
27 24 25 26 3syl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( L + 1 ) ... ( L + M ) ) C_ ( L ... ( L + M ) ) )
28 2 eqcomi 
 |-  ( # ` B ) = M
29 28 oveq2i 
 |-  ( L + ( # ` B ) ) = ( L + M )
30 29 oveq2i 
 |-  ( L ... ( L + ( # ` B ) ) ) = ( L ... ( L + M ) )
31 27 30 sseqtrrdi 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( L + 1 ) ... ( L + M ) ) C_ ( L ... ( L + ( # ` B ) ) ) )
32 31 sseld 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( ( L + 1 ) ... ( L + M ) ) -> N e. ( L ... ( L + ( # ` B ) ) ) ) )
33 32 3impia 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> N e. ( L ... ( L + ( # ` B ) ) ) )
34 19 33 jca 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( 0 e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) )
35 1 pfxccatin12 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( 0 e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. 0 , N >. ) = ( ( A substr <. 0 , L >. ) ++ ( B prefix ( N - L ) ) ) ) )
36 16 34 35 sylc 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) substr <. 0 , N >. ) = ( ( A substr <. 0 , L >. ) ++ ( B prefix ( N - L ) ) ) )
37 1 opeq2i 
 |-  <. 0 , L >. = <. 0 , ( # ` A ) >.
38 37 oveq2i 
 |-  ( A substr <. 0 , L >. ) = ( A substr <. 0 , ( # ` A ) >. )
39 pfxval 
 |-  ( ( A e. Word V /\ ( # ` A ) e. NN0 ) -> ( A prefix ( # ` A ) ) = ( A substr <. 0 , ( # ` A ) >. ) )
40 5 39 mpdan 
 |-  ( A e. Word V -> ( A prefix ( # ` A ) ) = ( A substr <. 0 , ( # ` A ) >. ) )
41 pfxid 
 |-  ( A e. Word V -> ( A prefix ( # ` A ) ) = A )
42 40 41 eqtr3d 
 |-  ( A e. Word V -> ( A substr <. 0 , ( # ` A ) >. ) = A )
43 38 42 syl5eq 
 |-  ( A e. Word V -> ( A substr <. 0 , L >. ) = A )
44 43 3ad2ant1 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( A substr <. 0 , L >. ) = A )
45 44 oveq1d 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A substr <. 0 , L >. ) ++ ( B prefix ( N - L ) ) ) = ( A ++ ( B prefix ( N - L ) ) ) )
46 15 36 45 3eqtrd 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) prefix N ) = ( A ++ ( B prefix ( N - L ) ) ) )