pfxccatin12lem2

Description: Lemma 2 for pfxccatin12 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 9-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		swrdccatin2.l	$⊢ L = \|A\|$
2	1	pfxccatin12lem2c	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (A ++ B \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A ++ B\|))$
3		simprl	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K \in (0 ..^N - M)$
4		swrdfv	$⊢ ((A ++ B \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A ++ B\|)) \land K \in (0 ..^N - M)) \to ((A ++ B) substr ⟨M, N⟩) (K) = (A ++ B) (K + M)$
5	2 3 4	syl2an2r	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to ((A ++ B) substr ⟨M, N⟩) (K) = (A ++ B) (K + M)$
6		elfzoelz	$⊢ K \in (0 ..^N - M) \to K \in ℤ$
7		elfz2nn0	$⊢ M \in (0 \dots L) \leftrightarrow (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L)$
8		nn0cn	$⊢ M \in ℕ_{0} \to M \in ℂ$
9		nn0cn	$⊢ L \in ℕ_{0} \to L \in ℂ$
10	8 9	anim12i	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (M \in ℂ \land L \in ℂ)$
11		zcn	$⊢ K \in ℤ \to K \in ℂ$
12		subcl	$⊢ (L \in ℂ \land M \in ℂ) \to L - M \in ℂ$
13	12	ancoms	$⊢ (M \in ℂ \land L \in ℂ) \to L - M \in ℂ$
14	13	anim1ci	$⊢ ((M \in ℂ \land L \in ℂ) \land K \in ℂ) \to (K \in ℂ \land L - M \in ℂ)$
15		subcl	$⊢ (K \in ℂ \land L - M \in ℂ) \to K - (L - M) \in ℂ$
16	14 15	syl	$⊢ ((M \in ℂ \land L \in ℂ) \land K \in ℂ) \to K - (L - M) \in ℂ$
17	16	addridd	$⊢ ((M \in ℂ \land L \in ℂ) \land K \in ℂ) \to K - (L - M) + 0 = K - (L - M)$
18		simpr	$⊢ ((M \in ℂ \land L \in ℂ) \land K \in ℂ) \to K \in ℂ$
19		simplr	$⊢ ((M \in ℂ \land L \in ℂ) \land K \in ℂ) \to L \in ℂ$
20		simpll	$⊢ ((M \in ℂ \land L \in ℂ) \land K \in ℂ) \to M \in ℂ$
21	18 19 20	subsub3d	$⊢ ((M \in ℂ \land L \in ℂ) \land K \in ℂ) \to K - (L - M) = K + M - L$
22	17 21	eqtr2d	$⊢ ((M \in ℂ \land L \in ℂ) \land K \in ℂ) \to K + M - L = K - (L - M) + 0$
23	10 11 22	syl2an	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0}) \land K \in ℤ) \to K + M - L = K - (L - M) + 0$
24		oveq2	$⊢ \|A\| = L \to K + M - \|A\| = K + M - L$
25	24	eqcoms	$⊢ L = \|A\| \to K + M - \|A\| = K + M - L$
26	25	eqeq1d	$⊢ L = \|A\| \to (K + M - \|A\| = K - (L - M) + 0 \leftrightarrow K + M - L = K - (L - M) + 0)$
27	23 26	imbitrrid	$⊢ L = \|A\| \to (((M \in ℕ_{0} \land L \in ℕ_{0}) \land K \in ℤ) \to K + M - \|A\| = K - (L - M) + 0)$
28	1 27	ax-mp	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0}) \land K \in ℤ) \to K + M - \|A\| = K - (L - M) + 0$
29	28	ex	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (K \in ℤ \to K + M - \|A\| = K - (L - M) + 0)$
30	29	3adant3	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (K \in ℤ \to K + M - \|A\| = K - (L - M) + 0)$
31	7 30	sylbi	$⊢ M \in (0 \dots L) \to (K \in ℤ \to K + M - \|A\| = K - (L - M) + 0)$
32	31	ad2antrl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (K \in ℤ \to K + M - \|A\| = K - (L - M) + 0)$
33	6 32	syl5com	$⊢ K \in (0 ..^N - M) \to (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to K + M - \|A\| = K - (L - M) + 0)$
34	33	adantr	$⊢ (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to K + M - \|A\| = K - (L - M) + 0)$
35	34	impcom	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K + M - \|A\| = K - (L - M) + 0$
36	35	fveq2d	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to B (K + M - \|A\|) = B (K - (L - M) + 0)$
37		simpll	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to (A \in Word V \land B \in Word V)$
38		pfxccatin12lem2a	$⊢ (M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to ((K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to K + M \in (L ..^L + \|B\|))$
39	38	adantl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to ((K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to K + M \in (L ..^L + \|B\|))$
40	39	imp	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K + M \in (L ..^L + \|B\|)$
41		id	$⊢ \|A\| = L \to \|A\| = L$
42		oveq1	$⊢ \|A\| = L \to \|A\| + \|B\| = L + \|B\|$
43	41 42	oveq12d	$⊢ \|A\| = L \to (\|A\| ..^\|A\| + \|B\|) = (L ..^L + \|B\|)$
44	43	eleq2d	$⊢ \|A\| = L \to (K + M \in (\|A\| ..^\|A\| + \|B\|) \leftrightarrow K + M \in (L ..^L + \|B\|))$
45	44	eqcoms	$⊢ L = \|A\| \to (K + M \in (\|A\| ..^\|A\| + \|B\|) \leftrightarrow K + M \in (L ..^L + \|B\|))$
46	1 45	ax-mp	$⊢ K + M \in (\|A\| ..^\|A\| + \|B\|) \leftrightarrow K + M \in (L ..^L + \|B\|)$
47	40 46	sylibr	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K + M \in (\|A\| ..^\|A\| + \|B\|)$
48		df-3an	$⊢ (A \in Word V \land B \in Word V \land K + M \in (\|A\| ..^\|A\| + \|B\|)) \leftrightarrow ((A \in Word V \land B \in Word V) \land K + M \in (\|A\| ..^\|A\| + \|B\|))$
49	37 47 48	sylanbrc	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to (A \in Word V \land B \in Word V \land K + M \in (\|A\| ..^\|A\| + \|B\|))$
50		ccatval2	$⊢ (A \in Word V \land B \in Word V \land K + M \in (\|A\| ..^\|A\| + \|B\|)) \to (A ++ B) (K + M) = B (K + M - \|A\|)$
51	49 50	syl	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to (A ++ B) (K + M) = B (K + M - \|A\|)$
52		simplr	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to B \in Word V$
53	52	adantr	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to B \in Word V$
54		lencl	$⊢ B \in Word V \to \|B\| \in ℕ_{0}$
55		elfzel2	$⊢ M \in (0 \dots L) \to L \in ℤ$
56		zsubcl	$⊢ (N \in ℤ \land L \in ℤ) \to N - L \in ℤ$
57	56	ancoms	$⊢ (L \in ℤ \land N \in ℤ) \to N - L \in ℤ$
58	57	adantr	$⊢ ((L \in ℤ \land N \in ℤ) \land L \leq N) \to N - L \in ℤ$
59		zre	$⊢ N \in ℤ \to N \in ℝ$
60		zre	$⊢ L \in ℤ \to L \in ℝ$
61		subge0	$⊢ (N \in ℝ \land L \in ℝ) \to (0 \leq N - L \leftrightarrow L \leq N)$
62	59 60 61	syl2anr	$⊢ (L \in ℤ \land N \in ℤ) \to (0 \leq N - L \leftrightarrow L \leq N)$
63	62	biimprd	$⊢ (L \in ℤ \land N \in ℤ) \to (L \leq N \to 0 \leq N - L)$
64	63	imp	$⊢ ((L \in ℤ \land N \in ℤ) \land L \leq N) \to 0 \leq N - L$
65		elnn0z	$⊢ N - L \in ℕ_{0} \leftrightarrow (N - L \in ℤ \land 0 \leq N - L)$
66	58 64 65	sylanbrc	$⊢ ((L \in ℤ \land N \in ℤ) \land L \leq N) \to N - L \in ℕ_{0}$
67	66	expcom	$⊢ L \leq N \to ((L \in ℤ \land N \in ℤ) \to N - L \in ℕ_{0})$
68	67	adantr	$⊢ (L \leq N \land N \leq L + \|B\|) \to ((L \in ℤ \land N \in ℤ) \to N - L \in ℕ_{0})$
69	68	expcomd	$⊢ (L \leq N \land N \leq L + \|B\|) \to (N \in ℤ \to (L \in ℤ \to N - L \in ℕ_{0}))$
70	69	com12	$⊢ N \in ℤ \to ((L \leq N \land N \leq L + \|B\|) \to (L \in ℤ \to N - L \in ℕ_{0}))$
71	70	3ad2ant3	$⊢ (L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \to ((L \leq N \land N \leq L + \|B\|) \to (L \in ℤ \to N - L \in ℕ_{0}))$
72	71	imp	$⊢ ((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq L + \|B\|)) \to (L \in ℤ \to N - L \in ℕ_{0})$
73	72	com12	$⊢ L \in ℤ \to (((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq L + \|B\|)) \to N - L \in ℕ_{0})$
74	73	adantr	$⊢ (L \in ℤ \land \|B\| \in ℕ_{0}) \to (((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq L + \|B\|)) \to N - L \in ℕ_{0})$
75	74	imp	$⊢ ((L \in ℤ \land \|B\| \in ℕ_{0}) \land ((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq L + \|B\|))) \to N - L \in ℕ_{0}$
76		simplr	$⊢ ((L \in ℤ \land \|B\| \in ℕ_{0}) \land ((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq L + \|B\|))) \to \|B\| \in ℕ_{0}$
77	59	3ad2ant3	$⊢ (L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \to N \in ℝ$
78	77	adantl	$⊢ ((L \in ℤ \land \|B\| \in ℕ_{0}) \land (L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ)) \to N \in ℝ$
79	60	adantr	$⊢ (L \in ℤ \land \|B\| \in ℕ_{0}) \to L \in ℝ$
80	79	adantr	$⊢ ((L \in ℤ \land \|B\| \in ℕ_{0}) \land (L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ)) \to L \in ℝ$
81		nn0re	$⊢ \|B\| \in ℕ_{0} \to \|B\| \in ℝ$
82	81	adantl	$⊢ (L \in ℤ \land \|B\| \in ℕ_{0}) \to \|B\| \in ℝ$
83	82	adantr	$⊢ ((L \in ℤ \land \|B\| \in ℕ_{0}) \land (L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ)) \to \|B\| \in ℝ$
84		lesubadd2	$⊢ (N \in ℝ \land L \in ℝ \land \|B\| \in ℝ) \to (N - L \leq \|B\| \leftrightarrow N \leq L + \|B\|)$
85	84	biimprd	$⊢ (N \in ℝ \land L \in ℝ \land \|B\| \in ℝ) \to (N \leq L + \|B\| \to N - L \leq \|B\|)$
86	78 80 83 85	syl3anc	$⊢ ((L \in ℤ \land \|B\| \in ℕ_{0}) \land (L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ)) \to (N \leq L + \|B\| \to N - L \leq \|B\|)$
87	86	ex	$⊢ (L \in ℤ \land \|B\| \in ℕ_{0}) \to ((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \to (N \leq L + \|B\| \to N - L \leq \|B\|))$
88	87	com13	$⊢ N \leq L + \|B\| \to ((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \to ((L \in ℤ \land \|B\| \in ℕ_{0}) \to N - L \leq \|B\|))$
89	88	adantl	$⊢ (L \leq N \land N \leq L + \|B\|) \to ((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \to ((L \in ℤ \land \|B\| \in ℕ_{0}) \to N - L \leq \|B\|))$
90	89	impcom	$⊢ ((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq L + \|B\|)) \to ((L \in ℤ \land \|B\| \in ℕ_{0}) \to N - L \leq \|B\|)$
91	90	impcom	$⊢ ((L \in ℤ \land \|B\| \in ℕ_{0}) \land ((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq L + \|B\|))) \to N - L \leq \|B\|$
92	75 76 91	3jca	$⊢ ((L \in ℤ \land \|B\| \in ℕ_{0}) \land ((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq L + \|B\|))) \to (N - L \in ℕ_{0} \land \|B\| \in ℕ_{0} \land N - L \leq \|B\|)$
93	92	ex	$⊢ (L \in ℤ \land \|B\| \in ℕ_{0}) \to (((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq L + \|B\|)) \to (N - L \in ℕ_{0} \land \|B\| \in ℕ_{0} \land N - L \leq \|B\|))$
94		elfz2	$⊢ N \in (L \dots L + \|B\|) \leftrightarrow ((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq L + \|B\|))$
95		elfz2nn0	$⊢ N - L \in (0 \dots \|B\|) \leftrightarrow (N - L \in ℕ_{0} \land \|B\| \in ℕ_{0} \land N - L \leq \|B\|)$
96	93 94 95	3imtr4g	$⊢ (L \in ℤ \land \|B\| \in ℕ_{0}) \to (N \in (L \dots L + \|B\|) \to N - L \in (0 \dots \|B\|))$
97	96	ex	$⊢ L \in ℤ \to (\|B\| \in ℕ_{0} \to (N \in (L \dots L + \|B\|) \to N - L \in (0 \dots \|B\|)))$
98	97	com23	$⊢ L \in ℤ \to (N \in (L \dots L + \|B\|) \to (\|B\| \in ℕ_{0} \to N - L \in (0 \dots \|B\|)))$
99	55 98	syl	$⊢ M \in (0 \dots L) \to (N \in (L \dots L + \|B\|) \to (\|B\| \in ℕ_{0} \to N - L \in (0 \dots \|B\|)))$
100	99	imp	$⊢ (M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to (\|B\| \in ℕ_{0} \to N - L \in (0 \dots \|B\|))$
101	54 100	syl5com	$⊢ B \in Word V \to ((M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to N - L \in (0 \dots \|B\|))$
102	101	adantl	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to N - L \in (0 \dots \|B\|))$
103	102	imp	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to N - L \in (0 \dots \|B\|)$
104	103	adantr	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to N - L \in (0 \dots \|B\|)$
105		pfxccatin12lem1	$⊢ (M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to ((K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to K - (L - M) \in (0 ..^N - L))$
106	105	adantl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to ((K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to K - (L - M) \in (0 ..^N - L))$
107	106	imp	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K - (L - M) \in (0 ..^N - L)$
108		pfxfv	$⊢ (B \in Word V \land N - L \in (0 \dots \|B\|) \land K - (L - M) \in (0 ..^N - L)) \to (B prefix (N - L)) (K - (L - M)) = B (K - (L - M))$
109	53 104 107 108	syl3anc	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to (B prefix (N - L)) (K - (L - M)) = B (K - (L - M))$
110	6	zcnd	$⊢ K \in (0 ..^N - M) \to K \in ℂ$
111	110	ad2antrl	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K \in ℂ$
112	55	zcnd	$⊢ M \in (0 \dots L) \to L \in ℂ$
113	112	ad2antrl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to L \in ℂ$
114	113	adantr	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to L \in ℂ$
115		elfzelz	$⊢ M \in (0 \dots L) \to M \in ℤ$
116	115	zcnd	$⊢ M \in (0 \dots L) \to M \in ℂ$
117	116	ad2antrl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to M \in ℂ$
118	117	adantr	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to M \in ℂ$
119	114 118	subcld	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to L - M \in ℂ$
120	111 119	subcld	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K - (L - M) \in ℂ$
121	120	addridd	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K - (L - M) + 0 = K - (L - M)$
122	121	eqcomd	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K - (L - M) = K - (L - M) + 0$
123	122	fveq2d	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to B (K - (L - M)) = B (K - (L - M) + 0)$
124	109 123	eqtrd	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to (B prefix (N - L)) (K - (L - M)) = B (K - (L - M) + 0)$
125	36 51 124	3eqtr4d	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to (A ++ B) (K + M) = (B prefix (N - L)) (K - (L - M))$
126		simpll	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to A \in Word V$
127		simprl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to M \in (0 \dots L)$
128		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
129		elnn0uz	$⊢ \|A\| \in ℕ_{0} \leftrightarrow \|A\| \in ℤ_{\geq 0}$
130		eluzfz2	$⊢ \|A\| \in ℤ_{\geq 0} \to \|A\| \in (0 \dots \|A\|)$
131	129 130	sylbi	$⊢ \|A\| \in ℕ_{0} \to \|A\| \in (0 \dots \|A\|)$
132	1 131	eqeltrid	$⊢ \|A\| \in ℕ_{0} \to L \in (0 \dots \|A\|)$
133	128 132	syl	$⊢ A \in Word V \to L \in (0 \dots \|A\|)$
134	133	adantr	$⊢ (A \in Word V \land B \in Word V) \to L \in (0 \dots \|A\|)$
135	134	adantr	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to L \in (0 \dots \|A\|)$
136	126 127 135	3jca	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (A \in Word V \land M \in (0 \dots L) \land L \in (0 \dots \|A\|))$
137	136	adantr	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to (A \in Word V \land M \in (0 \dots L) \land L \in (0 \dots \|A\|))$
138		swrdlen	$⊢ (A \in Word V \land M \in (0 \dots L) \land L \in (0 \dots \|A\|)) \to \|A substr ⟨M, L⟩\| = L - M$
139	137 138	syl	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to \|A substr ⟨M, L⟩\| = L - M$
140	139	eqcomd	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to L - M = \|A substr ⟨M, L⟩\|$
141	140	oveq2d	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K - (L - M) = K - \|A substr ⟨M, L⟩\|$
142	141	fveq2d	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to (B prefix (N - L)) (K - (L - M)) = (B prefix (N - L)) (K - \|A substr ⟨M, L⟩\|)$
143	5 125 142	3eqtrd	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to ((A ++ B) substr ⟨M, N⟩) (K) = (B prefix (N - L)) (K - \|A substr ⟨M, L⟩\|)$
144	143	ex	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to ((K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to ((A ++ B) substr ⟨M, N⟩) (K) = (B prefix (N - L)) (K - \|A substr ⟨M, L⟩\|))$

Metamath Proof Explorer

Theorem pfxccatin12lem2

Proof