swrdco

Description: Mapping of words commutes with the substring operation. (Contributed by AV, 11-Nov-2018)

		Ref	Expression
	Assertion	swrdco	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to F \circ (W substr ⟨M, N⟩) = (F \circ W) substr ⟨M, N⟩$

Proof

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : A ⟶ B \to F Fn A$
2	1	3ad2ant3	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to F Fn A$
3		swrdvalfn	$⊢ (W \in Word A \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (W substr ⟨M, N⟩) Fn (0 ..^N - M)$
4	3	3expb	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|))) \to (W substr ⟨M, N⟩) Fn (0 ..^N - M)$
5	4	3adant3	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to (W substr ⟨M, N⟩) Fn (0 ..^N - M)$
6		swrdrn	$⊢ (W \in Word A \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to ran (W substr ⟨M, N⟩) \subseteq A$
7	6	3expb	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|))) \to ran (W substr ⟨M, N⟩) \subseteq A$
8	7	3adant3	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to ran (W substr ⟨M, N⟩) \subseteq A$
9		fnco	$⊢ (F Fn A \land (W substr ⟨M, N⟩) Fn (0 ..^N - M) \land ran (W substr ⟨M, N⟩) \subseteq A) \to (F \circ (W substr ⟨M, N⟩)) Fn (0 ..^N - M)$
10	2 5 8 9	syl3anc	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to (F \circ (W substr ⟨M, N⟩)) Fn (0 ..^N - M)$
11		wrdco	$⊢ (W \in Word A \land F : A ⟶ B) \to F \circ W \in Word B$
12	11	3adant2	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to F \circ W \in Word B$
13		simp2l	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to M \in (0 \dots N)$
14		lenco	$⊢ (W \in Word A \land F : A ⟶ B) \to \|F \circ W\| = \|W\|$
15	14	eqcomd	$⊢ (W \in Word A \land F : A ⟶ B) \to \|W\| = \|F \circ W\|$
16	15	oveq2d	$⊢ (W \in Word A \land F : A ⟶ B) \to (0 \dots \|W\|) = (0 \dots \|F \circ W\|)$
17	16	eleq2d	$⊢ (W \in Word A \land F : A ⟶ B) \to (N \in (0 \dots \|W\|) \leftrightarrow N \in (0 \dots \|F \circ W\|))$
18	17	biimpd	$⊢ (W \in Word A \land F : A ⟶ B) \to (N \in (0 \dots \|W\|) \to N \in (0 \dots \|F \circ W\|))$
19	18	expcom	$⊢ F : A ⟶ B \to (W \in Word A \to (N \in (0 \dots \|W\|) \to N \in (0 \dots \|F \circ W\|)))$
20	19	com13	$⊢ N \in (0 \dots \|W\|) \to (W \in Word A \to (F : A ⟶ B \to N \in (0 \dots \|F \circ W\|)))$
21	20	adantl	$⊢ (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (W \in Word A \to (F : A ⟶ B \to N \in (0 \dots \|F \circ W\|)))$
22	21	3imp21	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to N \in (0 \dots \|F \circ W\|)$
23		swrdvalfn	$⊢ (F \circ W \in Word B \land M \in (0 \dots N) \land N \in (0 \dots \|F \circ W\|)) \to ((F \circ W) substr ⟨M, N⟩) Fn (0 ..^N - M)$
24	12 13 22 23	syl3anc	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to ((F \circ W) substr ⟨M, N⟩) Fn (0 ..^N - M)$
25		3anass	$⊢ (W \in Word A \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \leftrightarrow (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)))$
26	25	biimpri	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|))) \to (W \in Word A \land M \in (0 \dots N) \land N \in (0 \dots \|W\|))$
27	26	3adant3	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to (W \in Word A \land M \in (0 \dots N) \land N \in (0 \dots \|W\|))$
28		swrdfv	$⊢ ((W \in Word A \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land i \in (0 ..^N - M)) \to (W substr ⟨M, N⟩) (i) = W (i + M)$
29	28	fveq2d	$⊢ ((W \in Word A \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land i \in (0 ..^N - M)) \to F ((W substr ⟨M, N⟩) (i)) = F (W (i + M))$
30	27 29	sylan	$⊢ ((W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \land i \in (0 ..^N - M)) \to F ((W substr ⟨M, N⟩) (i)) = F (W (i + M))$
31		wrdfn	$⊢ W \in Word A \to W Fn (0 ..^\|W\|)$
32	31	3ad2ant1	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to W Fn (0 ..^\|W\|)$
33		elfzodifsumelfzo	$⊢ (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (i \in (0 ..^N - M) \to i + M \in (0 ..^\|W\|))$
34	33	3ad2ant2	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to (i \in (0 ..^N - M) \to i + M \in (0 ..^\|W\|))$
35	34	imp	$⊢ ((W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \land i \in (0 ..^N - M)) \to i + M \in (0 ..^\|W\|)$
36		fvco2	$⊢ (W Fn (0 ..^\|W\|) \land i + M \in (0 ..^\|W\|)) \to (F \circ W) (i + M) = F (W (i + M))$
37	32 35 36	syl2an2r	$⊢ ((W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \land i \in (0 ..^N - M)) \to (F \circ W) (i + M) = F (W (i + M))$
38	30 37	eqtr4d	$⊢ ((W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \land i \in (0 ..^N - M)) \to F ((W substr ⟨M, N⟩) (i)) = (F \circ W) (i + M)$
39		fvco2	$⊢ ((W substr ⟨M, N⟩) Fn (0 ..^N - M) \land i \in (0 ..^N - M)) \to (F \circ (W substr ⟨M, N⟩)) (i) = F ((W substr ⟨M, N⟩) (i))$
40	5 39	sylan	$⊢ ((W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \land i \in (0 ..^N - M)) \to (F \circ (W substr ⟨M, N⟩)) (i) = F ((W substr ⟨M, N⟩) (i))$
41	14	ancoms	$⊢ (F : A ⟶ B \land W \in Word A) \to \|F \circ W\| = \|W\|$
42	41	eqcomd	$⊢ (F : A ⟶ B \land W \in Word A) \to \|W\| = \|F \circ W\|$
43	42	oveq2d	$⊢ (F : A ⟶ B \land W \in Word A) \to (0 \dots \|W\|) = (0 \dots \|F \circ W\|)$
44	43	eleq2d	$⊢ (F : A ⟶ B \land W \in Word A) \to (N \in (0 \dots \|W\|) \leftrightarrow N \in (0 \dots \|F \circ W\|))$
45	44	biimpd	$⊢ (F : A ⟶ B \land W \in Word A) \to (N \in (0 \dots \|W\|) \to N \in (0 \dots \|F \circ W\|))$
46	45	ex	$⊢ F : A ⟶ B \to (W \in Word A \to (N \in (0 \dots \|W\|) \to N \in (0 \dots \|F \circ W\|)))$
47	46	com13	$⊢ N \in (0 \dots \|W\|) \to (W \in Word A \to (F : A ⟶ B \to N \in (0 \dots \|F \circ W\|)))$
48	47	adantl	$⊢ (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (W \in Word A \to (F : A ⟶ B \to N \in (0 \dots \|F \circ W\|)))$
49	48	3imp21	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to N \in (0 \dots \|F \circ W\|)$
50	12 13 49	3jca	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to (F \circ W \in Word B \land M \in (0 \dots N) \land N \in (0 \dots \|F \circ W\|))$
51		swrdfv	$⊢ ((F \circ W \in Word B \land M \in (0 \dots N) \land N \in (0 \dots \|F \circ W\|)) \land i \in (0 ..^N - M)) \to ((F \circ W) substr ⟨M, N⟩) (i) = (F \circ W) (i + M)$
52	50 51	sylan	$⊢ ((W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \land i \in (0 ..^N - M)) \to ((F \circ W) substr ⟨M, N⟩) (i) = (F \circ W) (i + M)$
53	38 40 52	3eqtr4d	$⊢ ((W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \land i \in (0 ..^N - M)) \to (F \circ (W substr ⟨M, N⟩)) (i) = ((F \circ W) substr ⟨M, N⟩) (i)$
54	10 24 53	eqfnfvd	$⊢ (W \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to F \circ (W substr ⟨M, N⟩) = (F \circ W) substr ⟨M, N⟩$

Metamath Proof Explorer

Theorem swrdco

Proof