repswlen

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

		Ref	Expression
	Assertion	repswlen	$⊢ (S \in V \land N \in ℕ_{0}) \to \|S repeatS N\| = N$

Step	Hyp	Ref	Expression
1		repsf	$⊢ (S \in V \land N \in ℕ_{0}) \to (S repeatS N) : (0 ..^N) ⟶ V$
2		ffn	$⊢ (S repeatS N) : (0 ..^N) ⟶ V \to (S repeatS N) Fn (0 ..^N)$
3		hashfn	$⊢ (S repeatS N) Fn (0 ..^N) \to \|S repeatS N\| = \|(0 ..^N)\|$
4	1 2 3	3syl	$⊢ (S \in V \land N \in ℕ_{0}) \to \|S repeatS N\| = \|(0 ..^N)\|$
5		hashfzo0	$⊢ N \in ℕ_{0} \to \|(0 ..^N)\| = N$
6	5	adantl	$⊢ (S \in V \land N \in ℕ_{0}) \to \|(0 ..^N)\| = N$
7	4 6	eqtrd	$⊢ (S \in V \land N \in ℕ_{0}) \to \|S repeatS N\| = N$

Metamath Proof Explorer