Metamath Proof Explorer

Theorem swrdccatin2d

Description: The subword of a concatenation of two words within the second of the concatenated words. (Contributed by AV, 31-May-2018) (Revised by Mario Carneiro/AV, 21-Oct-2018)

Ref Expression
Hypotheses swrdccatind.l 
|- ( ph -> ( # ` A ) = L )
swrdccatind.w 
|- ( ph -> ( A e. Word V /\ B e. Word V ) )
swrdccatin2d.1 
|- ( ph -> M e. ( L ... N ) )
swrdccatin2d.2 
|- ( ph -> N e. ( L ... ( L + ( # ` B ) ) ) )
Assertion swrdccatin2d 
|- ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - L ) , ( 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 swrdccatin2d.1 
 |-  ( ph -> M e. ( L ... N ) )
4 swrdccatin2d.2 
 |-  ( ph -> N e. ( L ... ( L + ( # ` B ) ) ) )
5 2 adantl 
 |-  ( ( ( # ` A ) = L /\ ph ) -> ( A e. Word V /\ B e. Word V ) )
6 3 4 jca 
 |-  ( ph -> ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) )
7 6 adantl 
 |-  ( ( ( # ` A ) = L /\ ph ) -> ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) )
8 oveq1 
 |-  ( ( # ` A ) = L -> ( ( # ` A ) ... N ) = ( L ... N ) )
9 8 eleq2d 
 |-  ( ( # ` A ) = L -> ( M e. ( ( # ` A ) ... N ) <-> M e. ( L ... N ) ) )
10 id 
 |-  ( ( # ` A ) = L -> ( # ` A ) = L )
11 oveq1 
 |-  ( ( # ` A ) = L -> ( ( # ` A ) + ( # ` B ) ) = ( L + ( # ` B ) ) )
12 10 11 oveq12d 
 |-  ( ( # ` A ) = L -> ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) = ( L ... ( L + ( # ` B ) ) ) )
13 12 eleq2d 
 |-  ( ( # ` A ) = L -> ( N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) <-> N e. ( L ... ( L + ( # ` B ) ) ) ) )
14 9 13 anbi12d 
 |-  ( ( # ` A ) = L -> ( ( M e. ( ( # ` A ) ... N ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) <-> ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
15 14 adantr 
 |-  ( ( ( # ` A ) = L /\ ph ) -> ( ( M e. ( ( # ` A ) ... N ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) <-> ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
16 7 15 mpbird 
 |-  ( ( ( # ` A ) = L /\ ph ) -> ( M e. ( ( # ` A ) ... N ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) )
17 5 16 jca 
 |-  ( ( ( # ` A ) = L /\ ph ) -> ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( ( # ` A ) ... N ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) ) )
18 17 ex 
 |-  ( ( # ` A ) = L -> ( ph -> ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( ( # ` A ) ... N ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) ) ) )
19 eqid 
 |-  ( # ` A ) = ( # ` A )
20 19 swrdccatin2 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( ( # ` A ) ... N ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - ( # ` A ) ) , ( N - ( # ` A ) ) >. ) ) )
21 20 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( ( # ` A ) ... N ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - ( # ` A ) ) , ( N - ( # ` A ) ) >. ) )
22 18 21 syl6 
 |-  ( ( # ` A ) = L -> ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - ( # ` A ) ) , ( N - ( # ` A ) ) >. ) ) )
23 oveq2 
 |-  ( ( # ` A ) = L -> ( M - ( # ` A ) ) = ( M - L ) )
24 oveq2 
 |-  ( ( # ` A ) = L -> ( N - ( # ` A ) ) = ( N - L ) )
25 23 24 opeq12d 
 |-  ( ( # ` A ) = L -> <. ( M - ( # ` A ) ) , ( N - ( # ` A ) ) >. = <. ( M - L ) , ( N - L ) >. )
26 25 oveq2d 
 |-  ( ( # ` A ) = L -> ( B substr <. ( M - ( # ` A ) ) , ( N - ( # ` A ) ) >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
27 26 eqeq2d 
 |-  ( ( # ` A ) = L -> ( ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - ( # ` A ) ) , ( N - ( # ` A ) ) >. ) <-> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) ) )
28 22 27 sylibd 
 |-  ( ( # ` A ) = L -> ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) ) )
29 1 28 mpcom 
 |-  ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )