pfxco

Description: Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020)

		Ref	Expression
	Assertion	pfxco	$⊢ (W \in Word A \land N \in (0 \dots \|W\|) \land F : A ⟶ B) \to F \circ (W prefix N) = (F \circ W) prefix N$

Proof

Step	Hyp	Ref	Expression
1		elfznn0	$⊢ N \in (0 \dots \|W\|) \to N \in ℕ_{0}$
2	1	3ad2ant2	$⊢ (W \in Word A \land N \in (0 \dots \|W\|) \land F : A ⟶ B) \to N \in ℕ_{0}$
3		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
4	2 3	syl	$⊢ (W \in Word A \land N \in (0 \dots \|W\|) \land F : A ⟶ B) \to 0 \in (0 \dots N)$
5		simp2	$⊢ (W \in Word A \land N \in (0 \dots \|W\|) \land F : A ⟶ B) \to N \in (0 \dots \|W\|)$
6	4 5	jca	$⊢ (W \in Word A \land N \in (0 \dots \|W\|) \land F : A ⟶ B) \to (0 \in (0 \dots N) \land N \in (0 \dots \|W\|))$
7		swrdco	$⊢ (W \in Word A \land (0 \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land F : A ⟶ B) \to F \circ (W substr ⟨0, N⟩) = (F \circ W) substr ⟨0, N⟩$
8	6 7	syld3an2	$⊢ (W \in Word A \land N \in (0 \dots \|W\|) \land F : A ⟶ B) \to F \circ (W substr ⟨0, N⟩) = (F \circ W) substr ⟨0, N⟩$
9		pfxval	$⊢ (W \in Word A \land N \in ℕ_{0}) \to W prefix N = W substr ⟨0, N⟩$
10	1 9	sylan2	$⊢ (W \in Word A \land N \in (0 \dots \|W\|)) \to W prefix N = W substr ⟨0, N⟩$
11	10	coeq2d	$⊢ (W \in Word A \land N \in (0 \dots \|W\|)) \to F \circ (W prefix N) = F \circ (W substr ⟨0, N⟩)$
12	11	3adant3	$⊢ (W \in Word A \land N \in (0 \dots \|W\|) \land F : A ⟶ B) \to F \circ (W prefix N) = F \circ (W substr ⟨0, N⟩)$
13		ffun	$⊢ F : A ⟶ B \to Fun F$
14	13	anim2i	$⊢ (W \in Word A \land F : A ⟶ B) \to (W \in Word A \land Fun F)$
15	14	ancomd	$⊢ (W \in Word A \land F : A ⟶ B) \to (Fun F \land W \in Word A)$
16	15	3adant2	$⊢ (W \in Word A \land N \in (0 \dots \|W\|) \land F : A ⟶ B) \to (Fun F \land W \in Word A)$
17		cofunexg	$⊢ (Fun F \land W \in Word A) \to F \circ W \in V$
18	16 17	syl	$⊢ (W \in Word A \land N \in (0 \dots \|W\|) \land F : A ⟶ B) \to F \circ W \in V$
19	18 2	jca	$⊢ (W \in Word A \land N \in (0 \dots \|W\|) \land F : A ⟶ B) \to (F \circ W \in V \land N \in ℕ_{0})$
20		pfxval	$⊢ (F \circ W \in V \land N \in ℕ_{0}) \to (F \circ W) prefix N = (F \circ W) substr ⟨0, N⟩$
21	19 20	syl	$⊢ (W \in Word A \land N \in (0 \dots \|W\|) \land F : A ⟶ B) \to (F \circ W) prefix N = (F \circ W) substr ⟨0, N⟩$
22	8 12 21	3eqtr4d	$⊢ (W \in Word A \land N \in (0 \dots \|W\|) \land F : A ⟶ B) \to F \circ (W prefix N) = (F \circ W) prefix N$

Metamath Proof Explorer

Theorem pfxco

Proof