Theorem gpgvtxdg3

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

	Ref	Expression
Hypotheses	gpgvtxdg3.j	|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
	gpgvtxdg3.g	|- G = ( N gPetersenGr K )
	gpgvtxdg3.v	|- V = ( Vtx ` G )
Assertion	gpgvtxdg3	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( ( VtxDeg ` G ) ` X ) = 3 )

Proof

Step	Hyp	Ref	Expression
1		gpgvtxdg3.j	|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2		gpgvtxdg3.g	|- G = ( N gPetersenGr K )
3		gpgvtxdg3.v	|- V = ( Vtx ` G )
4	1	eleq2i	|- ( K e. J <-> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
5	4	biimpi	|- ( K e. J -> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
6	5	anim2i	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) )
7	6	3adant3	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) )
8		gpgusgra	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph )
9	7 8	syl	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( N gPetersenGr K ) e. USGraph )
10	2 9	eqeltrid	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> G e. USGraph )
11		simp3	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> X e. V )
12	3	hashnbusgrvd	|- ( ( G e. USGraph /\ X e. V ) -> ( # ` ( G NeighbVtx X ) ) = ( ( VtxDeg ` G ) ` X ) )
13	12	eqcomd	|- ( ( G e. USGraph /\ X e. V ) -> ( ( VtxDeg ` G ) ` X ) = ( # ` ( G NeighbVtx X ) ) )
14	10 11 13	syl2anc	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( ( VtxDeg ` G ) ` X ) = ( # ` ( G NeighbVtx X ) ) )
15		eqid	|- ( G NeighbVtx X ) = ( G NeighbVtx X )
16	1 2 3 15	gpgcubic	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( # ` ( G NeighbVtx X ) ) = 3 )
17	14 16	eqtrd	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( ( VtxDeg ` G ) ` X ) = 3 )