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

Proof

Step Hyp Ref Expression
1 swrdccatind.l ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = 𝐿 )
2 swrdccatind.w ⊢ ( 𝜑 → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
3 pfxccatin12d.m ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝐿 ) )
4 pfxccatin12d.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
5 1 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐴 ) ) = ( 0 ... 𝐿 ) )
6 5 eleq2d ⊢ ( 𝜑 → ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ↔ 𝑀 ∈ ( 0 ... 𝐿 ) ) )
7 1 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( 𝐿 + ( ♯ ‘ 𝐵 ) ) )
8 1 7 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) = ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
9 8 eleq2d ⊢ ( 𝜑 → ( 𝑁 ∈ ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↔ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
10 6 9 anbi12d ⊢ ( 𝜑 → ( ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑁 ∈ ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ↔ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
11 3 4 10 mpbir2and ⊢ ( 𝜑 → ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑁 ∈ ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) )
12 eqid ⊢ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 )
13 12 pfxccatin12 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑁 ∈ ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 𝑀 , ( ♯ ‘ 𝐴 ) ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − ( ♯ ‘ 𝐴 ) ) ) ) ) )
14 2 11 13 sylc ⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 𝑀 , ( ♯ ‘ 𝐴 ) ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − ( ♯ ‘ 𝐴 ) ) ) ) )
15 1 opeq2d ⊢ ( 𝜑 → ⟨ 𝑀 , ( ♯ ‘ 𝐴 ) ⟩ = ⟨ 𝑀 , 𝐿 ⟩ )
16 15 oveq2d ⊢ ( 𝜑 → ( 𝐴 substr ⟨ 𝑀 , ( ♯ ‘ 𝐴 ) ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) )
17 1 oveq2d ⊢ ( 𝜑 → ( 𝑁 − ( ♯ ‘ 𝐴 ) ) = ( 𝑁 − 𝐿 ) )
18 17 oveq2d ⊢ ( 𝜑 → ( 𝐵 prefix ( 𝑁 − ( ♯ ‘ 𝐴 ) ) ) = ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) )
19 16 18 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 substr ⟨ 𝑀 , ( ♯ ‘ 𝐴 ) ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − ( ♯ ‘ 𝐴 ) ) ) ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )
20 14 19 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )