Metamath Proof Explorer

Theorem gpgiedg

Description: The indexed 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 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 ) >. } ) } ) )

Proof

Step Hyp Ref Expression
1 gpgov.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpgov.i 
 |-  I = ( 0 ..^ N )
3 1 2 gpgov 
 |-  ( ( N e. NN /\ K e. J ) -> ( N gPetersenGr K ) = { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _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 ) >. } ) } ) >. } )
4 3 fveq2d 
 |-  ( ( N e. NN /\ K e. J ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( iEdg ` { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _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 prex 
 |-  { 0 , 1 } e. _V
6 2 ovexi 
 |-  I e. _V
7 5 6 xpex 
 |-  ( { 0 , 1 } X. I ) e. _V
8 eqid 
 |-  { 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 ) >. } ) }
9 5 a1i 
 |-  ( I = ( 0 ..^ N ) -> { 0 , 1 } e. _V )
10 ovexd 
 |-  ( I = ( 0 ..^ N ) -> ( 0 ..^ N ) e. _V )
11 2 10 eqeltrid 
 |-  ( I = ( 0 ..^ N ) -> I e. _V )
12 9 11 xpexd 
 |-  ( I = ( 0 ..^ N ) -> ( { 0 , 1 } X. I ) e. _V )
13 12 pwexd 
 |-  ( I = ( 0 ..^ N ) -> ~P ( { 0 , 1 } X. I ) e. _V )
14 8 13 rabexd 
 |-  ( I = ( 0 ..^ 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 ) >. } ) } e. _V )
15 14 resiexd 
 |-  ( I = ( 0 ..^ N ) -> ( _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. _V )
16 2 15 ax-mp 
 |-  ( _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. _V
17 7 16 pm3.2i 
 |-  ( ( { 0 , 1 } X. I ) e. _V /\ ( _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. _V )
18 eqid 
 |-  { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _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 ) >. } ) } ) >. } = { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _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 ) >. } ) } ) >. }
19 18 struct2griedg 
 |-  ( ( ( { 0 , 1 } X. I ) e. _V /\ ( _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. _V ) -> ( iEdg ` { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _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 ) >. } ) } ) >. } ) = ( _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 ) >. } ) } ) )
20 17 19 mp1i 
 |-  ( ( N e. NN /\ K e. J ) -> ( iEdg ` { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _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 ) >. } ) } ) >. } ) = ( _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 ) >. } ) } ) )
21 4 20 eqtrd 
 |-  ( ( 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 ) >. } ) } ) )