Metamath Proof Explorer

Theorem pthdlem2

Description: Lemma 2 for pthd . (Contributed by Alexander van der Vekens, 11-Nov-2017) (Revised by AV, 10-Feb-2021)

Ref Expression
Hypotheses pthd.p 
|- ( ph -> P e. Word _V )
pthd.r 
|- R = ( ( # ` P ) - 1 )
pthd.s 
|- ( ph -> A. i e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )
Assertion pthdlem2 
|- ( ph -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) )

Proof

Step Hyp Ref Expression
1 pthd.p 
 |-  ( ph -> P e. Word _V )
2 pthd.r 
 |-  R = ( ( # ` P ) - 1 )
3 pthd.s 
 |-  ( ph -> A. i e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )
4 lencl 
 |-  ( P e. Word _V -> ( # ` P ) e. NN0 )
5 df-ne 
 |-  ( ( # ` P ) =/= 0 <-> -. ( # ` P ) = 0 )
6 elnnne0 
 |-  ( ( # ` P ) e. NN <-> ( ( # ` P ) e. NN0 /\ ( # ` P ) =/= 0 ) )
7 6 simplbi2 
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) =/= 0 -> ( # ` P ) e. NN ) )
8 5 7 syl5bir 
 |-  ( ( # ` P ) e. NN0 -> ( -. ( # ` P ) = 0 -> ( # ` P ) e. NN ) )
9 1 4 8 3syl 
 |-  ( ph -> ( -. ( # ` P ) = 0 -> ( # ` P ) e. NN ) )
10 eqid 
 |-  0 = 0
11 10 orci 
 |-  ( 0 = 0 \/ 0 = R )
12 1 2 3 pthdlem2lem 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( 0 = 0 \/ 0 = R ) ) -> ( P ` 0 ) e/ ( P " ( 1 ..^ R ) ) )
13 11 12 mp3an3 
 |-  ( ( ph /\ ( # ` P ) e. NN ) -> ( P ` 0 ) e/ ( P " ( 1 ..^ R ) ) )
14 eqid 
 |-  R = R
15 14 olci 
 |-  ( R = 0 \/ R = R )
16 1 2 3 pthdlem2lem 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( R = 0 \/ R = R ) ) -> ( P ` R ) e/ ( P " ( 1 ..^ R ) ) )
17 15 16 mp3an3 
 |-  ( ( ph /\ ( # ` P ) e. NN ) -> ( P ` R ) e/ ( P " ( 1 ..^ R ) ) )
18 wrdffz 
 |-  ( P e. Word _V -> P : ( 0 ... ( ( # ` P ) - 1 ) ) --> _V )
19 1 18 syl 
 |-  ( ph -> P : ( 0 ... ( ( # ` P ) - 1 ) ) --> _V )
20 19 adantr 
 |-  ( ( ph /\ ( # ` P ) e. NN ) -> P : ( 0 ... ( ( # ` P ) - 1 ) ) --> _V )
21 2 oveq2i 
 |-  ( 0 ... R ) = ( 0 ... ( ( # ` P ) - 1 ) )
22 21 feq2i 
 |-  ( P : ( 0 ... R ) --> _V <-> P : ( 0 ... ( ( # ` P ) - 1 ) ) --> _V )
23 20 22 sylibr 
 |-  ( ( ph /\ ( # ` P ) e. NN ) -> P : ( 0 ... R ) --> _V )
24 nnm1nn0 
 |-  ( ( # ` P ) e. NN -> ( ( # ` P ) - 1 ) e. NN0 )
25 2 24 eqeltrid 
 |-  ( ( # ` P ) e. NN -> R e. NN0 )
26 25 adantl 
 |-  ( ( ph /\ ( # ` P ) e. NN ) -> R e. NN0 )
27 fvinim0ffz 
 |-  ( ( P : ( 0 ... R ) --> _V /\ R e. NN0 ) -> ( ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) <-> ( ( P ` 0 ) e/ ( P " ( 1 ..^ R ) ) /\ ( P ` R ) e/ ( P " ( 1 ..^ R ) ) ) ) )
28 23 26 27 syl2anc 
 |-  ( ( ph /\ ( # ` P ) e. NN ) -> ( ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) <-> ( ( P ` 0 ) e/ ( P " ( 1 ..^ R ) ) /\ ( P ` R ) e/ ( P " ( 1 ..^ R ) ) ) ) )
29 13 17 28 mpbir2and 
 |-  ( ( ph /\ ( # ` P ) e. NN ) -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) )
30 29 ex 
 |-  ( ph -> ( ( # ` P ) e. NN -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) ) )
31 9 30 syld 
 |-  ( ph -> ( -. ( # ` P ) = 0 -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) ) )
32 oveq1 
 |-  ( ( # ` P ) = 0 -> ( ( # ` P ) - 1 ) = ( 0 - 1 ) )
33 2 32 syl5eq 
 |-  ( ( # ` P ) = 0 -> R = ( 0 - 1 ) )
34 33 oveq2d 
 |-  ( ( # ` P ) = 0 -> ( 1 ..^ R ) = ( 1 ..^ ( 0 - 1 ) ) )
35 0le2 
 |-  0 <_ 2
36 1p1e2 
 |-  ( 1 + 1 ) = 2
37 35 36 breqtrri 
 |-  0 <_ ( 1 + 1 )
38 0re 
 |-  0 e. RR
39 1re 
 |-  1 e. RR
40 38 39 39 lesubadd2i 
 |-  ( ( 0 - 1 ) <_ 1 <-> 0 <_ ( 1 + 1 ) )
41 37 40 mpbir 
 |-  ( 0 - 1 ) <_ 1
42 1z 
 |-  1 e. ZZ
43 0z 
 |-  0 e. ZZ
44 peano2zm 
 |-  ( 0 e. ZZ -> ( 0 - 1 ) e. ZZ )
45 43 44 ax-mp 
 |-  ( 0 - 1 ) e. ZZ
46 fzon 
 |-  ( ( 1 e. ZZ /\ ( 0 - 1 ) e. ZZ ) -> ( ( 0 - 1 ) <_ 1 <-> ( 1 ..^ ( 0 - 1 ) ) = (/) ) )
47 42 45 46 mp2an 
 |-  ( ( 0 - 1 ) <_ 1 <-> ( 1 ..^ ( 0 - 1 ) ) = (/) )
48 41 47 mpbi 
 |-  ( 1 ..^ ( 0 - 1 ) ) = (/)
49 34 48 eqtrdi 
 |-  ( ( # ` P ) = 0 -> ( 1 ..^ R ) = (/) )
50 49 imaeq2d 
 |-  ( ( # ` P ) = 0 -> ( P " ( 1 ..^ R ) ) = ( P " (/) ) )
51 ima0 
 |-  ( P " (/) ) = (/)
52 50 51 eqtrdi 
 |-  ( ( # ` P ) = 0 -> ( P " ( 1 ..^ R ) ) = (/) )
53 52 ineq2d 
 |-  ( ( # ` P ) = 0 -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = ( ( P " { 0 , R } ) i^i (/) ) )
54 in0 
 |-  ( ( P " { 0 , R } ) i^i (/) ) = (/)
55 53 54 eqtrdi 
 |-  ( ( # ` P ) = 0 -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) )
56 31 55 pm2.61d2 
 |-  ( ph -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) )