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