repswsymb

Description: The symbols of a "repeated symbol word". (Contributed by AV, 4-Nov-2018)

		Ref	Expression
	Assertion	repswsymb	$⊢ (S \in V \land N \in ℕ_{0} \land I \in (0 ..^N)) \to (S repeatS N) (I) = S$

Step	Hyp	Ref	Expression
1		reps	$⊢ (S \in V \land N \in ℕ_{0}) \to S repeatS N = (x \in (0 ..^N) ⟼ S)$
2	1	3adant3	$⊢ (S \in V \land N \in ℕ_{0} \land I \in (0 ..^N)) \to S repeatS N = (x \in (0 ..^N) ⟼ S)$
3		eqidd	$⊢ ((S \in V \land N \in ℕ_{0} \land I \in (0 ..^N)) \land x = I) \to S = S$
4		simp3	$⊢ (S \in V \land N \in ℕ_{0} \land I \in (0 ..^N)) \to I \in (0 ..^N)$
5		simp1	$⊢ (S \in V \land N \in ℕ_{0} \land I \in (0 ..^N)) \to S \in V$
6	2 3 4 5	fvmptd	$⊢ (S \in V \land N \in ℕ_{0} \land I \in (0 ..^N)) \to (S repeatS N) (I) = S$

Metamath Proof Explorer