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	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = 𝐿 )
	swrdccatind.w	⊢ ( 𝜑 → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
	swrdccatin1d.1	⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑁 ) )
	swrdccatin1d.2	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝐿 ) )
Assertion	swrdccatin1d	⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		swrdccatind.l	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = 𝐿 )
2		swrdccatind.w	⊢ ( 𝜑 → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
3		swrdccatin1d.1	⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑁 ) )
4		swrdccatin1d.2	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝐿 ) )
5		oveq2	⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( 0 ... ( ♯ ‘ 𝐴 ) ) = ( 0 ... 𝐿 ) )
6	5	eleq2d	⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ↔ 𝑁 ∈ ( 0 ... 𝐿 ) ) )
7	4 6	syl5ibr	⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( 𝜑 → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) )
8	1 7	mpcom	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
9	3 8	jca	⊢ ( 𝜑 → ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) )
10		swrdccatin1	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )
11	2 9 10	sylc	⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) )