Metamath Proof Explorer

Theorem gpgvtx1

Description: The inside vertices 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 eluz3nn 
 |-  ( 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 1elpr01 
 |-  1 e. { 0 , 1 }
14 13 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> 1 e. { 0 , 1 } )
15 elfzoelz 
 |-  ( y e. ( 0 ..^ N ) -> y e. ZZ )
16 15 adantl 
 |-  ( ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) -> y e. ZZ )
17 16 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> y e. ZZ )
18 elfzoelz 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. ZZ )
19 18 1 eleq2s 
 |-  ( K e. J -> K e. ZZ )
20 19 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> K e. ZZ )
21 20 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> K e. ZZ )
22 17 21 zaddcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( y + K ) e. ZZ )
23 8 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> N e. NN )
24 23 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> N e. NN )
25 zmodfzo 
 |-  ( ( ( y + K ) e. ZZ /\ N e. NN ) -> ( ( y + K ) mod N ) e. ( 0 ..^ N ) )
26 22 24 25 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( ( y + K ) mod N ) e. ( 0 ..^ N ) )
27 14 26 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 ) ) )
28 simprr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> y e. ( 0 ..^ N ) )
29 14 28 opelxpd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> <. 1 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
30 17 21 zsubcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( y - K ) e. ZZ )
31 zmodfzo 
 |-  ( ( ( y - K ) e. ZZ /\ N e. NN ) -> ( ( y - K ) mod N ) e. ( 0 ..^ N ) )
32 30 24 31 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( ( y - K ) mod N ) e. ( 0 ..^ N ) )
33 14 32 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 ) ) )
34 27 29 33 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 ) ) ) )
35 34 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 ) ) ) )
36 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 ) ) ) )
37 eleq2 
 |-  ( V = ( { 0 , 1 } X. ( 0 ..^ N ) ) -> ( <. 1 , y >. e. V <-> <. 1 , y >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
38 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 ) ) ) )
39 36 37 38 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 ) ) ) ) )
40 39 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 ) ) ) ) )
41 35 40 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 ) )
42 12 41 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 ) )
43 vex 
 |-  x e. _V
44 vex 
 |-  y e. _V
45 43 44 op2ndd 
 |-  ( X = <. x , y >. -> ( 2nd ` X ) = y )
46 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) + K ) = ( y + K ) )
47 46 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) + K ) mod N ) = ( ( y + K ) mod N ) )
48 47 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. = <. 1 , ( ( y + K ) mod N ) >. )
49 48 eleq1d 
 |-  ( ( 2nd ` X ) = y -> ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. e. V <-> <. 1 , ( ( y + K ) mod N ) >. e. V ) )
50 opeq2 
 |-  ( ( 2nd ` X ) = y -> <. 1 , ( 2nd ` X ) >. = <. 1 , y >. )
51 50 eleq1d 
 |-  ( ( 2nd ` X ) = y -> ( <. 1 , ( 2nd ` X ) >. e. V <-> <. 1 , y >. e. V ) )
52 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) - K ) = ( y - K ) )
53 52 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) - K ) mod N ) = ( ( y - K ) mod N ) )
54 53 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. = <. 1 , ( ( y - K ) mod N ) >. )
55 54 eleq1d 
 |-  ( ( 2nd ` X ) = y -> ( <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. e. V <-> <. 1 , ( ( y - K ) mod N ) >. e. V ) )
56 49 51 55 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 ) ) )
57 45 56 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 ) ) )
58 42 57 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 ) ) )
59 58 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 ) ) )
60 5 59 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 ) ) )
61 60 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 ) )