Metamath Proof Explorer

Theorem pgnbgreunbgrlem5lem3

Description: Lemma 3 for pgnbgreunbgrlem5 . (Contributed by AV, 20-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 pgnbgreunbgrlem5lem3 
|- ( ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( 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 c0ex 
 |-  0 e. _V
9 ovex 
 |-  ( ( y - 1 ) mod 5 ) e. _V
10 8 9 op1st 
 |-  ( 1st ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) = 0
11 simpr 
 |-  ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 1 , b >. } e. E ) -> { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 1 , b >. } e. E )
12 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
13 12 1 2 3 gpgvtxedg0 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( 1st ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) = 0 /\ { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 1 , b >. } e. E ) -> ( <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) + 1 ) mod 5 ) >. \/ <. 1 , b >. = <. 1 , ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) >. \/ <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) - 1 ) mod 5 ) >. ) )
14 7 10 11 13 mp3an12i 
 |-  ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 1 , b >. } e. E ) -> ( <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) + 1 ) mod 5 ) >. \/ <. 1 , b >. = <. 1 , ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) >. \/ <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) - 1 ) mod 5 ) >. ) )
15 14 ex 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 1 , b >. } e. E -> ( <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) + 1 ) mod 5 ) >. \/ <. 1 , b >. = <. 1 , ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) >. \/ <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) - 1 ) mod 5 ) >. ) ) )
16 1ex 
 |-  1 e. _V
17 vex 
 |-  b e. _V
18 16 17 opth 
 |-  ( <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) + 1 ) mod 5 ) >. <-> ( 1 = 0 /\ b = ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) + 1 ) mod 5 ) ) )
19 ax-1ne0 
 |-  1 =/= 0
20 19 a1i 
 |-  ( { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E -> 1 =/= 0 )
21 20 necon2bi 
 |-  ( 1 = 0 -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
22 21 adantr 
 |-  ( ( 1 = 0 /\ b = ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) + 1 ) mod 5 ) ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
23 18 22 sylbi 
 |-  ( <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) + 1 ) mod 5 ) >. -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
24 23 a1i 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) + 1 ) mod 5 ) >. -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
25 16 17 opth 
 |-  ( <. 1 , b >. = <. 1 , ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) >. <-> ( 1 = 1 /\ b = ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) ) )
26 8 9 op2nd 
 |-  ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) = ( ( y - 1 ) mod 5 )
27 26 eqeq2i 
 |-  ( b = ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) <-> b = ( ( y - 1 ) mod 5 ) )
28 1 3 pgnioedg5 
 |-  ( y e. ( 0 ..^ 5 ) -> -. { <. 1 , ( ( y - 1 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
29 28 adantl 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> -. { <. 1 , ( ( y - 1 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
30 opeq2 
 |-  ( b = ( ( y - 1 ) mod 5 ) -> <. 1 , b >. = <. 1 , ( ( y - 1 ) mod 5 ) >. )
31 30 preq1d 
 |-  ( b = ( ( y - 1 ) mod 5 ) -> { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } = { <. 1 , ( ( y - 1 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } )
32 31 eleq1d 
 |-  ( b = ( ( y - 1 ) mod 5 ) -> ( { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E <-> { <. 1 , ( ( y - 1 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
33 32 notbid 
 |-  ( b = ( ( y - 1 ) mod 5 ) -> ( -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E <-> -. { <. 1 , ( ( y - 1 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
34 29 33 imbitrrid 
 |-  ( b = ( ( y - 1 ) mod 5 ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
35 27 34 sylbi 
 |-  ( b = ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
36 25 35 simplbiim 
 |-  ( <. 1 , b >. = <. 1 , ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
37 36 com12 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( <. 1 , b >. = <. 1 , ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) >. -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
38 16 17 opth 
 |-  ( <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) - 1 ) mod 5 ) >. <-> ( 1 = 0 /\ b = ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) - 1 ) mod 5 ) ) )
39 21 adantr 
 |-  ( ( 1 = 0 /\ b = ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) - 1 ) mod 5 ) ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
40 38 39 sylbi 
 |-  ( <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) - 1 ) mod 5 ) >. -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
41 40 a1i 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) - 1 ) mod 5 ) >. -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
42 24 37 41 3jaod 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) + 1 ) mod 5 ) >. \/ <. 1 , b >. = <. 1 , ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) >. \/ <. 1 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , ( ( y - 1 ) mod 5 ) >. ) - 1 ) mod 5 ) >. ) -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
43 15 42 syld 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 1 , b >. } e. E -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
44 43 adantl 
 |-  ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 1 , b >. } e. E -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
45 preq1 
 |-  ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. -> { K , <. 1 , b >. } = { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 1 , b >. } )
46 45 eleq1d 
 |-  ( K = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( { K , <. 1 , b >. } e. E <-> { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 1 , b >. } e. E ) )
47 46 adantl 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( { K , <. 1 , b >. } e. E <-> { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 1 , b >. } e. E ) )
48 preq2 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> { <. 1 , b >. , L } = { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } )
49 48 eleq1d 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( { <. 1 , b >. , L } e. E <-> { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
50 49 notbid 
 |-  ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. -> ( -. { <. 1 , b >. , L } e. E <-> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
51 50 adantr 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( -. { <. 1 , b >. , L } e. E <-> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
52 47 51 imbi12d 
 |-  ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) -> ( ( { K , <. 1 , b >. } e. E -> -. { <. 1 , b >. , L } e. E ) <-> ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 1 , b >. } e. E -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) ) )
53 52 adantr 
 |-  ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 1 , b >. } e. E -> -. { <. 1 , b >. , L } e. E ) <-> ( { <. 0 , ( ( y - 1 ) mod 5 ) >. , <. 1 , b >. } e. E -> -. { <. 1 , b >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) ) )
54 44 53 mpbird 
 |-  ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { K , <. 1 , b >. } e. E -> -. { <. 1 , b >. , L } e. E ) )
55 54 imp 
 |-  ( ( ( ( L = <. 0 , ( ( y + 1 ) mod 5 ) >. /\ K = <. 0 , ( ( y - 1 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 1 , b >. } e. E ) -> -. { <. 1 , b >. , L } e. E )