Metamath Proof Explorer

Theorem repswsymb

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

Ref Expression
Assertion repswsymb 
|- ( ( S e. V /\ N e. NN0 /\ I e. ( 0 ..^ N ) ) -> ( ( S repeatS N ) ` I ) = S )

Proof

Step Hyp Ref Expression
1 reps 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( x e. ( 0 ..^ N ) |-> S ) )
2 1 3adant3 
 |-  ( ( S e. V /\ N e. NN0 /\ I e. ( 0 ..^ N ) ) -> ( S repeatS N ) = ( x e. ( 0 ..^ N ) |-> S ) )
3 eqidd 
 |-  ( ( ( S e. V /\ N e. NN0 /\ I e. ( 0 ..^ N ) ) /\ x = I ) -> S = S )
4 simp3 
 |-  ( ( S e. V /\ N e. NN0 /\ I e. ( 0 ..^ N ) ) -> I e. ( 0 ..^ N ) )
5 simp1 
 |-  ( ( S e. V /\ N e. NN0 /\ I e. ( 0 ..^ N ) ) -> S e. V )
6 2 3 4 5 fvmptd 
 |-  ( ( S e. V /\ N e. NN0 /\ I e. ( 0 ..^ N ) ) -> ( ( S repeatS N ) ` I ) = S )