swrdccat

Description: The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018)

		Ref	Expression
	Hypothesis	swrdccatin2.l	$⊢ L = \|A\|$
	Assertion	swrdccat	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (A ++ B) substr ⟨M, N⟩ = (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩))$

Proof

Step	Hyp	Ref	Expression
1		swrdccatin2.l	$⊢ L = \|A\|$
2	1	pfxccat3	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (A ++ B) substr ⟨M, N⟩ = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L)))))$
3	2	imp	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (A ++ B) substr ⟨M, N⟩ = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L))))$
4		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
5	4	adantr	$⊢ (A \in Word V \land B \in Word V) \to \|A\| \in ℕ_{0}$
6	1	eqcomi	$⊢ \|A\| = L$
7	6	eleq1i	$⊢ \|A\| \in ℕ_{0} \leftrightarrow L \in ℕ_{0}$
8		elfz2nn0	$⊢ M \in (0 \dots N) \leftrightarrow (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
9		iftrue	$⊢ N \leq L \to if (N \leq L, N, L) = N$
10	9	adantl	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to if (N \leq L, N, L) = N$
11	10	opeq2d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to ⟨M, if (N \leq L, N, L)⟩ = ⟨M, N⟩$
12	11	oveq2d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to A substr ⟨M, if (N \leq L, N, L)⟩ = A substr ⟨M, N⟩$
13		iftrue	$⊢ 0 \leq M - L \to if (0 \leq M - L, M - L, 0) = M - L$
14	13	opeq1d	$⊢ 0 \leq M - L \to ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = ⟨M - L, N - L⟩$
15	14	oveq2d	$⊢ 0 \leq M - L \to B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = B substr ⟨M - L, N - L⟩$
16	15	adantr	$⊢ (0 \leq M - L \land (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L)) \to B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = B substr ⟨M - L, N - L⟩$
17		simpr	$⊢ (A \in Word V \land B \in Word V) \to B \in Word V$
18		nn0z	$⊢ L \in ℕ_{0} \to L \in ℤ$
19		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
20	19	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M \in ℤ$
21		zsubcl	$⊢ (M \in ℤ \land L \in ℤ) \to M - L \in ℤ$
22	20 21	sylan	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℤ) \to M - L \in ℤ$
23		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
24	23	adantl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to N \in ℤ$
25		zsubcl	$⊢ (N \in ℤ \land L \in ℤ) \to N - L \in ℤ$
26	24 25	sylan	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℤ) \to N - L \in ℤ$
27	22 26	jca	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℤ) \to (M - L \in ℤ \land N - L \in ℤ)$
28	18 27	sylan2	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to (M - L \in ℤ \land N - L \in ℤ)$
29	17 28	anim12i	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (B \in Word V \land (M - L \in ℤ \land N - L \in ℤ))$
30		3anass	$⊢ (B \in Word V \land M - L \in ℤ \land N - L \in ℤ) \leftrightarrow (B \in Word V \land (M - L \in ℤ \land N - L \in ℤ))$
31	29 30	sylibr	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (B \in Word V \land M - L \in ℤ \land N - L \in ℤ)$
32	31	ad2antrl	$⊢ (0 \leq M - L \land (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L)) \to (B \in Word V \land M - L \in ℤ \land N - L \in ℤ)$
33		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
34		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
35	33 34	anim12i	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \in ℝ \land N \in ℝ)$
36		nn0re	$⊢ L \in ℕ_{0} \to L \in ℝ$
37		subge0	$⊢ (M \in ℝ \land L \in ℝ) \to (0 \leq M - L \leftrightarrow L \leq M)$
38	37	adantlr	$⊢ ((M \in ℝ \land N \in ℝ) \land L \in ℝ) \to (0 \leq M - L \leftrightarrow L \leq M)$
39		simpr	$⊢ (M \in ℝ \land N \in ℝ) \to N \in ℝ$
40	39	adantr	$⊢ ((M \in ℝ \land N \in ℝ) \land L \in ℝ) \to N \in ℝ$
41		simpr	$⊢ ((M \in ℝ \land N \in ℝ) \land L \in ℝ) \to L \in ℝ$
42		simpl	$⊢ (M \in ℝ \land N \in ℝ) \to M \in ℝ$
43	42	adantr	$⊢ ((M \in ℝ \land N \in ℝ) \land L \in ℝ) \to M \in ℝ$
44		letr	$⊢ (N \in ℝ \land L \in ℝ \land M \in ℝ) \to ((N \leq L \land L \leq M) \to N \leq M)$
45	40 41 43 44	syl3anc	$⊢ ((M \in ℝ \land N \in ℝ) \land L \in ℝ) \to ((N \leq L \land L \leq M) \to N \leq M)$
46	45	expcomd	$⊢ ((M \in ℝ \land N \in ℝ) \land L \in ℝ) \to (L \leq M \to (N \leq L \to N \leq M))$
47	38 46	sylbid	$⊢ ((M \in ℝ \land N \in ℝ) \land L \in ℝ) \to (0 \leq M - L \to (N \leq L \to N \leq M))$
48	47	com23	$⊢ ((M \in ℝ \land N \in ℝ) \land L \in ℝ) \to (N \leq L \to (0 \leq M - L \to N \leq M))$
49	35 36 48	syl2an	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to (N \leq L \to (0 \leq M - L \to N \leq M))$
50	49	adantl	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (N \leq L \to (0 \leq M - L \to N \leq M))$
51	50	imp	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to (0 \leq M - L \to N \leq M)$
52	51	impcom	$⊢ (0 \leq M - L \land (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L)) \to N \leq M$
53	34	adantl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to N \in ℝ$
54	53	adantr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to N \in ℝ$
55	33	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M \in ℝ$
56	55	adantr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to M \in ℝ$
57	36	adantl	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to L \in ℝ$
58	54 56 57	3jca	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to (N \in ℝ \land M \in ℝ \land L \in ℝ)$
59	58	adantl	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (N \in ℝ \land M \in ℝ \land L \in ℝ)$
60	59	ad2antrl	$⊢ (0 \leq M - L \land (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L)) \to (N \in ℝ \land M \in ℝ \land L \in ℝ)$
61		lesub1	$⊢ (N \in ℝ \land M \in ℝ \land L \in ℝ) \to (N \leq M \leftrightarrow N - L \leq M - L)$
62	60 61	syl	$⊢ (0 \leq M - L \land (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L)) \to (N \leq M \leftrightarrow N - L \leq M - L)$
63	52 62	mpbid	$⊢ (0 \leq M - L \land (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L)) \to N - L \leq M - L$
64		swrdlend	$⊢ (B \in Word V \land M - L \in ℤ \land N - L \in ℤ) \to (N - L \leq M - L \to B substr ⟨M - L, N - L⟩ = \emptyset)$
65	32 63 64	sylc	$⊢ (0 \leq M - L \land (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L)) \to B substr ⟨M - L, N - L⟩ = \emptyset$
66	16 65	eqtrd	$⊢ (0 \leq M - L \land (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L)) \to B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = \emptyset$
67		iffalse	$⊢ \neg 0 \leq M - L \to if (0 \leq M - L, M - L, 0) = 0$
68	67	opeq1d	$⊢ \neg 0 \leq M - L \to ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = ⟨0, N - L⟩$
69	68	oveq2d	$⊢ \neg 0 \leq M - L \to B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = B substr ⟨0, N - L⟩$
70	17	adantr	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to B \in Word V$
71	70	adantr	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to B \in Word V$
72		0zd	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to 0 \in ℤ$
73	24 18 25	syl2an	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to N - L \in ℤ$
74	73	adantl	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to N - L \in ℤ$
75	74	adantr	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to N - L \in ℤ$
76	71 72 75	3jca	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to (B \in Word V \land 0 \in ℤ \land N - L \in ℤ)$
77	53 36	anim12i	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to (N \in ℝ \land L \in ℝ)$
78	77	adantl	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (N \in ℝ \land L \in ℝ)$
79		suble0	$⊢ (N \in ℝ \land L \in ℝ) \to (N - L \leq 0 \leftrightarrow N \leq L)$
80	78 79	syl	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (N - L \leq 0 \leftrightarrow N \leq L)$
81	80	biimpar	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to N - L \leq 0$
82		swrdlend	$⊢ (B \in Word V \land 0 \in ℤ \land N - L \in ℤ) \to (N - L \leq 0 \to B substr ⟨0, N - L⟩ = \emptyset)$
83	76 81 82	sylc	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to B substr ⟨0, N - L⟩ = \emptyset$
84	69 83	sylan9eq	$⊢ (\neg 0 \leq M - L \land (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L)) \to B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = \emptyset$
85	66 84	pm2.61ian	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = \emptyset$
86	12 85	oveq12d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = (A substr ⟨M, N⟩) ++ \emptyset$
87		swrdcl	$⊢ A \in Word V \to A substr ⟨M, N⟩ \in Word V$
88		ccatrid	$⊢ A substr ⟨M, N⟩ \in Word V \to (A substr ⟨M, N⟩) ++ \emptyset = A substr ⟨M, N⟩$
89	87 88	syl	$⊢ A \in Word V \to (A substr ⟨M, N⟩) ++ \emptyset = A substr ⟨M, N⟩$
90	89	adantr	$⊢ (A \in Word V \land B \in Word V) \to (A substr ⟨M, N⟩) ++ \emptyset = A substr ⟨M, N⟩$
91	90	adantr	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (A substr ⟨M, N⟩) ++ \emptyset = A substr ⟨M, N⟩$
92	91	adantr	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to (A substr ⟨M, N⟩) ++ \emptyset = A substr ⟨M, N⟩$
93	86 92	eqtrd	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land N \leq L) \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = A substr ⟨M, N⟩$
94		iffalse	$⊢ \neg N \leq L \to if (N \leq L, N, L) = L$
95	94	3ad2ant2	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land L \leq M) \to if (N \leq L, N, L) = L$
96	95	opeq2d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land L \leq M) \to ⟨M, if (N \leq L, N, L)⟩ = ⟨M, L⟩$
97	96	oveq2d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land L \leq M) \to A substr ⟨M, if (N \leq L, N, L)⟩ = A substr ⟨M, L⟩$
98		simpl	$⊢ (A \in Word V \land B \in Word V) \to A \in Word V$
99	98 20 18	3anim123i	$⊢ ((A \in Word V \land B \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to (A \in Word V \land M \in ℤ \land L \in ℤ)$
100	99	3expb	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (A \in Word V \land M \in ℤ \land L \in ℤ)$
101		swrdlend	$⊢ (A \in Word V \land M \in ℤ \land L \in ℤ) \to (L \leq M \to A substr ⟨M, L⟩ = \emptyset)$
102	100 101	syl	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (L \leq M \to A substr ⟨M, L⟩ = \emptyset)$
103	102	imp	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land L \leq M) \to A substr ⟨M, L⟩ = \emptyset$
104	103	3adant2	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land L \leq M) \to A substr ⟨M, L⟩ = \emptyset$
105	97 104	eqtrd	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land L \leq M) \to A substr ⟨M, if (N \leq L, N, L)⟩ = \emptyset$
106	55 36 37	syl2an	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to (0 \leq M - L \leftrightarrow L \leq M)$
107	106	biimprd	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to (L \leq M \to 0 \leq M - L)$
108	107	adantl	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (L \leq M \to 0 \leq M - L)$
109	108	imp	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land L \leq M) \to 0 \leq M - L$
110	109	3adant2	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land L \leq M) \to 0 \leq M - L$
111	110 14	syl	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land L \leq M) \to ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = ⟨M - L, N - L⟩$
112	111	oveq2d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land L \leq M) \to B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = B substr ⟨M - L, N - L⟩$
113	105 112	oveq12d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land L \leq M) \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = \emptyset ++ (B substr ⟨M - L, N - L⟩)$
114		swrdcl	$⊢ B \in Word V \to B substr ⟨M - L, N - L⟩ \in Word V$
115	114	adantl	$⊢ (A \in Word V \land B \in Word V) \to B substr ⟨M - L, N - L⟩ \in Word V$
116		ccatlid	$⊢ B substr ⟨M - L, N - L⟩ \in Word V \to \emptyset ++ (B substr ⟨M - L, N - L⟩) = B substr ⟨M - L, N - L⟩$
117	115 116	syl	$⊢ (A \in Word V \land B \in Word V) \to \emptyset ++ (B substr ⟨M - L, N - L⟩) = B substr ⟨M - L, N - L⟩$
118	117	adantr	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to \emptyset ++ (B substr ⟨M - L, N - L⟩) = B substr ⟨M - L, N - L⟩$
119	118	3ad2ant1	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land L \leq M) \to \emptyset ++ (B substr ⟨M - L, N - L⟩) = B substr ⟨M - L, N - L⟩$
120	113 119	eqtrd	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land L \leq M) \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = B substr ⟨M - L, N - L⟩$
121	94	3ad2ant2	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to if (N \leq L, N, L) = L$
122	121	opeq2d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to ⟨M, if (N \leq L, N, L)⟩ = ⟨M, L⟩$
123	122	oveq2d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to A substr ⟨M, if (N \leq L, N, L)⟩ = A substr ⟨M, L⟩$
124	33 36 37	syl2an	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (0 \leq M - L \leftrightarrow L \leq M)$
125	124	adantlr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to (0 \leq M - L \leftrightarrow L \leq M)$
126	125	adantl	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (0 \leq M - L \leftrightarrow L \leq M)$
127	126	biimpd	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (0 \leq M - L \to L \leq M)$
128	127	con3dimp	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg L \leq M) \to \neg 0 \leq M - L$
129	128	3adant2	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to \neg 0 \leq M - L$
130	129 67	syl	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to if (0 \leq M - L, M - L, 0) = 0$
131	130	opeq1d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = ⟨0, N - L⟩$
132	131	oveq2d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = B substr ⟨0, N - L⟩$
133	70	3ad2ant1	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to B \in Word V$
134		simplrr	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L) \to L \in ℕ_{0}$
135		simprlr	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to N \in ℕ_{0}$
136	135	adantr	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L) \to N \in ℕ_{0}$
137		ltnle	$⊢ (L \in ℝ \land N \in ℝ) \to (L < N \leftrightarrow \neg N \leq L)$
138		ltle	$⊢ (L \in ℝ \land N \in ℝ) \to (L < N \to L \leq N)$
139	137 138	sylbird	$⊢ (L \in ℝ \land N \in ℝ) \to (\neg N \leq L \to L \leq N)$
140	36 53 139	syl2anr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0}) \to (\neg N \leq L \to L \leq N)$
141	140	adantl	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (\neg N \leq L \to L \leq N)$
142	141	imp	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L) \to L \leq N$
143		nn0sub2	$⊢ (L \in ℕ_{0} \land N \in ℕ_{0} \land L \leq N) \to N - L \in ℕ_{0}$
144	134 136 142 143	syl3anc	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L) \to N - L \in ℕ_{0}$
145	144	3adant3	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to N - L \in ℕ_{0}$
146	133 145	jca	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to (B \in Word V \land N - L \in ℕ_{0})$
147		pfxval	$⊢ (B \in Word V \land N - L \in ℕ_{0}) \to B prefix (N - L) = B substr ⟨0, N - L⟩$
148	146 147	syl	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to B prefix (N - L) = B substr ⟨0, N - L⟩$
149	132 148	eqtr4d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩ = B prefix (N - L)$
150	123 149	oveq12d	$⊢ (((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \land \neg N \leq L \land \neg L \leq M) \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = (A substr ⟨M, L⟩) ++ (B prefix (N - L))$
151	93 120 150	2if2	$⊢ ((A \in Word V \land B \in Word V) \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land L \in ℕ_{0})) \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L))))$
152	151	exp32	$⊢ (A \in Word V \land B \in Word V) \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to (L \in ℕ_{0} \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L))))))$
153	152	com12	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((A \in Word V \land B \in Word V) \to (L \in ℕ_{0} \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L))))))$
154	153	3adant3	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to ((A \in Word V \land B \in Word V) \to (L \in ℕ_{0} \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L))))))$
155	8 154	sylbi	$⊢ M \in (0 \dots N) \to ((A \in Word V \land B \in Word V) \to (L \in ℕ_{0} \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L))))))$
156	155	adantr	$⊢ (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to ((A \in Word V \land B \in Word V) \to (L \in ℕ_{0} \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L))))))$
157	156	com13	$⊢ L \in ℕ_{0} \to ((A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L))))))$
158	7 157	sylbi	$⊢ \|A\| \in ℕ_{0} \to ((A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L))))))$
159	5 158	mpcom	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L)))))$
160	159	imp	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩) = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L))))$
161	3 160	eqtr4d	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (A ++ B) substr ⟨M, N⟩ = (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩)$
162	161	ex	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (A ++ B) substr ⟨M, N⟩ = (A substr ⟨M, if (N \leq L, N, L)⟩) ++ (B substr ⟨if (0 \leq M - L, M - L, 0), N - L⟩))$

Metamath Proof Explorer

Theorem swrdccat

Proof