Description: Definition to construct a word consisting of one repeated symbol, often called "repeated symbol word" for short in the following. (Contributed by Alexander van der Vekens, 4-Nov-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-reps | |- repeatS = ( s e. _V , n e. NN0 |-> ( x e. ( 0 ..^ n ) |-> s ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | creps | |- repeatS |
|
| 1 | vs | |- s |
|
| 2 | cvv | |- _V |
|
| 3 | vn | |- n |
|
| 4 | cn0 | |- NN0 |
|
| 5 | vx | |- x |
|
| 6 | cc0 | |- 0 |
|
| 7 | cfzo | |- ..^ |
|
| 8 | 3 | cv | |- n |
| 9 | 6 8 7 | co | |- ( 0 ..^ n ) |
| 10 | 1 | cv | |- s |
| 11 | 5 9 10 | cmpt | |- ( x e. ( 0 ..^ n ) |-> s ) |
| 12 | 1 3 2 4 11 | cmpo | |- ( s e. _V , n e. NN0 |-> ( x e. ( 0 ..^ n ) |-> s ) ) |
| 13 | 0 12 | wceq | |- repeatS = ( s e. _V , n e. NN0 |-> ( x e. ( 0 ..^ n ) |-> s ) ) |