Theorem gpgvtxdg3

Description: Every vertex in a generalized Petersen graph has degree 3. (Contributed by AV, 4-Sep-2025)

	Ref	Expression
Hypotheses	gpgvtxdg3.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	gpgvtxdg3.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
	gpgvtxdg3.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	gpgvtxdg3	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑋 ) = 3 )

Proof

Step	Hyp	Ref	Expression
1		gpgvtxdg3.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2		gpgvtxdg3.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
3		gpgvtxdg3.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4	1	eleq2i	⊢ ( 𝐾 ∈ 𝐽 ↔ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
5	4	biimpi	⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
6	5	anim2i	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) )
7	6	3adant3	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) )
8		gpgusgra	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph )
9	7 8	syl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph )
10	2 9	eqeltrid	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → 𝐺 ∈ USGraph )
11		simp3	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
12	3	hashnbusgrvd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑋 ) )
13	12	eqcomd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑋 ) = ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) )
14	10 11 13	syl2anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑋 ) = ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) )
15		eqid	⊢ ( 𝐺 NeighbVtx 𝑋 ) = ( 𝐺 NeighbVtx 𝑋 )
16	1 2 3 15	gpgcubic	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) = 3 )
17	14 16	eqtrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑋 ) = 3 )