Metamath Proof Explorer

Theorem gpgvtx0

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