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