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 >. ) )