Metamath Proof Explorer

Theorem 2pthdlem1

Description: Lemma 1 for 2pthd . (Contributed by AV, 14-Feb-2021)

Ref Expression
Hypotheses 2wlkd.p 
|- P = <" A B C ">
2wlkd.f 
|- F = <" J K ">
2wlkd.s 
|- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )
2wlkd.n 
|- ( ph -> ( A =/= B /\ B =/= C ) )
Assertion 2pthdlem1 
|- ( ph -> A. k e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ ( # ` F ) ) ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) )

Proof

Step Hyp Ref Expression
1 2wlkd.p 
 |-  P = <" A B C ">
2 2wlkd.f 
 |-  F = <" J K ">
3 2wlkd.s 
 |-  ( ph -> ( A e. V /\ B e. V /\ C e. V ) )
4 2wlkd.n 
 |-  ( ph -> ( A =/= B /\ B =/= C ) )
5 1 2 3 2wlkdlem3 
 |-  ( ph -> ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) )
6 simpl 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> ( P ` 0 ) = A )
7 simpr 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> ( P ` 1 ) = B )
8 6 7 neeq12d 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> ( ( P ` 0 ) =/= ( P ` 1 ) <-> A =/= B ) )
9 8 bicomd 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> ( A =/= B <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
10 9 3adant3 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( A =/= B <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
11 10 biimpcd 
 |-  ( A =/= B -> ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( P ` 0 ) =/= ( P ` 1 ) ) )
12 11 adantr 
 |-  ( ( A =/= B /\ B =/= C ) -> ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( P ` 0 ) =/= ( P ` 1 ) ) )
13 12 imp 
 |-  ( ( ( A =/= B /\ B =/= C ) /\ ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) ) -> ( P ` 0 ) =/= ( P ` 1 ) )
14 13 a1d 
 |-  ( ( ( A =/= B /\ B =/= C ) /\ ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) ) -> ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) )
15 eqid 
 |-  1 = 1
16 eqneqall 
 |-  ( 1 = 1 -> ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) )
17 15 16 mp1i 
 |-  ( ( ( A =/= B /\ B =/= C ) /\ ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) ) -> ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) )
18 simpr 
 |-  ( ( ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( P ` 2 ) = C )
19 simpl 
 |-  ( ( ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( P ` 1 ) = B )
20 18 19 neeq12d 
 |-  ( ( ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( ( P ` 2 ) =/= ( P ` 1 ) <-> C =/= B ) )
21 necom 
 |-  ( C =/= B <-> B =/= C )
22 20 21 bitr2di 
 |-  ( ( ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( B =/= C <-> ( P ` 2 ) =/= ( P ` 1 ) ) )
23 22 3adant1 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( B =/= C <-> ( P ` 2 ) =/= ( P ` 1 ) ) )
24 23 biimpcd 
 |-  ( B =/= C -> ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( P ` 2 ) =/= ( P ` 1 ) ) )
25 24 adantl 
 |-  ( ( A =/= B /\ B =/= C ) -> ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( P ` 2 ) =/= ( P ` 1 ) ) )
26 25 imp 
 |-  ( ( ( A =/= B /\ B =/= C ) /\ ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) ) -> ( P ` 2 ) =/= ( P ` 1 ) )
27 26 a1d 
 |-  ( ( ( A =/= B /\ B =/= C ) /\ ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) ) -> ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) )
28 14 17 27 3jca 
 |-  ( ( ( A =/= B /\ B =/= C ) /\ ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) ) -> ( ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) /\ ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) /\ ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) ) )
29 4 5 28 syl2anc 
 |-  ( ph -> ( ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) /\ ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) /\ ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) ) )
