Metamath Proof Explorer

Theorem pgnioedg2

Description: An inside and an outside vertex not adjacent in a Petersen graph. (Contributed by AV, 21-Nov-2025)

Ref Expression
Hypotheses pgnioedg1.g 
|- G = ( 5 gPetersenGr 2 )
pgnioedg1.e 
|- E = ( Edg ` G )
Assertion pgnioedg2 
|- ( y e. ( 0 ..^ 5 ) -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )

Proof

Step Hyp Ref Expression
1 pgnioedg1.g 
 |-  G = ( 5 gPetersenGr 2 )
2 pgnioedg1.e 
 |-  E = ( Edg ` G )
3 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
4 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
5 3 4 pm3.2i 
 |-  ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
6 1ex 
 |-  1 e. _V
7 ovex 
 |-  ( ( y + 2 ) mod 5 ) e. _V
8 6 7 op1st 
 |-  ( 1st ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) = 1
9 simpr 
 |-  ( ( y e. ( 0 ..^ 5 ) /\ { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) -> { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
10 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
11 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
12 10 1 11 2 gpgvtxedg1 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( 1st ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) = 1 /\ { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) -> ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) + 2 ) mod 5 ) >. \/ <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 0 , ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) >. \/ <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) - 2 ) mod 5 ) >. ) )
13 5 8 9 12 mp3an12i 
 |-  ( ( y e. ( 0 ..^ 5 ) /\ { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) -> ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) + 2 ) mod 5 ) >. \/ <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 0 , ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) >. \/ <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) - 2 ) mod 5 ) >. ) )
14 13 ex 
 |-  ( y e. ( 0 ..^ 5 ) -> ( { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E -> ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) + 2 ) mod 5 ) >. \/ <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 0 , ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) >. \/ <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) - 2 ) mod 5 ) >. ) ) )
15 c0ex 
 |-  0 e. _V
16 ovex 
 |-  ( ( y + 1 ) mod 5 ) e. _V
17 15 16 opth 
 |-  ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) + 2 ) mod 5 ) >. <-> ( 0 = 1 /\ ( ( y + 1 ) mod 5 ) = ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) + 2 ) mod 5 ) ) )
18 0ne1 
 |-  0 =/= 1
19 eqneqall 
 |-  ( 0 = 1 -> ( 0 =/= 1 -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
20 18 19 mpi 
 |-  ( 0 = 1 -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
21 20 adantr 
 |-  ( ( 0 = 1 /\ ( ( y + 1 ) mod 5 ) = ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) + 2 ) mod 5 ) ) -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
22 17 21 sylbi 
 |-  ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) + 2 ) mod 5 ) >. -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
23 22 a1i 
 |-  ( y e. ( 0 ..^ 5 ) -> ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) + 2 ) mod 5 ) >. -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
24 15 16 opth 
 |-  ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 0 , ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) >. <-> ( 0 = 0 /\ ( ( y + 1 ) mod 5 ) = ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) ) )
25 6 7 op2nd 
 |-  ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) = ( ( y + 2 ) mod 5 )
26 25 eqeq2i 
 |-  ( ( ( y + 1 ) mod 5 ) = ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) <-> ( ( y + 1 ) mod 5 ) = ( ( y + 2 ) mod 5 ) )
27 5nn 
 |-  5 e. NN
28 27 nnzi 
 |-  5 e. ZZ
29 uzid 
 |-  ( 5 e. ZZ -> 5 e. ( ZZ>= ` 5 ) )
30 28 29 ax-mp 
 |-  5 e. ( ZZ>= ` 5 )
31 eqid 
 |-  ( 0 ..^ 5 ) = ( 0 ..^ 5 )
32 31 modp2nep1 
 |-  ( ( 5 e. ( ZZ>= ` 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( y + 2 ) mod 5 ) =/= ( ( y + 1 ) mod 5 ) )
33 32 necomd 
 |-  ( ( 5 e. ( ZZ>= ` 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( y + 1 ) mod 5 ) =/= ( ( y + 2 ) mod 5 ) )
34 30 33 mpan 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y + 1 ) mod 5 ) =/= ( ( y + 2 ) mod 5 ) )
35 eqneqall 
 |-  ( ( ( y + 1 ) mod 5 ) = ( ( y + 2 ) mod 5 ) -> ( ( ( y + 1 ) mod 5 ) =/= ( ( y + 2 ) mod 5 ) -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
36 34 35 syl5 
 |-  ( ( ( y + 1 ) mod 5 ) = ( ( y + 2 ) mod 5 ) -> ( y e. ( 0 ..^ 5 ) -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
37 26 36 sylbi 
 |-  ( ( ( y + 1 ) mod 5 ) = ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( y e. ( 0 ..^ 5 ) -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
38 24 37 simplbiim 
 |-  ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 0 , ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) >. -> ( y e. ( 0 ..^ 5 ) -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
39 38 com12 
 |-  ( y e. ( 0 ..^ 5 ) -> ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 0 , ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) >. -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
40 15 16 opth 
 |-  ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) - 2 ) mod 5 ) >. <-> ( 0 = 1 /\ ( ( y + 1 ) mod 5 ) = ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) - 2 ) mod 5 ) ) )
41 20 adantr 
 |-  ( ( 0 = 1 /\ ( ( y + 1 ) mod 5 ) = ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) - 2 ) mod 5 ) ) -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
42 40 41 sylbi 
 |-  ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) - 2 ) mod 5 ) >. -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )
43 42 a1i 
 |-  ( y e. ( 0 ..^ 5 ) -> ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) - 2 ) mod 5 ) >. -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
44 23 39 43 3jaod 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) + 2 ) mod 5 ) >. \/ <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 0 , ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) >. \/ <. 0 , ( ( y + 1 ) mod 5 ) >. = <. 1 , ( ( ( 2nd ` <. 1 , ( ( y + 2 ) mod 5 ) >. ) - 2 ) mod 5 ) >. ) -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
45 14 44 syld 
 |-  ( y e. ( 0 ..^ 5 ) -> ( { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E ) )
46 45 pm2.01d 
 |-  ( y e. ( 0 ..^ 5 ) -> -. { <. 1 , ( ( y + 2 ) mod 5 ) >. , <. 0 , ( ( y + 1 ) mod 5 ) >. } e. E )