Metamath Proof Explorer

Theorem pfx2

Description: A prefix of length two. (Contributed by AV, 15-May-2020)

Ref Expression
Assertion pfx2 
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( W prefix 2 ) = <" ( W ` 0 ) ( W ` 1 ) "> )

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 1 a1i 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 2 e. NN0 )
3 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
4 3 adantr 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( # ` W ) e. NN0 )
5 simpr 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 2 <_ ( # ` W ) )
6 elfz2nn0 
 |-  ( 2 e. ( 0 ... ( # ` W ) ) <-> ( 2 e. NN0 /\ ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) )
7 2 4 5 6 syl3anbrc 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 2 e. ( 0 ... ( # ` W ) ) )
8 pfxlen 
 |-  ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix 2 ) ) = 2 )
9 s2len 
 |-  ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) = 2
10 9 eqcomi 
 |-  2 = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> )
11 10 a1i 
 |-  ( ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) /\ ( # ` ( W prefix 2 ) ) = 2 ) -> 2 = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) )
12 2nn 
 |-  2 e. NN
13 lbfzo0 
 |-  ( 0 e. ( 0 ..^ 2 ) <-> 2 e. NN )
14 12 13 mpbir 
 |-  0 e. ( 0 ..^ 2 )
15 pfxfv 
 |-  ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) /\ 0 e. ( 0 ..^ 2 ) ) -> ( ( W prefix 2 ) ` 0 ) = ( W ` 0 ) )
16 14 15 mp3an3 
 |-  ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix 2 ) ` 0 ) = ( W ` 0 ) )
17 16 adantr 
 |-  ( ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) /\ ( # ` ( W prefix 2 ) ) = 2 ) -> ( ( W prefix 2 ) ` 0 ) = ( W ` 0 ) )
18 fvex 
 |-  ( W ` 0 ) e. _V
19 s2fv0 
 |-  ( ( W ` 0 ) e. _V -> ( <" ( W ` 0 ) ( W ` 1 ) "> ` 0 ) = ( W ` 0 ) )
20 18 19 ax-mp 
 |-  ( <" ( W ` 0 ) ( W ` 1 ) "> ` 0 ) = ( W ` 0 )
21 17 20 eqtr4di 
 |-  ( ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) /\ ( # ` ( W prefix 2 ) ) = 2 ) -> ( ( W prefix 2 ) ` 0 ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` 0 ) )
22 1nn0 
 |-  1 e. NN0
23 1lt2 
 |-  1 < 2
24 elfzo0 
 |-  ( 1 e. ( 0 ..^ 2 ) <-> ( 1 e. NN0 /\ 2 e. NN /\ 1 < 2 ) )
25 22 12 23 24 mpbir3an 
 |-  1 e. ( 0 ..^ 2 )
26 pfxfv 
 |-  ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) /\ 1 e. ( 0 ..^ 2 ) ) -> ( ( W prefix 2 ) ` 1 ) = ( W ` 1 ) )
27 25 26 mp3an3 
 |-  ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix 2 ) ` 1 ) = ( W ` 1 ) )
28 fvex 
 |-  ( W ` 1 ) e. _V
29 s2fv1 
 |-  ( ( W ` 1 ) e. _V -> ( <" ( W ` 0 ) ( W ` 1 ) "> ` 1 ) = ( W ` 1 ) )
30 28 29 ax-mp 
 |-  ( <" ( W ` 0 ) ( W ` 1 ) "> ` 1 ) = ( W ` 1 )
31 27 30 eqtr4di 
 |-  ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix 2 ) ` 1 ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` 1 ) )
32 31 adantr 
 |-  ( ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) /\ ( # ` ( W prefix 2 ) ) = 2 ) -> ( ( W prefix 2 ) ` 1 ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` 1 ) )
33 0nn0 
 |-  0 e. NN0
34 fveq2 
 |-  ( i = 0 -> ( ( W prefix 2 ) ` i ) = ( ( W prefix 2 ) ` 0 ) )
35 fveq2 
 |-  ( i = 0 -> ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` 0 ) )
36 34 35 eqeq12d 
 |-  ( i = 0 -> ( ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) <-> ( ( W prefix 2 ) ` 0 ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` 0 ) ) )
37 fveq2 
 |-  ( i = 1 -> ( ( W prefix 2 ) ` i ) = ( ( W prefix 2 ) ` 1 ) )
38 fveq2 
 |-  ( i = 1 -> ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` 1 ) )
39 37 38 eqeq12d 
 |-  ( i = 1 -> ( ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) <-> ( ( W prefix 2 ) ` 1 ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` 1 ) ) )
