pfxccat3a

Description: A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018) (Revised by AV, 10-May-2020)

	Ref	Expression
Hypotheses	swrdccatin2.l	$⊢ L = \|A\|$
	pfxccatpfx2.m	$⊢ M = \|B\|$
Assertion	pfxccat3a	$⊢ (A \in Word V \land B \in Word V) \to (N \in (0 \dots L + M) \to (A ++ B) prefix N = if (N \leq L, A prefix N, A ++ (B prefix (N - L))))$

Proof

Step	Hyp	Ref	Expression
1		swrdccatin2.l	$⊢ L = \|A\|$
2		pfxccatpfx2.m	$⊢ M = \|B\|$
3		simprl	$⊢ (N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to (A \in Word V \land B \in Word V)$
4		elfznn0	$⊢ N \in (0 \dots L + M) \to N \in ℕ_{0}$
5	4	adantl	$⊢ ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M)) \to N \in ℕ_{0}$
6	5	adantl	$⊢ (N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to N \in ℕ_{0}$
7		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
8	1 7	eqeltrid	$⊢ A \in Word V \to L \in ℕ_{0}$
9	8	adantr	$⊢ (A \in Word V \land B \in Word V) \to L \in ℕ_{0}$
10	9	adantr	$⊢ ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M)) \to L \in ℕ_{0}$
11	10	adantl	$⊢ (N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to L \in ℕ_{0}$
12		simpl	$⊢ (N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to N \leq L$
13		elfz2nn0	$⊢ N \in (0 \dots L) \leftrightarrow (N \in ℕ_{0} \land L \in ℕ_{0} \land N \leq L)$
14	6 11 12 13	syl3anbrc	$⊢ (N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to N \in (0 \dots L)$
15		df-3an	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots L)) \leftrightarrow ((A \in Word V \land B \in Word V) \land N \in (0 \dots L))$
16	3 14 15	sylanbrc	$⊢ (N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to (A \in Word V \land B \in Word V \land N \in (0 \dots L))$
17	1	pfxccatpfx1	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots L)) \to (A ++ B) prefix N = A prefix N$
18	16 17	syl	$⊢ (N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to (A ++ B) prefix N = A prefix N$
19		iftrue	$⊢ N \leq L \to if (N \leq L, A prefix N, A ++ (B prefix (N - L))) = A prefix N$
20	19	adantr	$⊢ (N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to if (N \leq L, A prefix N, A ++ (B prefix (N - L))) = A prefix N$
21	18 20	eqtr4d	$⊢ (N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to (A ++ B) prefix N = if (N \leq L, A prefix N, A ++ (B prefix (N - L)))$
22		simprl	$⊢ (\neg N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to (A \in Word V \land B \in Word V)$
23		elfz2nn0	$⊢ N \in (0 \dots L + M) \leftrightarrow (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)$
24	1	eleq1i	$⊢ L \in ℕ_{0} \leftrightarrow \|A\| \in ℕ_{0}$
25		nn0ltp1le	$⊢ (L \in ℕ_{0} \land N \in ℕ_{0}) \to (L < N \leftrightarrow L + 1 \leq N)$
26		nn0re	$⊢ L \in ℕ_{0} \to L \in ℝ$
27		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
28		ltnle	$⊢ (L \in ℝ \land N \in ℝ) \to (L < N \leftrightarrow \neg N \leq L)$
29	26 27 28	syl2an	$⊢ (L \in ℕ_{0} \land N \in ℕ_{0}) \to (L < N \leftrightarrow \neg N \leq L)$
30	25 29	bitr3d	$⊢ (L \in ℕ_{0} \land N \in ℕ_{0}) \to (L + 1 \leq N \leftrightarrow \neg N \leq L)$
31	30	3ad2antr1	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \to (L + 1 \leq N \leftrightarrow \neg N \leq L)$
32		simpr3	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \to N \leq L + M$
33	32	anim1ci	$⊢ ((L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \land L + 1 \leq N) \to (L + 1 \leq N \land N \leq L + M)$
34		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
35	34	3ad2ant1	$⊢ (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M) \to N \in ℤ$
36	35	adantl	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \to N \in ℤ$
37	36	adantr	$⊢ ((L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \land L + 1 \leq N) \to N \in ℤ$
38		peano2nn0	$⊢ L \in ℕ_{0} \to L + 1 \in ℕ_{0}$
39	38	nn0zd	$⊢ L \in ℕ_{0} \to L + 1 \in ℤ$
40	39	adantr	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \to L + 1 \in ℤ$
41	40	adantr	$⊢ ((L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \land L + 1 \leq N) \to L + 1 \in ℤ$
42		nn0z	$⊢ L + M \in ℕ_{0} \to L + M \in ℤ$
43	42	3ad2ant2	$⊢ (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M) \to L + M \in ℤ$
44	43	adantl	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \to L + M \in ℤ$
45	44	adantr	$⊢ ((L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \land L + 1 \leq N) \to L + M \in ℤ$
46		elfz	$⊢ (N \in ℤ \land L + 1 \in ℤ \land L + M \in ℤ) \to (N \in (L + 1 \dots L + M) \leftrightarrow (L + 1 \leq N \land N \leq L + M))$
47	37 41 45 46	syl3anc	$⊢ ((L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \land L + 1 \leq N) \to (N \in (L + 1 \dots L + M) \leftrightarrow (L + 1 \leq N \land N \leq L + M))$
48	33 47	mpbird	$⊢ ((L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \land L + 1 \leq N) \to N \in (L + 1 \dots L + M)$
49	48	ex	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \to (L + 1 \leq N \to N \in (L + 1 \dots L + M))$
50	31 49	sylbird	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M)) \to (\neg N \leq L \to N \in (L + 1 \dots L + M))$
51	50	ex	$⊢ L \in ℕ_{0} \to ((N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M) \to (\neg N \leq L \to N \in (L + 1 \dots L + M)))$
52	24 51	sylbir	$⊢ \|A\| \in ℕ_{0} \to ((N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M) \to (\neg N \leq L \to N \in (L + 1 \dots L + M)))$
53	7 52	syl	$⊢ A \in Word V \to ((N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M) \to (\neg N \leq L \to N \in (L + 1 \dots L + M)))$
54	53	adantr	$⊢ (A \in Word V \land B \in Word V) \to ((N \in ℕ_{0} \land L + M \in ℕ_{0} \land N \leq L + M) \to (\neg N \leq L \to N \in (L + 1 \dots L + M)))$
55	23 54	biimtrid	$⊢ (A \in Word V \land B \in Word V) \to (N \in (0 \dots L + M) \to (\neg N \leq L \to N \in (L + 1 \dots L + M)))$
56	55	imp	$⊢ ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M)) \to (\neg N \leq L \to N \in (L + 1 \dots L + M))$
57	56	impcom	$⊢ (\neg N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to N \in (L + 1 \dots L + M)$
58		df-3an	$⊢ (A \in Word V \land B \in Word V \land N \in (L + 1 \dots L + M)) \leftrightarrow ((A \in Word V \land B \in Word V) \land N \in (L + 1 \dots L + M))$
59	22 57 58	sylanbrc	$⊢ (\neg N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to (A \in Word V \land B \in Word V \land N \in (L + 1 \dots L + M))$
60	1 2	pfxccatpfx2	$⊢ (A \in Word V \land B \in Word V \land N \in (L + 1 \dots L + M)) \to (A ++ B) prefix N = A ++ (B prefix (N - L))$
61	59 60	syl	$⊢ (\neg N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to (A ++ B) prefix N = A ++ (B prefix (N - L))$
62		iffalse	$⊢ \neg N \leq L \to if (N \leq L, A prefix N, A ++ (B prefix (N - L))) = A ++ (B prefix (N - L))$
63	62	adantr	$⊢ (\neg N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to if (N \leq L, A prefix N, A ++ (B prefix (N - L))) = A ++ (B prefix (N - L))$
64	61 63	eqtr4d	$⊢ (\neg N \leq L \land ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M))) \to (A ++ B) prefix N = if (N \leq L, A prefix N, A ++ (B prefix (N - L)))$
65	21 64	pm2.61ian	$⊢ ((A \in Word V \land B \in Word V) \land N \in (0 \dots L + M)) \to (A ++ B) prefix N = if (N \leq L, A prefix N, A ++ (B prefix (N - L)))$
66	65	ex	$⊢ (A \in Word V \land B \in Word V) \to (N \in (0 \dots L + M) \to (A ++ B) prefix N = if (N \leq L, A prefix N, A ++ (B prefix (N - L))))$

Metamath Proof Explorer

Theorem pfxccat3a

Proof