Metamath Proof Explorer

Theorem gpgvtx0

Description: The vertices of the first kind in a generalized Petersen graph G . (Contributed by AV, 30-Aug-2025)

Ref Expression
Hypotheses gpgvtx0.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgvtx0.g 
|- G = ( N gPetersenGr K )
gpgvtx0.v 
|- V = ( Vtx ` G )
Assertion gpgvtx0 
|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V /\ <. 0 , ( 2nd ` X ) >. e. V /\ <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V ) )

Proof

Step Hyp Ref Expression
1 gpgvtx0.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpgvtx0.g 
 |-  G = ( N gPetersenGr K )
3 gpgvtx0.v 
 |-  V = ( Vtx ` G )
4 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
5 4 1 2 3 gpgvtxel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. V <-> E. x e. { 0 , 1 } E. y e. ( 0 ..^ N ) X = <. x , y >. ) )
6 2 fveq2i 
 |-  ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) )
7 3 6 eqtri 
 |-  V = ( Vtx ` ( N gPetersenGr K ) )
8 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
9 1 4 gpgvtx 
 |-  ( ( N e. NN /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) )
10 8 9 sylan 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) )
11 10 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) )
12 7 11 eqtrid 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> V = ( { 0 , 1 } X. ( 0 ..^ N ) ) )
13 c0ex 
 |-  0 e. _V
14 13 prid1 
 |-  0 e. { 0 , 1 }
15 14 a1i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ y e. ( 0 ..^ N ) ) -> 0 e. { 0 , 1 } )
16 elfzoelz 
 |-  ( y e. ( 0 ..^ N ) -> y e. ZZ )
17 16 peano2zd 
 |-  ( y e. ( 0 ..^ N ) -> ( y + 1 ) e. ZZ )
18 zmodfzo 
 |-  ( ( ( y + 1 ) e. ZZ /\ N e. NN ) -> ( ( y + 1 ) mod N ) e. ( 0 ..^ N ) )
19 17 8 18 syl2anr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ y e. ( 0 ..^ N ) ) -> ( ( y + 1 ) mod N ) e. ( 0 ..^ N ) )
20 15 19 opelxpd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ y e. ( 0 ..^ N ) ) -> <. 0 , ( ( y + 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
21 simpr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ y e. ( 0 ..^ N ) ) -> y e. ( 0 ..^ N ) )
22 15 21 opelxpd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ y e. ( 0 ..^ N ) ) -> <. 0 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
23 1zzd 
 |-  ( y e. ( 0 ..^ N ) -> 1 e. ZZ )
24 16 23 zsubcld 
 |-  ( y e. ( 0 ..^ N ) -> ( y - 1 ) e. ZZ )
25 zmodfzo 
 |-  ( ( ( y - 1 ) e. ZZ /\ N e. NN ) -> ( ( y - 1 ) mod N ) e. ( 0 ..^ N ) )
