Metamath Proof Explorer

Theorem pfxccatin12d

Description: The subword of a concatenation of two words within both of the concatenated words. (Contributed by AV, 31-May-2018) (Revised by AV, 10-May-2020)

Ref Expression
Hypotheses swrdccatind.l 
|- ( ph -> ( # ` A ) = L )
swrdccatind.w 
|- ( ph -> ( A e. Word V /\ B e. Word V ) )
pfxccatin12d.m 
|- ( ph -> M e. ( 0 ... L ) )
pfxccatin12d.n 
|- ( ph -> N e. ( L ... ( L + ( # ` B ) ) ) )
Assertion pfxccatin12d 
|- ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatind.l 
 |-  ( ph -> ( # ` A ) = L )
2 swrdccatind.w 
 |-  ( ph -> ( A e. Word V /\ B e. Word V ) )
3 pfxccatin12d.m 
 |-  ( ph -> M e. ( 0 ... L ) )
4 pfxccatin12d.n 
 |-  ( ph -> N e. ( L ... ( L + ( # ` B ) ) ) )
5 1 oveq2d 
 |-  ( ph -> ( 0 ... ( # ` A ) ) = ( 0 ... L ) )
6 5 eleq2d 
 |-  ( ph -> ( M e. ( 0 ... ( # ` A ) ) <-> M e. ( 0 ... L ) ) )
7 1 oveq1d 
 |-  ( ph -> ( ( # ` A ) + ( # ` B ) ) = ( L + ( # ` B ) ) )
8 1 7 oveq12d 
 |-  ( ph -> ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) = ( L ... ( L + ( # ` B ) ) ) )
9 8 eleq2d 
 |-  ( ph -> ( N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) <-> N e. ( L ... ( L + ( # ` B ) ) ) ) )
10 6 9 anbi12d 
 |-  ( ph -> ( ( M e. ( 0 ... ( # ` A ) ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) <-> ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
11 3 4 10 mpbir2and 
 |-  ( ph -> ( M e. ( 0 ... ( # ` A ) ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) )
12 eqid 
 |-  ( # ` A ) = ( # ` A )
13 12 pfxccatin12 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... ( # ` A ) ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , ( # ` A ) >. ) ++ ( B prefix ( N - ( # ` A ) ) ) ) ) )
14 2 11 13 sylc 
 |-  ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , ( # ` A ) >. ) ++ ( B prefix ( N - ( # ` A ) ) ) ) )
15 1 opeq2d 
 |-  ( ph -> <. M , ( # ` A ) >. = <. M , L >. )
16 15 oveq2d 
 |-  ( ph -> ( A substr <. M , ( # ` A ) >. ) = ( A substr <. M , L >. ) )
17 1 oveq2d 
 |-  ( ph -> ( N - ( # ` A ) ) = ( N - L ) )
18 17 oveq2d 
 |-  ( ph -> ( B prefix ( N - ( # ` A ) ) ) = ( B prefix ( N - L ) ) )
19 16 18 oveq12d 
 |-  ( ph -> ( ( A substr <. M , ( # ` A ) >. ) ++ ( B prefix ( N - ( # ` A ) ) ) ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) )
20 14 19 eqtrd 
 |-  ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) )