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 \in Word V \land B \in Word V) \to (M \in (0 \dots L + \|B\|) \to (A ++ B) substr ⟨M, L + \|B\|⟩ = if (L \leq M, B substr ⟨M - L, \|B\|⟩, (A substr ⟨M, L⟩) ++ B))$

Proof

Step	Hyp	Ref	Expression
1		swrdccatin2.l	$⊢ L = \|A\|$
2		simpl	$⊢ ((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \to (A \in Word V \land B \in Word V)$
3		simpr	$⊢ ((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \to M \in (0 \dots L + \|B\|)$
4		elfzubelfz	$⊢ M \in (0 \dots L + \|B\|) \to L + \|B\| \in (0 \dots L + \|B\|)$
5	4	adantl	$⊢ ((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \to L + \|B\| \in (0 \dots L + \|B\|)$
6	1	pfxccat3	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots L + \|B\|) \land L + \|B\| \in (0 \dots L + \|B\|)) \to (A ++ B) substr ⟨M, L + \|B\|⟩ = if (L + \|B\| \leq L, A substr ⟨M, L + \|B\|⟩, if (L \leq M, B substr ⟨M - L, L + \|B\| - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (L + \|B\| - L)))))$
7	6	imp	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L + \|B\|) \land L + \|B\| \in (0 \dots L + \|B\|))) \to (A ++ B) substr ⟨M, L + \|B\|⟩ = if (L + \|B\| \leq L, A substr ⟨M, L + \|B\|⟩, if (L \leq M, B substr ⟨M - L, L + \|B\| - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (L + \|B\| - L))))$
8	2 3 5 7	syl12anc	$⊢ ((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \to (A ++ B) substr ⟨M, L + \|B\|⟩ = if (L + \|B\| \leq L, A substr ⟨M, L + \|B\|⟩, if (L \leq M, B substr ⟨M - L, L + \|B\| - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (L + \|B\| - L))))$
9	1	swrdccat3blem	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land L + \|B\| \leq L) \to if (L \leq M, B substr ⟨M - L, \|B\|⟩, (A substr ⟨M, L⟩) ++ B) = A substr ⟨M, L + \|B\|⟩$
10		iftrue	$⊢ L \leq M \to if (L \leq M, B substr ⟨M - L, \|B\|⟩, (A substr ⟨M, L⟩) ++ B) = B substr ⟨M - L, \|B\|⟩$
11	10	3ad2ant3	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land \neg L + \|B\| \leq L \land L \leq M) \to if (L \leq M, B substr ⟨M - L, \|B\|⟩, (A substr ⟨M, L⟩) ++ B) = B substr ⟨M - L, \|B\|⟩$
12		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
13	12	nn0cnd	$⊢ A \in Word V \to \|A\| \in ℂ$
14		lencl	$⊢ B \in Word V \to \|B\| \in ℕ_{0}$
15	14	nn0cnd	$⊢ B \in Word V \to \|B\| \in ℂ$
16	1	eqcomi	$⊢ \|A\| = L$
17	16	eleq1i	$⊢ \|A\| \in ℂ \leftrightarrow L \in ℂ$
18		pncan2	$⊢ (L \in ℂ \land \|B\| \in ℂ) \to L + \|B\| - L = \|B\|$
19	17 18	sylanb	$⊢ (\|A\| \in ℂ \land \|B\| \in ℂ) \to L + \|B\| - L = \|B\|$
20	13 15 19	syl2an	$⊢ (A \in Word V \land B \in Word V) \to L + \|B\| - L = \|B\|$
21	20	eqcomd	$⊢ (A \in Word V \land B \in Word V) \to \|B\| = L + \|B\| - L$
22	21	adantr	$⊢ ((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \to \|B\| = L + \|B\| - L$
23	22	3ad2ant1	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land \neg L + \|B\| \leq L \land L \leq M) \to \|B\| = L + \|B\| - L$
24	23	opeq2d	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land \neg L + \|B\| \leq L \land L \leq M) \to ⟨M - L, \|B\|⟩ = ⟨M - L, L + \|B\| - L⟩$
25	24	oveq2d	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land \neg L + \|B\| \leq L \land L \leq M) \to B substr ⟨M - L, \|B\|⟩ = B substr ⟨M - L, L + \|B\| - L⟩$
26	11 25	eqtrd	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land \neg L + \|B\| \leq L \land L \leq M) \to if (L \leq M, B substr ⟨M - L, \|B\|⟩, (A substr ⟨M, L⟩) ++ B) = B substr ⟨M - L, L + \|B\| - L⟩$
27		iffalse	$⊢ \neg L \leq M \to if (L \leq M, B substr ⟨M - L, \|B\|⟩, (A substr ⟨M, L⟩) ++ B) = (A substr ⟨M, L⟩) ++ B$
28	27	3ad2ant3	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land \neg L + \|B\| \leq L \land \neg L \leq M) \to if (L \leq M, B substr ⟨M - L, \|B\|⟩, (A substr ⟨M, L⟩) ++ B) = (A substr ⟨M, L⟩) ++ B$
29	20	adantr	$⊢ ((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \to L + \|B\| - L = \|B\|$
30	29	3ad2ant1	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land \neg L + \|B\| \leq L \land \neg L \leq M) \to L + \|B\| - L = \|B\|$
31	30	oveq2d	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land \neg L + \|B\| \leq L \land \neg L \leq M) \to B prefix (L + \|B\| - L) = B prefix \|B\|$
32		pfxid	$⊢ B \in Word V \to B prefix \|B\| = B$
33	32	adantl	$⊢ (A \in Word V \land B \in Word V) \to B prefix \|B\| = B$
34	33	adantr	$⊢ ((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \to B prefix \|B\| = B$
35	34	3ad2ant1	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land \neg L + \|B\| \leq L \land \neg L \leq M) \to B prefix \|B\| = B$
36	31 35	eqtr2d	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land \neg L + \|B\| \leq L \land \neg L \leq M) \to B = B prefix (L + \|B\| - L)$
37	36	oveq2d	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land \neg L + \|B\| \leq L \land \neg L \leq M) \to (A substr ⟨M, L⟩) ++ B = (A substr ⟨M, L⟩) ++ (B prefix (L + \|B\| - L))$
38	28 37	eqtrd	$⊢ (((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \land \neg L + \|B\| \leq L \land \neg L \leq M) \to if (L \leq 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 \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \to if (L \leq M, B substr ⟨M - L, \|B\|⟩, (A substr ⟨M, L⟩) ++ B) = if (L + \|B\| \leq L, A substr ⟨M, L + \|B\|⟩, if (L \leq M, B substr ⟨M - L, L + \|B\| - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (L + \|B\| - L))))$
40	8 39	eqtr4d	$⊢ ((A \in Word V \land B \in Word V) \land M \in (0 \dots L + \|B\|)) \to (A ++ B) substr ⟨M, L + \|B\|⟩ = if (L \leq M, B substr ⟨M - L, \|B\|⟩, (A substr ⟨M, L⟩) ++ B)$
41	40	ex	$⊢ (A \in Word V \land B \in Word V) \to (M \in (0 \dots L + \|B\|) \to (A ++ B) substr ⟨M, L + \|B\|⟩ = if (L \leq M, B substr ⟨M - L, \|B\|⟩, (A substr ⟨M, L⟩) ++ B))$

Metamath Proof Explorer

Theorem swrdccat3b

Proof