Theorem repswfsts

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

	Ref	Expression
Assertion	repswfsts	|- ( ( S e. V /\ N e. NN ) -> ( ( S repeatS N ) ` 0 ) = S )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( S e. V /\ N e. NN ) -> S e. V )
2		nnnn0	|- ( N e. NN -> N e. NN0 )
3	2	adantl	|- ( ( S e. V /\ N e. NN ) -> N e. NN0 )
4		lbfzo0	|- ( 0 e. ( 0 ..^ N ) <-> N e. NN )
5	4	biimpri	|- ( N e. NN -> 0 e. ( 0 ..^ N ) )
6	5	adantl	|- ( ( S e. V /\ N e. NN ) -> 0 e. ( 0 ..^ N ) )
7		repswsymb	|- ( ( S e. V /\ N e. NN0 /\ 0 e. ( 0 ..^ N ) ) -> ( ( S repeatS N ) ` 0 ) = S )
8	1 3 6 7	syl3anc	|- ( ( S e. V /\ N e. NN ) -> ( ( S repeatS N ) ` 0 ) = S )