Metamath Proof Explorer

Theorem gpgedg

Description: The edges of the generalized Petersen graph GPG(N,K). (Contributed by AV, 26-Aug-2025)

Ref Expression
Hypotheses gpgov.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgov.i 
|- I = ( 0 ..^ N )
Assertion gpgedg 
|- ( ( N e. NN /\ K e. J ) -> ( Edg ` ( N gPetersenGr K ) ) = { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } )

Proof

Step Hyp Ref Expression
1 gpgov.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpgov.i 
 |-  I = ( 0 ..^ N )
3 edgval 
 |-  ( Edg ` ( N gPetersenGr K ) ) = ran ( iEdg ` ( N gPetersenGr K ) )
4 1 2 gpgiedg 
 |-  ( ( N e. NN /\ K e. J ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) )
5 4 rneqd 
 |-  ( ( N e. NN /\ K e. J ) -> ran ( iEdg ` ( N gPetersenGr K ) ) = ran ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) )
6 rnresi 
 |-  ran ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) = { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) }
7 5 6 eqtrdi 
 |-  ( ( N e. NN /\ K e. J ) -> ran ( iEdg ` ( N gPetersenGr K ) ) = { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } )
8 3 7 eqtrid 
 |-  ( ( N e. NN /\ K e. J ) -> ( Edg ` ( N gPetersenGr K ) ) = { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } )