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

Metamath Proof Explorer

Theorem swrdccatin1d

Description: The subword of a concatenation of two words within the first 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 ) )
swrdccatin1d.1 
|- ( ph -> M e. ( 0 ... N ) )
swrdccatin1d.2 
|- ( ph -> N e. ( 0 ... L ) )
Assertion swrdccatin1d 
|- ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) )

Proof

Step Hyp Ref Expression
1 swrdccatind.l 
 |-  ( ph -> ( # ` A ) = L )
2 swrdccatind.w 
 |-  ( ph -> ( A e. Word V /\ B e. Word V ) )
3 swrdccatin1d.1 
 |-  ( ph -> M e. ( 0 ... N ) )
4 swrdccatin1d.2 
 |-  ( ph -> N e. ( 0 ... L ) )
5 oveq2 
 |-  ( ( # ` A ) = L -> ( 0 ... ( # ` A ) ) = ( 0 ... L ) )
6 5 eleq2d 
 |-  ( ( # ` A ) = L -> ( N e. ( 0 ... ( # ` A ) ) <-> N e. ( 0 ... L ) ) )
7 4 6 imbitrrid 
 |-  ( ( # ` A ) = L -> ( ph -> N e. ( 0 ... ( # ` A ) ) ) )
8 1 7 mpcom 
 |-  ( ph -> N e. ( 0 ... ( # ` A ) ) )
9 3 8 jca 
 |-  ( ph -> ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) )
10 swrdccatin1 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) ) )
11 2 9 10 sylc 
 |-  ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) )