26 24 8 25 syl2anr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ y e. ( 0 ..^ N ) ) -> ( ( y - 1 ) mod N ) e. ( 0 ..^ N ) )
27 15 26 opelxpd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ y e. ( 0 ..^ N ) ) -> <. 0 , ( ( y - 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
28 20 22 27 3jca 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ y e. ( 0 ..^ N ) ) -> ( <. 0 , ( ( y + 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , ( ( y - 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
29 28 ad2ant2rl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( <. 0 , ( ( y + 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , ( ( y - 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
30 29 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ V = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> ( <. 0 , ( ( y + 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , ( ( y - 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
31 eleq2 
 |-  ( V = ( { 0 , 1 } X. ( 0 ..^ N ) ) -> ( <. 0 , ( ( y + 1 ) mod N ) >. e. V <-> <. 0 , ( ( y + 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
32 eleq2 
 |-  ( V = ( { 0 , 1 } X. ( 0 ..^ N ) ) -> ( <. 0 , y >. e. V <-> <. 0 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
33 eleq2 
 |-  ( V = ( { 0 , 1 } X. ( 0 ..^ N ) ) -> ( <. 0 , ( ( y - 1 ) mod N ) >. e. V <-> <. 0 , ( ( y - 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
34 31 32 33 3anbi123d 
 |-  ( V = ( { 0 , 1 } X. ( 0 ..^ N ) ) -> ( ( <. 0 , ( ( y + 1 ) mod N ) >. e. V /\ <. 0 , y >. e. V /\ <. 0 , ( ( y - 1 ) mod N ) >. e. V ) <-> ( <. 0 , ( ( y + 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , ( ( y - 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) ) )
35 34 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ V = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> ( ( <. 0 , ( ( y + 1 ) mod N ) >. e. V /\ <. 0 , y >. e. V /\ <. 0 , ( ( y - 1 ) mod N ) >. e. V ) <-> ( <. 0 , ( ( y + 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , ( ( y - 1 ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) ) )
36 30 35 mpbird 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ V = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> ( <. 0 , ( ( y + 1 ) mod N ) >. e. V /\ <. 0 , y >. e. V /\ <. 0 , ( ( y - 1 ) mod N ) >. e. V ) )
37 12 36 mpdan 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( <. 0 , ( ( y + 1 ) mod N ) >. e. V /\ <. 0 , y >. e. V /\ <. 0 , ( ( y - 1 ) mod N ) >. e. V ) )
38 vex 
 |-  x e. _V
39 vex 
 |-  y e. _V
40 38 39 op2ndd 
 |-  ( X = <. x , y >. -> ( 2nd ` X ) = y )
41 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) + 1 ) = ( y + 1 ) )
42 41 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) + 1 ) mod N ) = ( ( y + 1 ) mod N ) )
43 42 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. = <. 0 , ( ( y + 1 ) mod N ) >. )
44 43 eleq1d 
 |-  ( ( 2nd ` X ) = y -> ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V <-> <. 0 , ( ( y + 1 ) mod N ) >. e. V ) )
45 opeq2 
 |-  ( ( 2nd ` X ) = y -> <. 0 , ( 2nd ` X ) >. = <. 0 , y >. )
46 45 eleq1d 
 |-  ( ( 2nd ` X ) = y -> ( <. 0 , ( 2nd ` X ) >. e. V <-> <. 0 , y >. e. V ) )
47 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) - 1 ) = ( y - 1 ) )
48 47 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) - 1 ) mod N ) = ( ( y - 1 ) mod N ) )
49 48 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. = <. 0 , ( ( y - 1 ) mod N ) >. )
50 49 eleq1d 
 |-  ( ( 2nd ` X ) = y -> ( <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V <-> <. 0 , ( ( y - 1 ) mod N ) >. e. V ) )
51 44 46 50 3anbi123d 
 |-  ( ( 2nd ` X ) = y -> ( ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V /\ <. 0 , ( 2nd ` X ) >. e. V /\ <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V ) <-> ( <. 0 , ( ( y + 1 ) mod N ) >. e. V /\ <. 0 , y >. e. V /\ <. 0 , ( ( y - 1 ) mod N ) >. e. V ) ) )
52 40 51 syl 
 |-  ( X = <. x , y >. -> ( ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V /\ <. 0 , ( 2nd ` X ) >. e. V /\ <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V ) <-> ( <. 0 , ( ( y + 1 ) mod N ) >. e. V /\ <. 0 , y >. e. V /\ <. 0 , ( ( y - 1 ) mod N ) >. e. V ) ) )
53 37 52 syl5ibrcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( X = <. x , y >. -> ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V /\ <. 0 , ( 2nd ` X ) >. e. V /\ <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V ) ) )
54 53 rexlimdvva 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( E. x e. { 0 , 1 } E. y e. ( 0 ..^ N ) X = <. x , y >. -> ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V /\ <. 0 , ( 2nd ` X ) >. e. V /\ <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V ) ) )
55 5 54 sylbid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. V -> ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V /\ <. 0 , ( 2nd ` X ) >. e. V /\ <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V ) ) )
56 55 imp 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V /\ <. 0 , ( 2nd ` X ) >. e. V /\ <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V ) )