Step |
Hyp |
Ref |
Expression |
1 |
|
repsw |
|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) e. Word V ) |
2 |
1
|
3adant3 |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( S repeatS N ) e. Word V ) |
3 |
|
repswlen |
|- ( ( S e. V /\ N e. NN0 ) -> ( # ` ( S repeatS N ) ) = N ) |
4 |
3
|
oveq2d |
|- ( ( S e. V /\ N e. NN0 ) -> ( 0 ... ( # ` ( S repeatS N ) ) ) = ( 0 ... N ) ) |
5 |
4
|
eleq2d |
|- ( ( S e. V /\ N e. NN0 ) -> ( L e. ( 0 ... ( # ` ( S repeatS N ) ) ) <-> L e. ( 0 ... N ) ) ) |
6 |
5
|
biimp3ar |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> L e. ( 0 ... ( # ` ( S repeatS N ) ) ) ) |
7 |
|
pfxlen |
|- ( ( ( S repeatS N ) e. Word V /\ L e. ( 0 ... ( # ` ( S repeatS N ) ) ) ) -> ( # ` ( ( S repeatS N ) prefix L ) ) = L ) |
8 |
2 6 7
|
syl2anc |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( # ` ( ( S repeatS N ) prefix L ) ) = L ) |
9 |
|
elfznn0 |
|- ( L e. ( 0 ... N ) -> L e. NN0 ) |
10 |
|
repswlen |
|- ( ( S e. V /\ L e. NN0 ) -> ( # ` ( S repeatS L ) ) = L ) |
11 |
9 10
|
sylan2 |
|- ( ( S e. V /\ L e. ( 0 ... N ) ) -> ( # ` ( S repeatS L ) ) = L ) |
12 |
11
|
3adant2 |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( # ` ( S repeatS L ) ) = L ) |
13 |
8 12
|
eqtr4d |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( # ` ( ( S repeatS N ) prefix L ) ) = ( # ` ( S repeatS L ) ) ) |
14 |
|
simpl1 |
|- ( ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) /\ i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ) -> S e. V ) |
15 |
|
simpl2 |
|- ( ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) /\ i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ) -> N e. NN0 ) |
16 |
|
elfzuz3 |
|- ( L e. ( 0 ... N ) -> N e. ( ZZ>= ` L ) ) |
17 |
16
|
3ad2ant3 |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> N e. ( ZZ>= ` L ) ) |
18 |
8
|
fveq2d |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( ZZ>= ` ( # ` ( ( S repeatS N ) prefix L ) ) ) = ( ZZ>= ` L ) ) |
19 |
17 18
|
eleqtrrd |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> N e. ( ZZ>= ` ( # ` ( ( S repeatS N ) prefix L ) ) ) ) |
20 |
|
fzoss2 |
|- ( N e. ( ZZ>= ` ( # ` ( ( S repeatS N ) prefix L ) ) ) -> ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) C_ ( 0 ..^ N ) ) |
21 |
19 20
|
syl |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) C_ ( 0 ..^ N ) ) |
22 |
21
|
sselda |
|- ( ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) /\ i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ) -> i e. ( 0 ..^ N ) ) |
23 |
|
repswsymb |
|- ( ( S e. V /\ N e. NN0 /\ i e. ( 0 ..^ N ) ) -> ( ( S repeatS N ) ` i ) = S ) |
24 |
14 15 22 23
|
syl3anc |
|- ( ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) /\ i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ) -> ( ( S repeatS N ) ` i ) = S ) |
25 |
2
|
adantr |
|- ( ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) /\ i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ) -> ( S repeatS N ) e. Word V ) |
26 |
6
|
adantr |
|- ( ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) /\ i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ) -> L e. ( 0 ... ( # ` ( S repeatS N ) ) ) ) |
27 |
8
|
oveq2d |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) = ( 0 ..^ L ) ) |
28 |
27
|
eleq2d |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) <-> i e. ( 0 ..^ L ) ) ) |
29 |
28
|
biimpa |
|- ( ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) /\ i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ) -> i e. ( 0 ..^ L ) ) |
30 |
|
pfxfv |
|- ( ( ( S repeatS N ) e. Word V /\ L e. ( 0 ... ( # ` ( S repeatS N ) ) ) /\ i e. ( 0 ..^ L ) ) -> ( ( ( S repeatS N ) prefix L ) ` i ) = ( ( S repeatS N ) ` i ) ) |
31 |
25 26 29 30
|
syl3anc |
|- ( ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) /\ i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ) -> ( ( ( S repeatS N ) prefix L ) ` i ) = ( ( S repeatS N ) ` i ) ) |
32 |
9
|
3ad2ant3 |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> L e. NN0 ) |
33 |
32
|
adantr |
|- ( ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) /\ i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ) -> L e. NN0 ) |
34 |
|
repswsymb |
|- ( ( S e. V /\ L e. NN0 /\ i e. ( 0 ..^ L ) ) -> ( ( S repeatS L ) ` i ) = S ) |
35 |
14 33 29 34
|
syl3anc |
|- ( ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) /\ i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ) -> ( ( S repeatS L ) ` i ) = S ) |
36 |
24 31 35
|
3eqtr4d |
|- ( ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) /\ i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ) -> ( ( ( S repeatS N ) prefix L ) ` i ) = ( ( S repeatS L ) ` i ) ) |
37 |
36
|
ralrimiva |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> A. i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ( ( ( S repeatS N ) prefix L ) ` i ) = ( ( S repeatS L ) ` i ) ) |
38 |
|
pfxcl |
|- ( ( S repeatS N ) e. Word V -> ( ( S repeatS N ) prefix L ) e. Word V ) |
39 |
2 38
|
syl |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( ( S repeatS N ) prefix L ) e. Word V ) |
40 |
|
repsw |
|- ( ( S e. V /\ L e. NN0 ) -> ( S repeatS L ) e. Word V ) |
41 |
9 40
|
sylan2 |
|- ( ( S e. V /\ L e. ( 0 ... N ) ) -> ( S repeatS L ) e. Word V ) |
42 |
|
eqwrd |
|- ( ( ( ( S repeatS N ) prefix L ) e. Word V /\ ( S repeatS L ) e. Word V ) -> ( ( ( S repeatS N ) prefix L ) = ( S repeatS L ) <-> ( ( # ` ( ( S repeatS N ) prefix L ) ) = ( # ` ( S repeatS L ) ) /\ A. i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ( ( ( S repeatS N ) prefix L ) ` i ) = ( ( S repeatS L ) ` i ) ) ) ) |
43 |
39 41 42
|
3imp3i2an |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( ( ( S repeatS N ) prefix L ) = ( S repeatS L ) <-> ( ( # ` ( ( S repeatS N ) prefix L ) ) = ( # ` ( S repeatS L ) ) /\ A. i e. ( 0 ..^ ( # ` ( ( S repeatS N ) prefix L ) ) ) ( ( ( S repeatS N ) prefix L ) ` i ) = ( ( S repeatS L ) ` i ) ) ) ) |
44 |
13 37 43
|
mpbir2and |
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( ( S repeatS N ) prefix L ) = ( S repeatS L ) ) |