Metamath Proof Explorer

Theorem pthdlem2lem

Description: Lemma for pthdlem2 . (Contributed 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 pthdlem2lem 
|- ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> ( P ` I ) e/ ( 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 3 3ad2ant1 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> A. i e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )
5 ralcom 
 |-  ( A. i e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) <-> A. j e. ( 1 ..^ R ) A. i e. ( 0 ..^ ( # ` P ) ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )
6 elfzo1 
 |-  ( j e. ( 1 ..^ R ) <-> ( j e. NN /\ R e. NN /\ j < R ) )
7 nnne0 
 |-  ( j e. NN -> j =/= 0 )
8 7 necomd 
 |-  ( j e. NN -> 0 =/= j )
9 8 3ad2ant1 
 |-  ( ( j e. NN /\ R e. NN /\ j < R ) -> 0 =/= j )
10 6 9 sylbi 
 |-  ( j e. ( 1 ..^ R ) -> 0 =/= j )
11 10 adantl 
 |-  ( ( ( # ` P ) e. NN /\ j e. ( 1 ..^ R ) ) -> 0 =/= j )
12 neeq1 
 |-  ( I = 0 -> ( I =/= j <-> 0 =/= j ) )
13 11 12 syl5ibr 
 |-  ( I = 0 -> ( ( ( # ` P ) e. NN /\ j e. ( 1 ..^ R ) ) -> I =/= j ) )
14 13 expd 
 |-  ( I = 0 -> ( ( # ` P ) e. NN -> ( j e. ( 1 ..^ R ) -> I =/= j ) ) )
15 nnre 
 |-  ( j e. NN -> j e. RR )
16 15 adantr 
 |-  ( ( j e. NN /\ R e. NN ) -> j e. RR )
17 nnre 
 |-  ( R e. NN -> R e. RR )
18 17 adantl 
 |-  ( ( j e. NN /\ R e. NN ) -> R e. RR )
19 16 18 ltlend 
 |-  ( ( j e. NN /\ R e. NN ) -> ( j < R <-> ( j <_ R /\ R =/= j ) ) )
20 simpr 
 |-  ( ( j <_ R /\ R =/= j ) -> R =/= j )
21 19 20 syl6bi 
 |-  ( ( j e. NN /\ R e. NN ) -> ( j < R -> R =/= j ) )
22 21 3impia 
 |-  ( ( j e. NN /\ R e. NN /\ j < R ) -> R =/= j )
23 6 22 sylbi 
 |-  ( j e. ( 1 ..^ R ) -> R =/= j )
24 23 adantl 
 |-  ( ( ( # ` P ) e. NN /\ j e. ( 1 ..^ R ) ) -> R =/= j )
25 neeq1 
 |-  ( I = R -> ( I =/= j <-> R =/= j ) )
26 24 25 syl5ibr 
 |-  ( I = R -> ( ( ( # ` P ) e. NN /\ j e. ( 1 ..^ R ) ) -> I =/= j ) )
27 26 expd 
 |-  ( I = R -> ( ( # ` P ) e. NN -> ( j e. ( 1 ..^ R ) -> I =/= j ) ) )
28 14 27 jaoi 
 |-  ( ( I = 0 \/ I = R ) -> ( ( # ` P ) e. NN -> ( j e. ( 1 ..^ R ) -> I =/= j ) ) )
29 28 impcom 
 |-  ( ( ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> ( j e. ( 1 ..^ R ) -> I =/= j ) )
30 29 3adant1 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> ( j e. ( 1 ..^ R ) -> I =/= j ) )
31 30 imp 
 |-  ( ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) /\ j e. ( 1 ..^ R ) ) -> I =/= j )
32 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` P ) ) <-> ( # ` P ) e. NN )
33 32 biimpri 
 |-  ( ( # ` P ) e. NN -> 0 e. ( 0 ..^ ( # ` P ) ) )
34 eleq1 
 |-  ( I = 0 -> ( I e. ( 0 ..^ ( # ` P ) ) <-> 0 e. ( 0 ..^ ( # ` P ) ) ) )
35 33 34 syl5ibr 
 |-  ( I = 0 -> ( ( # ` P ) e. NN -> I e. ( 0 ..^ ( # ` P ) ) ) )
36 fzo0end 
 |-  ( ( # ` P ) e. NN -> ( ( # ` P ) - 1 ) e. ( 0 ..^ ( # ` P ) ) )
37 2 36 eqeltrid 
 |-  ( ( # ` P ) e. NN -> R e. ( 0 ..^ ( # ` P ) ) )
38 eleq1 
 |-  ( I = R -> ( I e. ( 0 ..^ ( # ` P ) ) <-> R e. ( 0 ..^ ( # ` P ) ) ) )
39 37 38 syl5ibr 
 |-  ( I = R -> ( ( # ` P ) e. NN -> I e. ( 0 ..^ ( # ` P ) ) ) )
40 35 39 jaoi 
 |-  ( ( I = 0 \/ I = R ) -> ( ( # ` P ) e. NN -> I e. ( 0 ..^ ( # ` P ) ) ) )
41 40 impcom 
 |-  ( ( ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> I e. ( 0 ..^ ( # ` P ) ) )
42 41 3adant1 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> I e. ( 0 ..^ ( # ` P ) ) )
43 42 adantr 
 |-  ( ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) /\ j e. ( 1 ..^ R ) ) -> I e. ( 0 ..^ ( # ` P ) ) )
44 neeq1 
 |-  ( i = I -> ( i =/= j <-> I =/= j ) )
45 fveq2 
 |-  ( i = I -> ( P ` i ) = ( P ` I ) )
46 45 neeq1d 
 |-  ( i = I -> ( ( P ` i ) =/= ( P ` j ) <-> ( P ` I ) =/= ( P ` j ) ) )
47 44 46 imbi12d 
 |-  ( i = I -> ( ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) <-> ( I =/= j -> ( P ` I ) =/= ( P ` j ) ) ) )
48 47 rspcv 
 |-  ( I e. ( 0 ..^ ( # ` P ) ) -> ( A. i e. ( 0 ..^ ( # ` P ) ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) -> ( I =/= j -> ( P ` I ) =/= ( P ` j ) ) ) )
49 43 48 syl 
 |-  ( ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) /\ j e. ( 1 ..^ R ) ) -> ( A. i e. ( 0 ..^ ( # ` P ) ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) -> ( I =/= j -> ( P ` I ) =/= ( P ` j ) ) ) )
50 31 49 mpid 
 |-  ( ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) /\ j e. ( 1 ..^ R ) ) -> ( A. i e. ( 0 ..^ ( # ` P ) ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) -> ( P ` I ) =/= ( P ` j ) ) )
51 nesym 
 |-  ( ( P ` I ) =/= ( P ` j ) <-> -. ( P ` j ) = ( P ` I ) )
52 50 51 syl6ib 
 |-  ( ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) /\ j e. ( 1 ..^ R ) ) -> ( A. i e. ( 0 ..^ ( # ` P ) ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) -> -. ( P ` j ) = ( P ` I ) ) )
53 52 ralimdva 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> ( A. j e. ( 1 ..^ R ) A. i e. ( 0 ..^ ( # ` P ) ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) -> A. j e. ( 1 ..^ R ) -. ( P ` j ) = ( P ` I ) ) )
54 5 53 syl5bi 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> ( A. i e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) -> A. j e. ( 1 ..^ R ) -. ( P ` j ) = ( P ` I ) ) )
55 4 54 mpd 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> A. j e. ( 1 ..^ R ) -. ( P ` j ) = ( P ` I ) )
56 ralnex 
 |-  ( A. j e. ( 1 ..^ R ) -. ( P ` j ) = ( P ` I ) <-> -. E. j e. ( 1 ..^ R ) ( P ` j ) = ( P ` I ) )
57 55 56 sylib 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> -. E. j e. ( 1 ..^ R ) ( P ` j ) = ( P ` I ) )
58 wrdf 
 |-  ( P e. Word _V -> P : ( 0 ..^ ( # ` P ) ) --> _V )
59 ffun 
 |-  ( P : ( 0 ..^ ( # ` P ) ) --> _V -> Fun P )
60 1 58 59 3syl 
 |-  ( ph -> Fun P )
61 60 3ad2ant1 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> Fun P )
62 fvelima 
 |-  ( ( Fun P /\ ( P ` I ) e. ( P " ( 1 ..^ R ) ) ) -> E. j e. ( 1 ..^ R ) ( P ` j ) = ( P ` I ) )
63 62 ex 
 |-  ( Fun P -> ( ( P ` I ) e. ( P " ( 1 ..^ R ) ) -> E. j e. ( 1 ..^ R ) ( P ` j ) = ( P ` I ) ) )
64 61 63 syl 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> ( ( P ` I ) e. ( P " ( 1 ..^ R ) ) -> E. j e. ( 1 ..^ R ) ( P ` j ) = ( P ` I ) ) )
65 57 64 mtod 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> -. ( P ` I ) e. ( P " ( 1 ..^ R ) ) )
66 df-nel 
 |-  ( ( P ` I ) e/ ( P " ( 1 ..^ R ) ) <-> -. ( P ` I ) e. ( P " ( 1 ..^ R ) ) )
67 65 66 sylibr 
 |-  ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> ( P ` I ) e/ ( P " ( 1 ..^ R ) ) )