Theorem repswlen

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

	Ref	Expression
Assertion	repswlen	$$⊢\left(S\in V\wedge N\in {\mathbb{N}}_0\right)\to \left|S\mathrm{repeatS}N\right|=N$$

Proof

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