Metamath Proof Explorer

Theorem swrdccat3b

Description: A suffix of a concatenation is either a suffix of the second concatenated word or a concatenation of a suffix of the first word with the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018) (Revised by Alexander van der Vekens, 30-May-2018) (Proof shortened by AV, 14-Oct-2022)

Ref Expression
Hypothesis swrdccatin2.l ⊢ L = A
Assertion swrdccat3b ⊢ A ∈ Word V ∧ B ∈ Word V → M ∈ 0 … L + B → A ++ B substr M L + B = if L ≤ M B substr M − L B A substr M L ++ B

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢ L = A
2 simpl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B → A ∈ Word V ∧ B ∈ Word V
3 simpr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B → M ∈ 0 … L + B
4 elfzubelfz ⊢ M ∈ 0 … L + B → L + B ∈ 0 … L + B
5 4 adantl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B → L + B ∈ 0 … L + B
6 1 pfxccat3 ⊢ A ∈ Word V ∧ B ∈ Word V → M ∈ 0 … L + B ∧ L + B ∈ 0 … L + B → A ++ B substr M L + B = if L + B ≤ L A substr M L + B if L ≤ M B substr M − L L + B - L A substr M L ++ B prefix L + B - L
7 6 imp ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ L + B ∈ 0 … L + B → A ++ B substr M L + B = if L + B ≤ L A substr M L + B if L ≤ M B substr M − L L + B - L A substr M L ++ B prefix L + B - L
8 2 3 5 7 syl12anc ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B → A ++ B substr M L + B = if L + B ≤ L A substr M L + B if L ≤ M B substr M − L L + B - L A substr M L ++ B prefix L + B - L
9 1 swrdccat3blem ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ L + B ≤ L → if L ≤ M B substr M − L B A substr M L ++ B = A substr M L + B
10 iftrue ⊢ L ≤ M → if L ≤ M B substr M − L B A substr M L ++ B = B substr M − L B
11 10 3ad2ant3 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ ¬ L + B ≤ L ∧ L ≤ M → if L ≤ M B substr M − L B A substr M L ++ B = B substr M − L B
12 lencl ⊢ A ∈ Word V → A ∈ ℕ 0
13 12 nn0cnd ⊢ A ∈ Word V → A ∈ ℂ
14 lencl ⊢ B ∈ Word V → B ∈ ℕ 0
15 14 nn0cnd ⊢ B ∈ Word V → B ∈ ℂ
16 1 eqcomi ⊢ A = L
17 16 eleq1i ⊢ A ∈ ℂ ↔ L ∈ ℂ
18 pncan2 ⊢ L ∈ ℂ ∧ B ∈ ℂ → L + B - L = B
19 17 18 sylanb ⊢ A ∈ ℂ ∧ B ∈ ℂ → L + B - L = B
20 13 15 19 syl2an ⊢ A ∈ Word V ∧ B ∈ Word V → L + B - L = B
21 20 eqcomd ⊢ A ∈ Word V ∧ B ∈ Word V → B = L + B - L
22 21 adantr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B → B = L + B - L
23 22 3ad2ant1 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ ¬ L + B ≤ L ∧ L ≤ M → B = L + B - L
24 23 opeq2d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ ¬ L + B ≤ L ∧ L ≤ M → M − L B = M − L L + B - L
25 24 oveq2d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ ¬ L + B ≤ L ∧ L ≤ M → B substr M − L B = B substr M − L L + B - L
26 11 25 eqtrd ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ ¬ L + B ≤ L ∧ L ≤ M → if L ≤ M B substr M − L B A substr M L ++ B = B substr M − L L + B - L
27 iffalse ⊢ ¬ L ≤ M → if L ≤ M B substr M − L B A substr M L ++ B = A substr M L ++ B
28 27 3ad2ant3 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ ¬ L + B ≤ L ∧ ¬ L ≤ M → if L ≤ M B substr M − L B A substr M L ++ B = A substr M L ++ B
29 20 adantr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B → L + B - L = B
30 29 3ad2ant1 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ ¬ L + B ≤ L ∧ ¬ L ≤ M → L + B - L = B
31 30 oveq2d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ ¬ L + B ≤ L ∧ ¬ L ≤ M → B prefix L + B - L = B prefix B
32 pfxid ⊢ B ∈ Word V → B prefix B = B
33 32 adantl ⊢ A ∈ Word V ∧ B ∈ Word V → B prefix B = B
34 33 adantr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B → B prefix B = B
35 34 3ad2ant1 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ ¬ L + B ≤ L ∧ ¬ L ≤ M → B prefix B = B
36 31 35 eqtr2d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ ¬ L + B ≤ L ∧ ¬ L ≤ M → B = B prefix L + B - L
37 36 oveq2d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ ¬ L + B ≤ L ∧ ¬ L ≤ M → A substr M L ++ B = A substr M L ++ B prefix L + B - L
38 28 37 eqtrd ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B ∧ ¬ L + B ≤ L ∧ ¬ L ≤ M → if L ≤ M B substr M − L B A substr M L ++ B = A substr M L ++ B prefix L + B - L
39 9 26 38 2if2 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B → if L ≤ M B substr M − L B A substr M L ++ B = if L + B ≤ L A substr M L + B if L ≤ M B substr M − L L + B - L A substr M L ++ B prefix L + B - L
40 8 39 eqtr4d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L + B → A ++ B substr M L + B = if L ≤ M B substr M − L B A substr M L ++ B
41 40 ex ⊢ A ∈ Word V ∧ B ∈ Word V → M ∈ 0 … L + B → A ++ B substr M L + B = if L ≤ M B substr M − L B A substr M L ++ B