Metamath Proof Explorer

Theorem pgnbgreunbgrlem5lem1

Description: Lemma 1 for pgnbgreunbgrlem5 . (Contributed by AV, 21-Nov-2025)

Ref Expression
Hypotheses pgnbgreunbgr.g 
|- G = ( 5 gPetersenGr 2 )
pgnbgreunbgr.v 
|- V = ( Vtx ` G )
pgnbgreunbgr.e 
|- E = ( Edg ` G )
pgnbgreunbgr.n 
|- N = ( G NeighbVtx X )
Assertion pgnbgreunbgrlem5lem1 
|- ( ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 1 , b >. } e. E ) -> -. { <. 1 , b >. , L } e. E )

Proof

Step Hyp Ref Expression
1 pgnbgreunbgr.g 
 |-  G = ( 5 gPetersenGr 2 )
2 pgnbgreunbgr.v 
 |-  V = ( Vtx ` G )
3 pgnbgreunbgr.e 
 |-  E = ( Edg ` G )
4 pgnbgreunbgr.n 
 |-  N = ( G NeighbVtx X )
5 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
6 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
7 5 6 pm3.2i 
 |-  ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
8 1ex 
 |-  1 e. _V
9 vex 
 |-  y e. _V
10 8 9 op1st 
 |-  ( 1st ` <. 1 , y >. ) = 1
11 simpr 
 |-  ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ { <. 1 , y >. , <. 1 , b >. } e. E ) -> { <. 1 , y >. , <. 1 , b >. } e. E )
12 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
13 12 1 2 3 gpgvtxedg1 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( 1st ` <. 1 , y >. ) = 1 /\ { <. 1 , y >. , <. 1 , b >. } e. E ) -> ( <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) + 2 ) mod 5 ) >. \/ <. 1 , b >. = <. 0 , ( 2nd ` <. 1 , y >. ) >. \/ <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) - 2 ) mod 5 ) >. ) )
14 7 10 11 13 mp3an12i 
 |-  ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ { <. 1 , y >. , <. 1 , b >. } e. E ) -> ( <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) + 2 ) mod 5 ) >. \/ <. 1 , b >. = <. 0 , ( 2nd ` <. 1 , y >. ) >. \/ <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) - 2 ) mod 5 ) >. ) )
15 14 ex 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 1 , y >. , <. 1 , b >. } e. E -> ( <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) + 2 ) mod 5 ) >. \/ <. 1 , b >. = <. 0 , ( 2nd ` <. 1 , y >. ) >. \/ <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) - 2 ) mod 5 ) >. ) ) )
16 vex 
 |-  b e. _V
17 8 16 opth 
 |-  ( <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) + 2 ) mod 5 ) >. <-> ( 1 = 1 /\ b = ( ( ( 2nd ` <. 1 , y >. ) + 2 ) mod 5 ) ) )
18 8 9 op2nd 
 |-  ( 2nd ` <. 1 , y >. ) = y
19 18 oveq1i 
 |-  ( ( 2nd ` <. 1 , y >. ) + 2 ) = ( y + 2 )
20 19 oveq1i 
 |-  ( ( ( 2nd ` <. 1 , y >. ) + 2 ) mod 5 ) = ( ( y + 2 ) mod 5 )
21 20 eqeq2i 
 |-  ( b = ( ( ( 2nd ` <. 1 , y >. ) + 2 ) mod 5 ) <-> b = ( ( y + 2 ) mod 5 ) )
