Metamath Proof Explorer

Theorem gpgusgra

Description: The generalized Petersen graph GPG(N,K) is a simple graph. (Contributed by AV, 27-Aug-2025)

Ref Expression
Assertion gpgusgra 
|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph )

Proof

Step Hyp Ref Expression
1 f1oi 
 |-  ( _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 ) >. } ) } ) : { 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 ) >. } ) } -1-1-onto-> { 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 ) >. } ) }
2 f1of1 
 |-  ( ( _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 ) >. } ) } ) : { 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 ) >. } ) } -1-1-onto-> { 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. ( 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. ( 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 ) >. } ) } -1-1-> { 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 ) >. } ) } )
3 1 2 mp1i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( _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 ) >. } ) } ) : { 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 ) >. } ) } -1-1-> { 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 ) >. } ) } )
4 eqid 
 |-  ( 1 ..^ ( |^ ` ( N / 2 ) ) ) = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
5 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
6 4 5 gpgusgralem 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> { 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 ) >. } ) } C_ { p e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | ( # ` p ) = 2 } )
7 f1ss 
 |-  ( ( ( _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 ) >. } ) } ) : { 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 ) >. } ) } -1-1-> { 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. ( 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 ) >. } ) } C_ { p e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | ( # ` p ) = 2 } ) -> ( _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 ) >. } ) } ) : { 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 ) >. } ) } -1-1-> { p e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | ( # ` p ) = 2 } )
8 3 6 7 syl2anc 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( _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 ) >. } ) } ) : { 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 ) >. } ) } -1-1-> { p e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | ( # ` p ) = 2 } )
9 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
10 4 5 gpgiedg 
 |-  ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( iEdg ` ( N gPetersenGr 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 ) >. } ) } ) )
11 9 10 sylan 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( iEdg ` ( N gPetersenGr 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 ) >. } ) } ) )
12 11 dmeqd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> dom ( iEdg ` ( N gPetersenGr K ) ) = dom ( _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 ) >. } ) } ) )
13 dmresi 
 |-  dom ( _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 ) >. } ) } ) = { 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 ) >. } ) }
14 12 13 eqtrdi 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> dom ( iEdg ` ( N gPetersenGr 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 ) >. } ) } )
15 4 5 gpgvtx 
 |-  ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) )
16 9 15 sylan 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) )
17 16 pweqd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ~P ( Vtx ` ( N gPetersenGr K ) ) = ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
18 17 rabeqdv 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } = { p e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | ( # ` p ) = 2 } )
19 11 14 18 f1eq123d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( ( iEdg ` ( N gPetersenGr K ) ) : dom ( iEdg ` ( N gPetersenGr K ) ) -1-1-> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } <-> ( _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 ) >. } ) } ) : { 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 ) >. } ) } -1-1-> { p e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | ( # ` p ) = 2 } ) )
20 8 19 mpbird 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( iEdg ` ( N gPetersenGr K ) ) : dom ( iEdg ` ( N gPetersenGr K ) ) -1-1-> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } )
21 ovex 
 |-  ( N gPetersenGr K ) e. _V
22 eqid 
 |-  ( Vtx ` ( N gPetersenGr K ) ) = ( Vtx ` ( N gPetersenGr K ) )
23 eqid 
 |-  ( iEdg ` ( N gPetersenGr K ) ) = ( iEdg ` ( N gPetersenGr K ) )
24 22 23 isusgrs 
 |-  ( ( N gPetersenGr K ) e. _V -> ( ( N gPetersenGr K ) e. USGraph <-> ( iEdg ` ( N gPetersenGr K ) ) : dom ( iEdg ` ( N gPetersenGr K ) ) -1-1-> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } ) )
25 21 24 mp1i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( ( N gPetersenGr K ) e. USGraph <-> ( iEdg ` ( N gPetersenGr K ) ) : dom ( iEdg ` ( N gPetersenGr K ) ) -1-1-> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } ) )
26 20 25 mpbird 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph )