Metamath Proof Explorer

Theorem gpgorder

Description: The order of the generalized Petersen graph GPG(N,K). (Contributed by AV, 29-Sep-2025)

Ref Expression
Hypothesis gpgorder.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
Assertion gpgorder 
|- ( ( N e. NN /\ K e. J ) -> ( # ` ( Vtx ` ( N gPetersenGr K ) ) ) = ( 2 x. N ) )

Proof

Step Hyp Ref Expression
1 gpgorder.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
3 1 2 gpgvtx 
 |-  ( ( N e. NN /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) )
4 3 fveq2d 
 |-  ( ( N e. NN /\ K e. J ) -> ( # ` ( Vtx ` ( N gPetersenGr K ) ) ) = ( # ` ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
5 prfi 
 |-  { 0 , 1 } e. Fin
6 fzofi 
 |-  ( 0 ..^ N ) e. Fin
7 5 6 pm3.2i 
 |-  ( { 0 , 1 } e. Fin /\ ( 0 ..^ N ) e. Fin )
8 hashxp 
 |-  ( ( { 0 , 1 } e. Fin /\ ( 0 ..^ N ) e. Fin ) -> ( # ` ( { 0 , 1 } X. ( 0 ..^ N ) ) ) = ( ( # ` { 0 , 1 } ) x. ( # ` ( 0 ..^ N ) ) ) )
9 7 8 mp1i 
 |-  ( ( N e. NN /\ K e. J ) -> ( # ` ( { 0 , 1 } X. ( 0 ..^ N ) ) ) = ( ( # ` { 0 , 1 } ) x. ( # ` ( 0 ..^ N ) ) ) )
10 prhash2ex 
 |-  ( # ` { 0 , 1 } ) = 2
11 10 a1i 
 |-  ( ( N e. NN /\ K e. J ) -> ( # ` { 0 , 1 } ) = 2 )
12 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
13 hashfzo0 
 |-  ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N )
14 12 13 syl 
 |-  ( N e. NN -> ( # ` ( 0 ..^ N ) ) = N )
15 14 adantr 
 |-  ( ( N e. NN /\ K e. J ) -> ( # ` ( 0 ..^ N ) ) = N )
16 11 15 oveq12d 
 |-  ( ( N e. NN /\ K e. J ) -> ( ( # ` { 0 , 1 } ) x. ( # ` ( 0 ..^ N ) ) ) = ( 2 x. N ) )
17 4 9 16 3eqtrd 
 |-  ( ( N e. NN /\ K e. J ) -> ( # ` ( Vtx ` ( N gPetersenGr K ) ) ) = ( 2 x. N ) )