swrdccatin1

Description: The subword of a concatenation of two words within the first of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018)

		Ref	Expression
	Assertion	swrdccatin1	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ \|A\| = 0 \to (0 \dots \|A\|) = (0 \dots 0)$
2	1	eleq2d	$⊢ \|A\| = 0 \to (N \in (0 \dots \|A\|) \leftrightarrow N \in (0 \dots 0))$
3		elfz1eq	$⊢ N \in (0 \dots 0) \to N = 0$
4		elfz1eq	$⊢ M \in (0 \dots 0) \to M = 0$
5		swrd00	$⊢ (A ++ B) substr ⟨0, 0⟩ = \emptyset$
6		swrd00	$⊢ A substr ⟨0, 0⟩ = \emptyset$
7	5 6	eqtr4i	$⊢ (A ++ B) substr ⟨0, 0⟩ = A substr ⟨0, 0⟩$
8		opeq1	$⊢ M = 0 \to ⟨M, 0⟩ = ⟨0, 0⟩$
9	8	oveq2d	$⊢ M = 0 \to (A ++ B) substr ⟨M, 0⟩ = (A ++ B) substr ⟨0, 0⟩$
10	8	oveq2d	$⊢ M = 0 \to A substr ⟨M, 0⟩ = A substr ⟨0, 0⟩$
11	7 9 10	3eqtr4a	$⊢ M = 0 \to (A ++ B) substr ⟨M, 0⟩ = A substr ⟨M, 0⟩$
12	4 11	syl	$⊢ M \in (0 \dots 0) \to (A ++ B) substr ⟨M, 0⟩ = A substr ⟨M, 0⟩$
13		oveq2	$⊢ N = 0 \to (0 \dots N) = (0 \dots 0)$
14	13	eleq2d	$⊢ N = 0 \to (M \in (0 \dots N) \leftrightarrow M \in (0 \dots 0))$
15		opeq2	$⊢ N = 0 \to ⟨M, N⟩ = ⟨M, 0⟩$
16	15	oveq2d	$⊢ N = 0 \to (A ++ B) substr ⟨M, N⟩ = (A ++ B) substr ⟨M, 0⟩$
17	15	oveq2d	$⊢ N = 0 \to A substr ⟨M, N⟩ = A substr ⟨M, 0⟩$
18	16 17	eqeq12d	$⊢ N = 0 \to ((A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩ \leftrightarrow (A ++ B) substr ⟨M, 0⟩ = A substr ⟨M, 0⟩)$
19	14 18	imbi12d	$⊢ N = 0 \to ((M \in (0 \dots N) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩) \leftrightarrow (M \in (0 \dots 0) \to (A ++ B) substr ⟨M, 0⟩ = A substr ⟨M, 0⟩))$
20	12 19	mpbiri	$⊢ N = 0 \to (M \in (0 \dots N) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩)$
21	3 20	syl	$⊢ N \in (0 \dots 0) \to (M \in (0 \dots N) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩)$
22	2 21	biimtrdi	$⊢ \|A\| = 0 \to (N \in (0 \dots \|A\|) \to (M \in (0 \dots N) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩))$
23	22	impcomd	$⊢ \|A\| = 0 \to ((M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩)$
24	23	adantl	$⊢ ((A \in Word V \land B \in Word V) \land \|A\| = 0) \to ((M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩)$
25		ccatcl	$⊢ (A \in Word V \land B \in Word V) \to A ++ B \in Word V$
26	25	ad2antrr	$⊢ (((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \to A ++ B \in Word V$
27		simprl	$⊢ (((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \to M \in (0 \dots N)$
28		elfzelfzccat	$⊢ (A \in Word V \land B \in Word V) \to (N \in (0 \dots \|A\|) \to N \in (0 \dots \|A ++ B\|))$
29	28	imp	$⊢ ((A \in Word V \land B \in Word V) \land N \in (0 \dots \|A\|)) \to N \in (0 \dots \|A ++ B\|)$
30	29	ad2ant2rl	$⊢ (((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \to N \in (0 \dots \|A ++ B\|)$
31		swrdvalfn	$⊢ (A ++ B \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A ++ B\|)) \to ((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - M)$
32	26 27 30 31	syl3anc	$⊢ (((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \to ((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - M)$
33		3anass	$⊢ (A \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \leftrightarrow (A \in Word V \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|)))$
34	33	simplbi2	$⊢ A \in Word V \to ((M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \to (A \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A\|)))$
35	34	ad2antrr	$⊢ ((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \to ((M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \to (A \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A\|)))$
36	35	imp	$⊢ (((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \to (A \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A\|))$
37		swrdvalfn	$⊢ (A \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \to (A substr ⟨M, N⟩) Fn (0 ..^N - M)$
38	36 37	syl	$⊢ (((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \to (A substr ⟨M, N⟩) Fn (0 ..^N - M)$
39		simp-4l	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to A \in Word V$
40		simp-4r	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to B \in Word V$
41		elfznn0	$⊢ M \in (0 \dots N) \to M \in ℕ_{0}$
42		nn0addcl	$⊢ (k \in ℕ_{0} \land M \in ℕ_{0}) \to k + M \in ℕ_{0}$
43	42	expcom	$⊢ M \in ℕ_{0} \to (k \in ℕ_{0} \to k + M \in ℕ_{0})$
44	41 43	syl	$⊢ M \in (0 \dots N) \to (k \in ℕ_{0} \to k + M \in ℕ_{0})$
45	44	ad2antrl	$⊢ (((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \to (k \in ℕ_{0} \to k + M \in ℕ_{0})$
46		elfzonn0	$⊢ k \in (0 ..^N - M) \to k \in ℕ_{0}$
47	45 46	impel	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to k + M \in ℕ_{0}$
48		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
49		elnnne0	$⊢ \|A\| \in ℕ \leftrightarrow (\|A\| \in ℕ_{0} \land \|A\| \neq 0)$
50	49	simplbi2	$⊢ \|A\| \in ℕ_{0} \to (\|A\| \neq 0 \to \|A\| \in ℕ)$
51	48 50	syl	$⊢ A \in Word V \to (\|A\| \neq 0 \to \|A\| \in ℕ)$
52	51	adantr	$⊢ (A \in Word V \land B \in Word V) \to (\|A\| \neq 0 \to \|A\| \in ℕ)$
53	52	imp	$⊢ ((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \to \|A\| \in ℕ$
54	53	ad2antrr	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to \|A\| \in ℕ$
55		elfzo0	$⊢ k \in (0 ..^N - M) \leftrightarrow (k \in ℕ_{0} \land N - M \in ℕ \land k < N - M)$
56		elfz2nn0	$⊢ N \in (0 \dots \|A\|) \leftrightarrow (N \in ℕ_{0} \land \|A\| \in ℕ_{0} \land N \leq \|A\|)$
57		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
58	57	ad2antrl	$⊢ ((N \in ℕ_{0} \land \|A\| \in ℕ_{0}) \land (k \in ℕ_{0} \land M \in ℕ_{0})) \to k \in ℝ$
59		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
60	59	ad2antll	$⊢ ((N \in ℕ_{0} \land \|A\| \in ℕ_{0}) \land (k \in ℕ_{0} \land M \in ℕ_{0})) \to M \in ℝ$
61		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
62	61	ad2antrr	$⊢ ((N \in ℕ_{0} \land \|A\| \in ℕ_{0}) \land (k \in ℕ_{0} \land M \in ℕ_{0})) \to N \in ℝ$
63	58 60 62	ltaddsubd	$⊢ ((N \in ℕ_{0} \land \|A\| \in ℕ_{0}) \land (k \in ℕ_{0} \land M \in ℕ_{0})) \to (k + M < N \leftrightarrow k < N - M)$
64		nn0readdcl	$⊢ (k \in ℕ_{0} \land M \in ℕ_{0}) \to k + M \in ℝ$
65	64	adantl	$⊢ ((N \in ℕ_{0} \land \|A\| \in ℕ_{0}) \land (k \in ℕ_{0} \land M \in ℕ_{0})) \to k + M \in ℝ$
66		nn0re	$⊢ \|A\| \in ℕ_{0} \to \|A\| \in ℝ$
67	66	ad2antlr	$⊢ ((N \in ℕ_{0} \land \|A\| \in ℕ_{0}) \land (k \in ℕ_{0} \land M \in ℕ_{0})) \to \|A\| \in ℝ$
68		ltletr	$⊢ (k + M \in ℝ \land N \in ℝ \land \|A\| \in ℝ) \to ((k + M < N \land N \leq \|A\|) \to k + M < \|A\|)$
69	65 62 67 68	syl3anc	$⊢ ((N \in ℕ_{0} \land \|A\| \in ℕ_{0}) \land (k \in ℕ_{0} \land M \in ℕ_{0})) \to ((k + M < N \land N \leq \|A\|) \to k + M < \|A\|)$
70	69	expd	$⊢ ((N \in ℕ_{0} \land \|A\| \in ℕ_{0}) \land (k \in ℕ_{0} \land M \in ℕ_{0})) \to (k + M < N \to (N \leq \|A\| \to k + M < \|A\|))$
71	63 70	sylbird	$⊢ ((N \in ℕ_{0} \land \|A\| \in ℕ_{0}) \land (k \in ℕ_{0} \land M \in ℕ_{0})) \to (k < N - M \to (N \leq \|A\| \to k + M < \|A\|))$
72	71	ex	$⊢ (N \in ℕ_{0} \land \|A\| \in ℕ_{0}) \to ((k \in ℕ_{0} \land M \in ℕ_{0}) \to (k < N - M \to (N \leq \|A\| \to k + M < \|A\|)))$
73	72	com24	$⊢ (N \in ℕ_{0} \land \|A\| \in ℕ_{0}) \to (N \leq \|A\| \to (k < N - M \to ((k \in ℕ_{0} \land M \in ℕ_{0}) \to k + M < \|A\|)))$
74	73	3impia	$⊢ (N \in ℕ_{0} \land \|A\| \in ℕ_{0} \land N \leq \|A\|) \to (k < N - M \to ((k \in ℕ_{0} \land M \in ℕ_{0}) \to k + M < \|A\|))$
75	74	com13	$⊢ (k \in ℕ_{0} \land M \in ℕ_{0}) \to (k < N - M \to ((N \in ℕ_{0} \land \|A\| \in ℕ_{0} \land N \leq \|A\|) \to k + M < \|A\|))$
76	75	impancom	$⊢ (k \in ℕ_{0} \land k < N - M) \to (M \in ℕ_{0} \to ((N \in ℕ_{0} \land \|A\| \in ℕ_{0} \land N \leq \|A\|) \to k + M < \|A\|))$
77	76	3adant2	$⊢ (k \in ℕ_{0} \land N - M \in ℕ \land k < N - M) \to (M \in ℕ_{0} \to ((N \in ℕ_{0} \land \|A\| \in ℕ_{0} \land N \leq \|A\|) \to k + M < \|A\|))$
78	77	com13	$⊢ (N \in ℕ_{0} \land \|A\| \in ℕ_{0} \land N \leq \|A\|) \to (M \in ℕ_{0} \to ((k \in ℕ_{0} \land N - M \in ℕ \land k < N - M) \to k + M < \|A\|))$
79	56 78	sylbi	$⊢ N \in (0 \dots \|A\|) \to (M \in ℕ_{0} \to ((k \in ℕ_{0} \land N - M \in ℕ \land k < N - M) \to k + M < \|A\|))$
80	41 79	mpan9	$⊢ (M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \to ((k \in ℕ_{0} \land N - M \in ℕ \land k < N - M) \to k + M < \|A\|)$
81	80	adantl	$⊢ (((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \to ((k \in ℕ_{0} \land N - M \in ℕ \land k < N - M) \to k + M < \|A\|)$
82	55 81	biimtrid	$⊢ (((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \to (k \in (0 ..^N - M) \to k + M < \|A\|)$
83	82	imp	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to k + M < \|A\|$
84		elfzo0	$⊢ k + M \in (0 ..^\|A\|) \leftrightarrow (k + M \in ℕ_{0} \land \|A\| \in ℕ \land k + M < \|A\|)$
85	47 54 83 84	syl3anbrc	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to k + M \in (0 ..^\|A\|)$
86		ccatval1	$⊢ (A \in Word V \land B \in Word V \land k + M \in (0 ..^\|A\|)) \to (A ++ B) (k + M) = A (k + M)$
87	39 40 85 86	syl3anc	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to (A ++ B) (k + M) = A (k + M)$
88	25	ad3antrrr	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to A ++ B \in Word V$
89		simplrl	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to M \in (0 \dots N)$
90	30	adantr	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to N \in (0 \dots \|A ++ B\|)$
91		simpr	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to k \in (0 ..^N - M)$
92		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)$
93	88 89 90 91 92	syl31anc	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to ((A ++ B) substr ⟨M, N⟩) (k) = (A ++ B) (k + M)$
94		swrdfv	$⊢ ((A \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \land k \in (0 ..^N - M)) \to (A substr ⟨M, N⟩) (k) = A (k + M)$
95	36 94	sylan	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to (A substr ⟨M, N⟩) (k) = A (k + M)$
96	87 93 95	3eqtr4d	$⊢ ((((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \land k \in (0 ..^N - M)) \to ((A ++ B) substr ⟨M, N⟩) (k) = (A substr ⟨M, N⟩) (k)$
97	32 38 96	eqfnfvd	$⊢ (((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\|))) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩$
98	97	ex	$⊢ ((A \in Word V \land B \in Word V) \land \|A\| \neq 0) \to ((M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩)$
99	24 98	pm2.61dane	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩)$

Metamath Proof Explorer

Theorem swrdccatin1

Proof