30 1 fveq2i 
 |-  ( # ` P ) = ( # ` <" A B C "> )
31 s3len 
 |-  ( # ` <" A B C "> ) = 3
32 30 31 eqtri 
 |-  ( # ` P ) = 3
33 32 oveq2i 
 |-  ( 0 ..^ ( # ` P ) ) = ( 0 ..^ 3 )
34 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
35 33 34 eqtri 
 |-  ( 0 ..^ ( # ` P ) ) = { 0 , 1 , 2 }
36 35 raleqi 
 |-  ( A. k e. ( 0 ..^ ( # ` P ) ) ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) <-> A. k e. { 0 , 1 , 2 } ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) )
37 c0ex 
 |-  0 e. _V
38 1ex 
 |-  1 e. _V
39 2ex 
 |-  2 e. _V
40 neeq1 
 |-  ( k = 0 -> ( k =/= 1 <-> 0 =/= 1 ) )
41 fveq2 
 |-  ( k = 0 -> ( P ` k ) = ( P ` 0 ) )
42 41 neeq1d 
 |-  ( k = 0 -> ( ( P ` k ) =/= ( P ` 1 ) <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
43 40 42 imbi12d 
 |-  ( k = 0 -> ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) <-> ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) ) )
44 neeq1 
 |-  ( k = 1 -> ( k =/= 1 <-> 1 =/= 1 ) )
45 fveq2 
 |-  ( k = 1 -> ( P ` k ) = ( P ` 1 ) )
46 45 neeq1d 
 |-  ( k = 1 -> ( ( P ` k ) =/= ( P ` 1 ) <-> ( P ` 1 ) =/= ( P ` 1 ) ) )
47 44 46 imbi12d 
 |-  ( k = 1 -> ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) <-> ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) ) )
48 neeq1 
 |-  ( k = 2 -> ( k =/= 1 <-> 2 =/= 1 ) )
49 fveq2 
 |-  ( k = 2 -> ( P ` k ) = ( P ` 2 ) )
50 49 neeq1d 
 |-  ( k = 2 -> ( ( P ` k ) =/= ( P ` 1 ) <-> ( P ` 2 ) =/= ( P ` 1 ) ) )
51 48 50 imbi12d 
 |-  ( k = 2 -> ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) <-> ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) ) )
52 37 38 39 43 47 51 raltp 
 |-  ( A. k e. { 0 , 1 , 2 } ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) <-> ( ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) /\ ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) /\ ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) ) )
53 36 52 bitri 
 |-  ( A. k e. ( 0 ..^ ( # ` P ) ) ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) <-> ( ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) /\ ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) /\ ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) ) )
54 29 53 sylibr 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` P ) ) ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) )
55 2 fveq2i 
 |-  ( # ` F ) = ( # ` <" J K "> )
56 s2len 
 |-  ( # ` <" J K "> ) = 2
57 55 56 eqtri 
 |-  ( # ` F ) = 2
58 57 oveq2i 
 |-  ( 1 ..^ ( # ` F ) ) = ( 1 ..^ 2 )
59 fzo12sn 
 |-  ( 1 ..^ 2 ) = { 1 }
60 58 59 eqtri 
 |-  ( 1 ..^ ( # ` F ) ) = { 1 }
61 60 raleqi 
 |-  ( A. j e. ( 1 ..^ ( # ` F ) ) ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) <-> A. j e. { 1 } ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) )
62 neeq2 
 |-  ( j = 1 -> ( k =/= j <-> k =/= 1 ) )
63 fveq2 
 |-  ( j = 1 -> ( P ` j ) = ( P ` 1 ) )
64 63 neeq2d 
 |-  ( j = 1 -> ( ( P ` k ) =/= ( P ` j ) <-> ( P ` k ) =/= ( P ` 1 ) ) )
65 62 64 imbi12d 
 |-  ( j = 1 -> ( ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) <-> ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) ) )
66 38 65 ralsn 
 |-  ( A. j e. { 1 } ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) <-> ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) )
67 61 66 bitri 
 |-  ( A. j e. ( 1 ..^ ( # ` F ) ) ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) <-> ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) )
68 67 ralbii 
 |-  ( A. k e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ ( # ` F ) ) ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) <-> A. k e. ( 0 ..^ ( # ` P ) ) ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) )
69 54 68 sylibr 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ ( # ` F ) ) ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) )