Metamath Proof Explorer

Theorem gpgov

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

Proof

Step Hyp Ref Expression
1 gpgov.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpgov.i 
 |-  I = ( 0 ..^ N )
3 prex 
 |-  { <. ( 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 ) >. } ) } ) >. } e. _V
4 oveq2 
 |-  ( n = N -> ( 0 ..^ n ) = ( 0 ..^ N ) )
5 4 2 eqtr4di 
 |-  ( n = N -> ( 0 ..^ n ) = I )
6 5 xpeq2d 
 |-  ( n = N -> ( { 0 , 1 } X. ( 0 ..^ n ) ) = ( { 0 , 1 } X. I ) )
7 6 opeq2d 
 |-  ( n = N -> <. ( Base ` ndx ) , ( { 0 , 1 } X. ( 0 ..^ n ) ) >. = <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. )
8 7 adantr 
 |-  ( ( n = N /\ k = K ) -> <. ( Base ` ndx ) , ( { 0 , 1 } X. ( 0 ..^ n ) ) >. = <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. )
9 6 pweqd 
 |-  ( n = N -> ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) = ~P ( { 0 , 1 } X. I ) )
10 9 adantr 
 |-  ( ( n = N /\ k = K ) -> ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) = ~P ( { 0 , 1 } X. I ) )
11 5 rexeqdv 
 |-  ( n = N -> ( E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) <-> 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 ) >. } ) ) )
12 11 adantr 
 |-  ( ( n = N /\ k = K ) -> ( E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) <-> 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 ) >. } ) ) )
13 oveq2 
 |-  ( n = N -> ( ( x + 1 ) mod n ) = ( ( x + 1 ) mod N ) )
14 13 opeq2d 
 |-  ( n = N -> <. 0 , ( ( x + 1 ) mod n ) >. = <. 0 , ( ( x + 1 ) mod N ) >. )
15 14 preq2d 
 |-  ( n = N -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } )
16 15 adantr 
 |-  ( ( n = N /\ k = K ) -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } )
17 16 eqeq2d 
 |-  ( ( n = N /\ k = K ) -> ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } <-> e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
18 biidd 
 |-  ( ( n = N /\ k = K ) -> ( e = { <. 0 , x >. , <. 1 , x >. } <-> e = { <. 0 , x >. , <. 1 , x >. } ) )
19 oveq2 
 |-  ( k = K -> ( x + k ) = ( x + K ) )
20 19 adantl 
 |-  ( ( n = N /\ k = K ) -> ( x + k ) = ( x + K ) )
21 simpl 
 |-  ( ( n = N /\ k = K ) -> n = N )
22 20 21 oveq12d 
 |-  ( ( n = N /\ k = K ) -> ( ( x + k ) mod n ) = ( ( x + K ) mod N ) )
23 22 opeq2d 
 |-  ( ( n = N /\ k = K ) -> <. 1 , ( ( x + k ) mod n ) >. = <. 1 , ( ( x + K ) mod N ) >. )
24 23 preq2d 
 |-  ( ( n = N /\ k = K ) -> { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } )
25 24 eqeq2d 
 |-  ( ( n = N /\ k = K ) -> ( e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } <-> e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
26 17 18 25 3orbi123d 
 |-  ( ( n = N /\ k = K ) -> ( ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) <-> ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
27 26 rexbidv 
 |-  ( ( n = N /\ k = K ) -> ( 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. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
28 12 27 bitrd 
 |-  ( ( n = N /\ k = K ) -> ( E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) <-> 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 ) >. } ) ) )
29 10 28 rabeqbidv 
 |-  ( ( n = N /\ k = K ) -> { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( 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 ) >. } ) } )
30 29 reseq2d 
 |-  ( ( n = N /\ k = K ) -> ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( 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 ) >. } ) } ) )
31 30 opeq2d 
 |-  ( ( n = N /\ k = K ) -> <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) } ) >. = <. ( .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 ) >. } ) } ) >. )
32 8 31 preq12d 
 |-  ( ( n = N /\ k = K ) -> { <. ( Base ` ndx ) , ( { 0 , 1 } X. ( 0 ..^ n ) ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( 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 ) >. } ) } ) >. } )
33 fvoveq1 
 |-  ( n = N -> ( |^ ` ( n / 2 ) ) = ( |^ ` ( N / 2 ) ) )
34 33 oveq2d 
 |-  ( n = N -> ( 1 ..^ ( |^ ` ( n / 2 ) ) ) = ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
35 34 1 eqtr4di 
 |-  ( n = N -> ( 1 ..^ ( |^ ` ( n / 2 ) ) ) = J )
36 df-gpg 
 |-  gPetersenGr = ( n e. NN , k e. ( 1 ..^ ( |^ ` ( n / 2 ) ) ) |-> { <. ( Base ` ndx ) , ( { 0 , 1 } X. ( 0 ..^ n ) ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) } ) >. } )
37 32 35 36 ovmpox 
 |-  ( ( N e. NN /\ K e. J /\ { <. ( 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 ) >. } ) } ) >. } e. _V ) -> ( 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 ) >. } ) } ) >. } )
38 3 37 mp3an3 
 |-  ( ( 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 ) >. } ) } ) >. } )