Metamath Proof Explorer

Theorem gpgvtx1

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

Ref Expression
Hypotheses gpgvtx0.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgvtx0.g 
|- G = ( N gPetersenGr K )
gpgvtx0.v 
|- V = ( Vtx ` G )
Assertion gpgvtx1 
|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. e. V /\ <. 1 , ( 2nd ` X ) >. e. V /\ <. 1 , ( ( ( 2nd ` X ) - K ) 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 1ex 
 |-  1 e. _V
14 13 prid2 
 |-  1 e. { 0 , 1 }
15 14 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> 1 e. { 0 , 1 } )
16 elfzoelz 
 |-  ( y e. ( 0 ..^ N ) -> y e. ZZ )
17 16 adantl 
 |-  ( ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) -> y e. ZZ )
18 17 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> y e. ZZ )
19 elfzoelz 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. ZZ )
20 19 1 eleq2s 
 |-  ( K e. J -> K e. ZZ )
21 20 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> K e. ZZ )
22 21 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> K e. ZZ )
23 18 22 zaddcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( y + K ) e. ZZ )
24 8 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> N e. NN )
25 24 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> N e. NN )
26 zmodfzo 
 |-  ( ( ( y + K ) e. ZZ /\ N e. NN ) -> ( ( y + K ) mod N ) e. ( 0 ..^ N ) )
27 23 25 26 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( ( y + K ) mod N ) e. ( 0 ..^ N ) )
28 15 27 opelxpd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> <. 1 , ( ( y + K ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
29 simprr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> y e. ( 0 ..^ N ) )
30 15 29 opelxpd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> <. 1 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
31 18 22 zsubcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( y - K ) e. ZZ )
32 zmodfzo 
 |-  ( ( ( y - K ) e. ZZ /\ N e. NN ) -> ( ( y - K ) mod N ) e. ( 0 ..^ N ) )
33 31 25 32 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( ( y - K ) mod N ) e. ( 0 ..^ N ) )
34 15 33 opelxpd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> <. 1 , ( ( y - K ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
35 28 30 34 3jca 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( <. 1 , ( ( y + K ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , ( ( y - K ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
36 35 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ V = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> ( <. 1 , ( ( y + K ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , ( ( y - K ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
37 eleq2 
 |-  ( V = ( { 0 , 1 } X. ( 0 ..^ N ) ) -> ( <. 1 , ( ( y + K ) mod N ) >. e. V <-> <. 1 , ( ( y + K ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
38 eleq2 
 |-  ( V = ( { 0 , 1 } X. ( 0 ..^ N ) ) -> ( <. 1 , y >. e. V <-> <. 1 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
39 eleq2 
 |-  ( V = ( { 0 , 1 } X. ( 0 ..^ N ) ) -> ( <. 1 , ( ( y - K ) mod N ) >. e. V <-> <. 1 , ( ( y - K ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
40 37 38 39 3anbi123d 
 |-  ( V = ( { 0 , 1 } X. ( 0 ..^ N ) ) -> ( ( <. 1 , ( ( y + K ) mod N ) >. e. V /\ <. 1 , y >. e. V /\ <. 1 , ( ( y - K ) mod N ) >. e. V ) <-> ( <. 1 , ( ( y + K ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , ( ( y - K ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) ) )
41 40 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ V = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> ( ( <. 1 , ( ( y + K ) mod N ) >. e. V /\ <. 1 , y >. e. V /\ <. 1 , ( ( y - K ) mod N ) >. e. V ) <-> ( <. 1 , ( ( y + K ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , ( ( y - K ) mod N ) >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) ) )
42 36 41 mpbird 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ V = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> ( <. 1 , ( ( y + K ) mod N ) >. e. V /\ <. 1 , y >. e. V /\ <. 1 , ( ( y - K ) mod N ) >. e. V ) )
43 12 42 mpdan 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( <. 1 , ( ( y + K ) mod N ) >. e. V /\ <. 1 , y >. e. V /\ <. 1 , ( ( y - K ) mod N ) >. e. V ) )
44 vex 
 |-  x e. _V
45 vex 
 |-  y e. _V
46 44 45 op2ndd 
 |-  ( X = <. x , y >. -> ( 2nd ` X ) = y )
47 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) + K ) = ( y + K ) )
48 47 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) + K ) mod N ) = ( ( y + K ) mod N ) )
49 48 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. = <. 1 , ( ( y + K ) mod N ) >. )
50 49 eleq1d 
 |-  ( ( 2nd ` X ) = y -> ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. e. V <-> <. 1 , ( ( y + K ) mod N ) >. e. V ) )
51 opeq2 
 |-  ( ( 2nd ` X ) = y -> <. 1 , ( 2nd ` X ) >. = <. 1 , y >. )
52 51 eleq1d 
 |-  ( ( 2nd ` X ) = y -> ( <. 1 , ( 2nd ` X ) >. e. V <-> <. 1 , y >. e. V ) )
53 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) - K ) = ( y - K ) )
54 53 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) - K ) mod N ) = ( ( y - K ) mod N ) )
55 54 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. = <. 1 , ( ( y - K ) mod N ) >. )
56 55 eleq1d 
 |-  ( ( 2nd ` X ) = y -> ( <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. e. V <-> <. 1 , ( ( y - K ) mod N ) >. e. V ) )
57 50 52 56 3anbi123d 
 |-  ( ( 2nd ` X ) = y -> ( ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. e. V /\ <. 1 , ( 2nd ` X ) >. e. V /\ <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. e. V ) <-> ( <. 1 , ( ( y + K ) mod N ) >. e. V /\ <. 1 , y >. e. V /\ <. 1 , ( ( y - K ) mod N ) >. e. V ) ) )
58 46 57 syl 
 |-  ( X = <. x , y >. -> ( ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. e. V /\ <. 1 , ( 2nd ` X ) >. e. V /\ <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. e. V ) <-> ( <. 1 , ( ( y + K ) mod N ) >. e. V /\ <. 1 , y >. e. V /\ <. 1 , ( ( y - K ) mod N ) >. e. V ) ) )
59 43 58 syl5ibrcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( X = <. x , y >. -> ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. e. V /\ <. 1 , ( 2nd ` X ) >. e. V /\ <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. e. V ) ) )
60 59 rexlimdvva 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( E. x e. { 0 , 1 } E. y e. ( 0 ..^ N ) X = <. x , y >. -> ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. e. V /\ <. 1 , ( 2nd ` X ) >. e. V /\ <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. e. V ) ) )
61 5 60 sylbid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. V -> ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. e. V /\ <. 1 , ( 2nd ` X ) >. e. V /\ <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. e. V ) ) )
62 61 imp 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. e. V /\ <. 1 , ( 2nd ` X ) >. e. V /\ <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. e. V ) )