Metamath Proof Explorer

Theorem gpg3nbgrvtx1

Description: In a generalized Petersen graph G , every vertex of the second kind has exactly three (different) neighbors. (Contributed by AV, 3-Sep-2025)

Ref Expression
Hypotheses gpgnbgr.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgnbgr.g 
|- G = ( N gPetersenGr K )
gpgnbgr.v 
|- V = ( Vtx ` G )
gpgnbgr.u 
|- U = ( G NeighbVtx X )
Assertion gpg3nbgrvtx1 
|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( # ` U ) = 3 )

Proof

Step Hyp Ref Expression
1 gpgnbgr.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpgnbgr.g 
 |-  G = ( N gPetersenGr K )
3 gpgnbgr.v 
 |-  V = ( Vtx ` G )
4 gpgnbgr.u 
 |-  U = ( G NeighbVtx X )
5 1 2 3 4 gpgnbgrvtx1 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> U = { <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } )
6 5 fveq2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( # ` U ) = ( # ` { <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } ) )
7 ax-1ne0 
 |-  1 =/= 0
8 7 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> 1 =/= 0 )
9 8 orcd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( 1 =/= 0 \/ ( ( ( 2nd ` X ) + K ) mod N ) =/= ( 2nd ` X ) ) )
10 1ex 
 |-  1 e. _V
11 ovex 
 |-  ( ( ( 2nd ` X ) + K ) mod N ) e. _V
12 10 11 opthne 
 |-  ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. =/= <. 0 , ( 2nd ` X ) >. <-> ( 1 =/= 0 \/ ( ( ( 2nd ` X ) + K ) mod N ) =/= ( 2nd ` X ) ) )
13 9 12 sylibr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. =/= <. 0 , ( 2nd ` X ) >. )
14 0ne1 
 |-  0 =/= 1
15 14 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> 0 =/= 1 )
16 15 orcd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( 0 =/= 1 \/ ( 2nd ` X ) =/= ( ( ( 2nd ` X ) - K ) mod N ) ) )
17 c0ex 
 |-  0 e. _V
18 fvex 
 |-  ( 2nd ` X ) e. _V
19 17 18 opthne 
 |-  ( <. 0 , ( 2nd ` X ) >. =/= <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. <-> ( 0 =/= 1 \/ ( 2nd ` X ) =/= ( ( ( 2nd ` X ) - K ) mod N ) ) )
20 16 19 sylibr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> <. 0 , ( 2nd ` X ) >. =/= <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. )
21 simpll 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> N e. ( ZZ>= ` 3 ) )
22 1 eleq2i 
 |-  ( K e. J <-> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
23 22 biimpi 
 |-  ( K e. J -> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
24 23 ad2antlr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
25 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
26 25 1 2 3 gpgvtxel2 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> ( 2nd ` X ) e. ( 0 ..^ N ) )
27 26 adantrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( 2nd ` X ) e. ( 0 ..^ N ) )
28 gpg3nbgrvtxlem 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) /\ ( 2nd ` X ) e. ( 0 ..^ N ) ) -> ( ( ( 2nd ` X ) + K ) mod N ) =/= ( ( ( 2nd ` X ) - K ) mod N ) )
29 21 24 27 28 syl3anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( ( ( 2nd ` X ) + K ) mod N ) =/= ( ( ( 2nd ` X ) - K ) mod N ) )
30 29 necomd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( ( ( 2nd ` X ) - K ) mod N ) =/= ( ( ( 2nd ` X ) + K ) mod N ) )
31 30 olcd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( 1 =/= 1 \/ ( ( ( 2nd ` X ) - K ) mod N ) =/= ( ( ( 2nd ` X ) + K ) mod N ) ) )
32 ovex 
 |-  ( ( ( 2nd ` X ) - K ) mod N ) e. _V
33 10 32 opthne 
 |-  ( <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. =/= <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. <-> ( 1 =/= 1 \/ ( ( ( 2nd ` X ) - K ) mod N ) =/= ( ( ( 2nd ` X ) + K ) mod N ) ) )
34 31 33 sylibr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. =/= <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. )
35 13 20 34 3jca 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. =/= <. 0 , ( 2nd ` X ) >. /\ <. 0 , ( 2nd ` X ) >. =/= <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. /\ <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. =/= <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. ) )
36 opex 
 |-  <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. e. _V
37 opex 
 |-  <. 0 , ( 2nd ` X ) >. e. _V
38 opex 
 |-  <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. e. _V
39 hashtpg 
 |-  ( ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. e. _V /\ <. 0 , ( 2nd ` X ) >. e. _V /\ <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. e. _V ) -> ( ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. =/= <. 0 , ( 2nd ` X ) >. /\ <. 0 , ( 2nd ` X ) >. =/= <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. /\ <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. =/= <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. ) <-> ( # ` { <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } ) = 3 ) )
40 36 37 38 39 mp3an 
 |-  ( ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. =/= <. 0 , ( 2nd ` X ) >. /\ <. 0 , ( 2nd ` X ) >. =/= <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. /\ <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. =/= <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. ) <-> ( # ` { <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } ) = 3 )
41 35 40 sylib 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( # ` { <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. , <. 0 , ( 2nd ` X ) >. , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } ) = 3 )
42 6 41 eqtrd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( # ` U ) = 3 )