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 ⊢ φ → A = L
swrdccatind.w ⊢ φ → A ∈ Word V ∧ B ∈ Word V
pfxccatin12d.m ⊢ φ → M ∈ 0 … L
pfxccatin12d.n ⊢ φ → N ∈ L … L + B
Assertion pfxccatin12d ⊢ φ → A ++ B substr M N = A substr M L ++ B prefix N − L

Proof

Step Hyp Ref Expression
1 swrdccatind.l ⊢ φ → A = L
2 swrdccatind.w ⊢ φ → A ∈ Word V ∧ B ∈ Word V
3 pfxccatin12d.m ⊢ φ → M ∈ 0 … L
4 pfxccatin12d.n ⊢ φ → N ∈ L … L + B
5 1 oveq2d ⊢ φ → 0 … A = 0 … L
6 5 eleq2d ⊢ φ → M ∈ 0 … A ↔ M ∈ 0 … L
7 1 oveq1d ⊢ φ → A + B = L + B
8 1 7 oveq12d ⊢ φ → A … A + B = L … L + B
9 8 eleq2d ⊢ φ → N ∈ A … A + B ↔ N ∈ L … L + B
10 6 9 anbi12d ⊢ φ → M ∈ 0 … A ∧ N ∈ A … A + B ↔ M ∈ 0 … L ∧ N ∈ L … L + B
11 3 4 10 mpbir2and ⊢ φ → M ∈ 0 … A ∧ N ∈ A … A + B
12 eqid ⊢ A = A
13 12 pfxccatin12 ⊢ A ∈ Word V ∧ B ∈ Word V → M ∈ 0 … A ∧ N ∈ A … A + B → A ++ B substr M N = A substr M A ++ B prefix N − A
14 2 11 13 sylc ⊢ φ → A ++ B substr M N = A substr M A ++ B prefix N − A
15 1 opeq2d ⊢ φ → M A = M L
16 15 oveq2d ⊢ φ → A substr M A = A substr M L
17 1 oveq2d ⊢ φ → N − A = N − L
18 17 oveq2d ⊢ φ → B prefix N − A = B prefix N − L
19 16 18 oveq12d ⊢ φ → A substr M A ++ B prefix N − A = A substr M L ++ B prefix N − L
20 14 19 eqtrd ⊢ φ → A ++ B substr M N = A substr M L ++ B prefix N − L