Theorem gpgorder

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

	Ref	Expression
Hypothesis	gpgorder.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
Assertion	gpgorder	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( ♯ ‘ ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ) = ( 2 · 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		gpgorder.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2		eqid	⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
3	1 2	gpgvtx	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
4	3	fveq2d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( ♯ ‘ ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ) = ( ♯ ‘ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
5		prfi	⊢ { 0 , 1 } ∈ Fin
6		fzofi	⊢ ( 0 ..^ 𝑁 ) ∈ Fin
7	5 6	pm3.2i	⊢ ( { 0 , 1 } ∈ Fin ∧ ( 0 ..^ 𝑁 ) ∈ Fin )
8		hashxp	⊢ ( ( { 0 , 1 } ∈ Fin ∧ ( 0 ..^ 𝑁 ) ∈ Fin ) → ( ♯ ‘ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) = ( ( ♯ ‘ { 0 , 1 } ) · ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ) )
9	7 8	mp1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( ♯ ‘ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) = ( ( ♯ ‘ { 0 , 1 } ) · ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ) )
10		prhash2ex	⊢ ( ♯ ‘ { 0 , 1 } ) = 2
11	10	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( ♯ ‘ { 0 , 1 } ) = 2 )
12		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
13		hashfzo0	⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
14	12 13	syl	⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
15	14	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
16	11 15	oveq12d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( ( ♯ ‘ { 0 , 1 } ) · ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ) = ( 2 · 𝑁 ) )
17	4 9 16	3eqtrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( ♯ ‘ ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ) = ( 2 · 𝑁 ) )