40 36 39 ralprg 
 |-  ( ( 0 e. NN0 /\ 1 e. NN0 ) -> ( A. i e. { 0 , 1 } ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) <-> ( ( ( W prefix 2 ) ` 0 ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` 0 ) /\ ( ( W prefix 2 ) ` 1 ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` 1 ) ) ) )
41 33 22 40 mp2an 
 |-  ( A. i e. { 0 , 1 } ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) <-> ( ( ( W prefix 2 ) ` 0 ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` 0 ) /\ ( ( W prefix 2 ) ` 1 ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` 1 ) ) )
42 21 32 41 sylanbrc 
 |-  ( ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) /\ ( # ` ( W prefix 2 ) ) = 2 ) -> A. i e. { 0 , 1 } ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) )
43 eqeq1 
 |-  ( ( # ` ( W prefix 2 ) ) = 2 -> ( ( # ` ( W prefix 2 ) ) = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) <-> 2 = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) ) )
44 oveq2 
 |-  ( ( # ` ( W prefix 2 ) ) = 2 -> ( 0 ..^ ( # ` ( W prefix 2 ) ) ) = ( 0 ..^ 2 ) )
45 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
46 44 45 eqtrdi 
 |-  ( ( # ` ( W prefix 2 ) ) = 2 -> ( 0 ..^ ( # ` ( W prefix 2 ) ) ) = { 0 , 1 } )
47 46 raleqdv 
 |-  ( ( # ` ( W prefix 2 ) ) = 2 -> ( A. i e. ( 0 ..^ ( # ` ( W prefix 2 ) ) ) ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) <-> A. i e. { 0 , 1 } ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) ) )
48 43 47 anbi12d 
 |-  ( ( # ` ( W prefix 2 ) ) = 2 -> ( ( ( # ` ( W prefix 2 ) ) = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) /\ A. i e. ( 0 ..^ ( # ` ( W prefix 2 ) ) ) ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) ) <-> ( 2 = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) /\ A. i e. { 0 , 1 } ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) ) ) )
49 48 adantl 
 |-  ( ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) /\ ( # ` ( W prefix 2 ) ) = 2 ) -> ( ( ( # ` ( W prefix 2 ) ) = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) /\ A. i e. ( 0 ..^ ( # ` ( W prefix 2 ) ) ) ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) ) <-> ( 2 = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) /\ A. i e. { 0 , 1 } ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) ) ) )
50 11 42 49 mpbir2and 
 |-  ( ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) /\ ( # ` ( W prefix 2 ) ) = 2 ) -> ( ( # ` ( W prefix 2 ) ) = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) /\ A. i e. ( 0 ..^ ( # ` ( W prefix 2 ) ) ) ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) ) )
51 8 50 mpdan 
 |-  ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W prefix 2 ) ) = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) /\ A. i e. ( 0 ..^ ( # ` ( W prefix 2 ) ) ) ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) ) )
52 pfxcl 
 |-  ( W e. Word V -> ( W prefix 2 ) e. Word V )
53 s2cli 
 |-  <" ( W ` 0 ) ( W ` 1 ) "> e. Word _V
54 eqwrd 
 |-  ( ( ( W prefix 2 ) e. Word V /\ <" ( W ` 0 ) ( W ` 1 ) "> e. Word _V ) -> ( ( W prefix 2 ) = <" ( W ` 0 ) ( W ` 1 ) "> <-> ( ( # ` ( W prefix 2 ) ) = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) /\ A. i e. ( 0 ..^ ( # ` ( W prefix 2 ) ) ) ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) ) ) )
55 52 53 54 sylancl 
 |-  ( W e. Word V -> ( ( W prefix 2 ) = <" ( W ` 0 ) ( W ` 1 ) "> <-> ( ( # ` ( W prefix 2 ) ) = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) /\ A. i e. ( 0 ..^ ( # ` ( W prefix 2 ) ) ) ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) ) ) )
56 55 adantr 
 |-  ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix 2 ) = <" ( W ` 0 ) ( W ` 1 ) "> <-> ( ( # ` ( W prefix 2 ) ) = ( # ` <" ( W ` 0 ) ( W ` 1 ) "> ) /\ A. i e. ( 0 ..^ ( # ` ( W prefix 2 ) ) ) ( ( W prefix 2 ) ` i ) = ( <" ( W ` 0 ) ( W ` 1 ) "> ` i ) ) ) )
57 51 56 mpbird 
 |-  ( ( W e. Word V /\ 2 e. ( 0 ... ( # ` W ) ) ) -> ( W prefix 2 ) = <" ( W ` 0 ) ( W ` 1 ) "> )
58 7 57 syldan 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( W prefix 2 ) = <" ( W ` 0 ) ( W ` 1 ) "> )