22 1 3 pgnioedg2 
 |-  ( y e. ( 0 ..^ 5 ) -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
23 22 adantl 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
24 opeq2 
 |-  ( b = ( ( y + 2 ) mod 5 ) -> <. 1 , b >. = <. 1 , ( ( y + 2 ) mod 5 ) >. )
25 24 preq1d 
 |-  ( b = ( ( y + 2 ) mod 5 ) -> { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } = { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } )
26 25 eleq1d 
 |-  ( b = ( ( y + 2 ) mod 5 ) -> ( { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E <-> { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
27 26 notbid 
 |-  ( b = ( ( y + 2 ) mod 5 ) -> ( -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E <-> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
28 23 27 imbitrrid 
 |-  ( b = ( ( y + 2 ) mod 5 ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
29 21 28 sylbi 
 |-  ( b = ( ( ( 2nd ` <. 1 , y >. ) + 2 ) mod 5 ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
30 17 29 simplbiim 
 |-  ( <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) + 2 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
31 30 com12 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) + 2 ) mod 5 ) >. -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
32 8 16 opth 
 |-  ( <. 1 , b >. = <. 0 , ( 2nd ` <. 1 , y >. ) >. <-> ( 1 = 0 /\ b = ( 2nd ` <. 1 , y >. ) ) )
33 ax-1ne0 
 |-  1 =/= 0
34 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
35 33 34 mpi 
 |-  ( 1 = 0 -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
36 35 adantr 
 |-  ( ( 1 = 0 /\ b = ( 2nd ` <. 1 , y >. ) ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
37 32 36 sylbi 
 |-  ( <. 1 , b >. = <. 0 , ( 2nd ` <. 1 , y >. ) >. -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
38 37 a1i 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( <. 1 , b >. = <. 0 , ( 2nd ` <. 1 , y >. ) >. -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
39 8 16 opth 
 |-  ( <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) - 2 ) mod 5 ) >. <-> ( 1 = 1 /\ b = ( ( ( 2nd ` <. 1 , y >. ) - 2 ) mod 5 ) ) )
40 18 oveq1i 
 |-  ( ( 2nd ` <. 1 , y >. ) - 2 ) = ( y - 2 )
41 40 oveq1i 
 |-  ( ( ( 2nd ` <. 1 , y >. ) - 2 ) mod 5 ) = ( ( y - 2 ) mod 5 )
42 41 eqeq2i 
 |-  ( b = ( ( ( 2nd ` <. 1 , y >. ) - 2 ) mod 5 ) <-> b = ( ( y - 2 ) mod 5 ) )
43 1 3 pgnioedg1 
 |-  ( y e. ( 0 ..^ 5 ) -> -. { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
44 43 adantl 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> -. { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
45 opeq2 
 |-  ( b = ( ( y - 2 ) mod 5 ) -> <. 1 , b >. = <. 1 , ( ( y - 2 ) mod 5 ) >. )
46 45 preq1d 
 |-  ( b = ( ( y - 2 ) mod 5 ) -> { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } = { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } )
47 46 eleq1d 
 |-  ( b = ( ( y - 2 ) mod 5 ) -> ( { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E <-> { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
48 47 notbid 
 |-  ( b = ( ( y - 2 ) mod 5 ) -> ( -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E <-> -. { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
49 44 48 imbitrrid 
 |-  ( b = ( ( y - 2 ) mod 5 ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
50 42 49 sylbi 
 |-  ( b = ( ( ( 2nd ` <. 1 , y >. ) - 2 ) mod 5 ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
51 39 50 simplbiim 
 |-  ( <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) - 2 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
52 51 com12 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) - 2 ) mod 5 ) >. -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
53 31 38 52 3jaod 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) + 2 ) mod 5 ) >. \/ <. 1 , b >. = <. 0 , ( 2nd ` <. 1 , y >. ) >. \/ <. 1 , b >. = <. 1 , ( ( ( 2nd ` <. 1 , y >. ) - 2 ) mod 5 ) >. ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
54 15 53 syld 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 1 , y >. , <. 1 , b >. } e. E -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
55 54 adantl 
 |-  ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { <. 1 , y >. , <. 1 , b >. } e. E -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
56 preq1 
 |-  ( K = <. 1 , y >. -> { K , <. 1 , b >. } = { <. 1 , y >. , <. 1 , b >. } )
57 56 eleq1d 
 |-  ( K = <. 1 , y >. -> ( { K , <. 1 , b >. } e. E <-> { <. 1 , y >. , <. 1 , b >. } e. E ) )
58 57 adantl 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( { K , <. 1 , b >. } e. E <-> { <. 1 , y >. , <. 1 , b >. } e. E ) )
59 preq2 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> { <. 1 , b >. , L } = { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } )
60 59 eleq1d 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( { <. 1 , b >. , L } e. E <-> { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
61 60 notbid 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( -. { <. 1 , b >. , L } e. E <-> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
62 61 adantr 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( -. { <. 1 , b >. , L } e. E <-> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
63 58 62 imbi12d 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) -> ( ( { K , <. 1 , b >. } e. E -> -. { <. 1 , b >. , L } e. E ) <-> ( { <. 1 , y >. , <. 1 , b >. } e. E -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) ) )
64 63 adantr 
 |-  ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E -> -. { <. 1 , b >. , L } e. E ) <-> ( { <. 1 , y >. , <. 1 , b >. } e. E -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) ) )
65 55 64 mpbird 
 |-  ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { K , <. 1 , b >. } e. E -> -. { <. 1 , b >. , L } e. E ) )
66 65 imp 
 |-  ( ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 1 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 1 , b >. } e. E ) -> -. { <. 1 , b >. , L } e. E )