Metamath Proof Explorer

Theorem swrdccatin2d

Description: The subword of a concatenation of two words within the second 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 𝑉 ) )
swrdccatin2d.1 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐿 ... 𝑁 ) )
swrdccatin2d.2 ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
Assertion swrdccatin2d ( 𝜑 → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 swrdccatind.l ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = 𝐿 )
2 swrdccatind.w ⊢ ( 𝜑 → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
3 swrdccatin2d.1 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐿 ... 𝑁 ) )
4 swrdccatin2d.2 ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
5 2 adantl ⊢ ( ( ( ♯ ‘ 𝐴 ) = 𝐿 ∧ 𝜑 ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
6 3 4 jca ⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝐿 ... 𝑁 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
7 6 adantl ⊢ ( ( ( ♯ ‘ 𝐴 ) = 𝐿 ∧ 𝜑 ) → ( 𝑀 ∈ ( 𝐿 ... 𝑁 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
8 oveq1 ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( ♯ ‘ 𝐴 ) ... 𝑁 ) = ( 𝐿 ... 𝑁 ) )
9 8 eleq2d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( 𝑀 ∈ ( ( ♯ ‘ 𝐴 ) ... 𝑁 ) ↔ 𝑀 ∈ ( 𝐿 ... 𝑁 ) ) )
10 id ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ♯ ‘ 𝐴 ) = 𝐿 )
11 oveq1 ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( 𝐿 + ( ♯ ‘ 𝐵 ) ) )
12 10 11 oveq12d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) = ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
13 12 eleq2d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( 𝑁 ∈ ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↔ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
14 9 13 anbi12d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( 𝑀 ∈ ( ( ♯ ‘ 𝐴 ) ... 𝑁 ) ∧ 𝑁 ∈ ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ↔ ( 𝑀 ∈ ( 𝐿 ... 𝑁 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
15 14 adantr ⊢ ( ( ( ♯ ‘ 𝐴 ) = 𝐿 ∧ 𝜑 ) → ( ( 𝑀 ∈ ( ( ♯ ‘ 𝐴 ) ... 𝑁 ) ∧ 𝑁 ∈ ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ↔ ( 𝑀 ∈ ( 𝐿 ... 𝑁 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
16 7 15 mpbird ⊢ ( ( ( ♯ ‘ 𝐴 ) = 𝐿 ∧ 𝜑 ) → ( 𝑀 ∈ ( ( ♯ ‘ 𝐴 ) ... 𝑁 ) ∧ 𝑁 ∈ ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) )
17 5 16 jca ⊢ ( ( ( ♯ ‘ 𝐴 ) = 𝐿 ∧ 𝜑 ) → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( ( ♯ ‘ 𝐴 ) ... 𝑁 ) ∧ 𝑁 ∈ ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ) )
18 17 ex ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( 𝜑 → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( ( ♯ ‘ 𝐴 ) ... 𝑁 ) ∧ 𝑁 ∈ ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ) ) )
19 eqid ⊢ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 )
20 19 swrdccatin2 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( ( ♯ ‘ 𝐴 ) ... 𝑁 ) ∧ 𝑁 ∈ ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − ( ♯ ‘ 𝐴 ) ) , ( 𝑁 − ( ♯ ‘ 𝐴 ) ) ⟩ ) ) )
21 20 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( ( ♯ ‘ 𝐴 ) ... 𝑁 ) ∧ 𝑁 ∈ ( ( ♯ ‘ 𝐴 ) ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − ( ♯ ‘ 𝐴 ) ) , ( 𝑁 − ( ♯ ‘ 𝐴 ) ) ⟩ ) )
22 18 21 syl6 ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( 𝜑 → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − ( ♯ ‘ 𝐴 ) ) , ( 𝑁 − ( ♯ ‘ 𝐴 ) ) ⟩ ) ) )
23 oveq2 ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( 𝑀 − ( ♯ ‘ 𝐴 ) ) = ( 𝑀 − 𝐿 ) )
24 oveq2 ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( 𝑁 − ( ♯ ‘ 𝐴 ) ) = ( 𝑁 − 𝐿 ) )
25 23 24 opeq12d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ⟨ ( 𝑀 − ( ♯ ‘ 𝐴 ) ) , ( 𝑁 − ( ♯ ‘ 𝐴 ) ) ⟩ = ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ )
26 25 oveq2d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( 𝐵 substr ⟨ ( 𝑀 − ( ♯ ‘ 𝐴 ) ) , ( 𝑁 − ( ♯ ‘ 𝐴 ) ) ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) )
27 26 eqeq2d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − ( ♯ ‘ 𝐴 ) ) , ( 𝑁 − ( ♯ ‘ 𝐴 ) ) ⟩ ) ↔ ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) )
28 22 27 sylibd ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( 𝜑 → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) )
29 1 28 mpcom ⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) )