Metamath Proof Explorer

Theorem repsco

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

		Ref	Expression
	Assertion	repsco	$⊢ (S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \to F \circ (S repeatS N) = F (S) repeatS N$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \land x \in (0 ..^N)) \to S \in A$
2		simpl2	$⊢ ((S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \land x \in (0 ..^N)) \to N \in ℕ_{0}$
3		simpr	$⊢ ((S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \land x \in (0 ..^N)) \to x \in (0 ..^N)$
4		repswsymb	$⊢ (S \in A \land N \in ℕ_{0} \land x \in (0 ..^N)) \to (S repeatS N) (x) = S$
5	1 2 3 4	syl3anc	$⊢ ((S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \land x \in (0 ..^N)) \to (S repeatS N) (x) = S$
6	5	fveq2d	$⊢ ((S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \land x \in (0 ..^N)) \to F ((S repeatS N) (x)) = F (S)$
7	6	mpteq2dva	$⊢ (S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \to (x \in (0 ..^N) ⟼ F ((S repeatS N) (x))) = (x \in (0 ..^N) ⟼ F (S))$
8		simp3	$⊢ (S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \to F : A ⟶ B$
9		repsf	$⊢ (S \in A \land N \in ℕ_{0}) \to (S repeatS N) : (0 ..^N) ⟶ A$
10	9	3adant3	$⊢ (S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \to (S repeatS N) : (0 ..^N) ⟶ A$
11		fcompt	$⊢ (F : A ⟶ B \land (S repeatS N) : (0 ..^N) ⟶ A) \to F \circ (S repeatS N) = (x \in (0 ..^N) ⟼ F ((S repeatS N) (x)))$
12	8 10 11	syl2anc	$⊢ (S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \to F \circ (S repeatS N) = (x \in (0 ..^N) ⟼ F ((S repeatS N) (x)))$
13		fvexd	$⊢ S \in A \to F (S) \in V$
14	13	anim1i	$⊢ (S \in A \land N \in ℕ_{0}) \to (F (S) \in V \land N \in ℕ_{0})$
15	14	3adant3	$⊢ (S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \to (F (S) \in V \land N \in ℕ_{0})$
16		reps	$⊢ (F (S) \in V \land N \in ℕ_{0}) \to F (S) repeatS N = (x \in (0 ..^N) ⟼ F (S))$
17	15 16	syl	$⊢ (S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \to F (S) repeatS N = (x \in (0 ..^N) ⟼ F (S))$
18	7 12 17	3eqtr4d	$⊢ (S \in A \land N \in ℕ_{0} \land F : A ⟶ B) \to F \circ (S repeatS N) = F (S) repeatS N$