Metamath Proof Explorer


Theorem repswpfx

Description: A prefix of a repeated symbol word is a repeated symbol word. (Contributed by AV, 11-May-2020)

Ref Expression
Assertion repswpfx
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( ( S repeatS N ) prefix L ) = ( S repeatS L ) )

Proof

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 ) )