Metamath Proof Explorer

Theorem pfxccatpfx2

Description: A prefix of a concatenation of two words being the first word concatenated with a prefix of the second word. (Contributed by AV, 10-May-2020)

Ref Expression
Hypotheses swrdccatin2.l ⊢ L = A
pfxccatpfx2.m ⊢ M = B
Assertion pfxccatpfx2 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → A ++ B prefix N = A ++ B prefix N − L

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢ L = A
2 pfxccatpfx2.m ⊢ M = B
3 ccatcl ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B ∈ Word V
4 3 3adant3 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → A ++ B ∈ Word V
5 lencl ⊢ A ∈ Word V → A ∈ ℕ 0
6 1 5 eqeltrid ⊢ A ∈ Word V → L ∈ ℕ 0
7 elfzuz ⊢ N ∈ L + 1 … L + M → N ∈ ℤ ≥ L + 1
8 peano2nn0 ⊢ L ∈ ℕ 0 → L + 1 ∈ ℕ 0
9 8 anim1i ⊢ L ∈ ℕ 0 ∧ N ∈ ℤ ≥ L + 1 → L + 1 ∈ ℕ 0 ∧ N ∈ ℤ ≥ L + 1
10 6 7 9 syl2an ⊢ A ∈ Word V ∧ N ∈ L + 1 … L + M → L + 1 ∈ ℕ 0 ∧ N ∈ ℤ ≥ L + 1
11 10 3adant2 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → L + 1 ∈ ℕ 0 ∧ N ∈ ℤ ≥ L + 1
12 eluznn0 ⊢ L + 1 ∈ ℕ 0 ∧ N ∈ ℤ ≥ L + 1 → N ∈ ℕ 0
13 11 12 syl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → N ∈ ℕ 0
14 pfxval ⊢ A ++ B ∈ Word V ∧ N ∈ ℕ 0 → A ++ B prefix N = A ++ B substr 0 N
15 4 13 14 syl2anc ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → A ++ B prefix N = A ++ B substr 0 N
16 3simpa ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → A ∈ Word V ∧ B ∈ Word V
17 6 3ad2ant1 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → L ∈ ℕ 0
18 0elfz ⊢ L ∈ ℕ 0 → 0 ∈ 0 … L
19 17 18 syl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → 0 ∈ 0 … L
20 5 nn0zd ⊢ A ∈ Word V → A ∈ ℤ
21 1 20 eqeltrid ⊢ A ∈ Word V → L ∈ ℤ
22 21 adantr ⊢ A ∈ Word V ∧ B ∈ Word V → L ∈ ℤ
23 uzid ⊢ L ∈ ℤ → L ∈ ℤ ≥ L
24 peano2uz ⊢ L ∈ ℤ ≥ L → L + 1 ∈ ℤ ≥ L
25 fzss1 ⊢ L + 1 ∈ ℤ ≥ L → L + 1 … L + M ⊆ L … L + M
26 22 23 24 25 4syl ⊢ A ∈ Word V ∧ B ∈ Word V → L + 1 … L + M ⊆ L … L + M
27 2 eqcomi ⊢ B = M
28 27 oveq2i ⊢ L + B = L + M
29 28 oveq2i ⊢ L … L + B = L … L + M
30 26 29 sseqtrrdi ⊢ A ∈ Word V ∧ B ∈ Word V → L + 1 … L + M ⊆ L … L + B
31 30 sseld ⊢ A ∈ Word V ∧ B ∈ Word V → N ∈ L + 1 … L + M → N ∈ L … L + B
32 31 3impia ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → N ∈ L … L + B
33 19 32 jca ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → 0 ∈ 0 … L ∧ N ∈ L … L + B
34 1 pfxccatin12 ⊢ A ∈ Word V ∧ B ∈ Word V → 0 ∈ 0 … L ∧ N ∈ L … L + B → A ++ B substr 0 N = A substr 0 L ++ B prefix N − L
35 16 33 34 sylc ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → A ++ B substr 0 N = A substr 0 L ++ B prefix N − L
36 1 opeq2i ⊢ 0 L = 0 A
37 36 oveq2i ⊢ A substr 0 L = A substr 0 A
38 pfxval ⊢ A ∈ Word V ∧ A ∈ ℕ 0 → A prefix A = A substr 0 A
39 5 38 mpdan ⊢ A ∈ Word V → A prefix A = A substr 0 A
40 pfxid ⊢ A ∈ Word V → A prefix A = A
41 39 40 eqtr3d ⊢ A ∈ Word V → A substr 0 A = A
42 37 41 eqtrid ⊢ A ∈ Word V → A substr 0 L = A
43 42 3ad2ant1 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → A substr 0 L = A
44 43 oveq1d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → A substr 0 L ++ B prefix N − L = A ++ B prefix N − L
45 15 35 44 3eqtrd ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ L + 1 … L + M → A ++ B prefix N = A ++ B prefix N − L