Theorem gpg3nbgrvtx1

Description: In a generalized Petersen graph G , every vertex of the second kind has exactly three (different) neighbors. (Contributed by AV, 3-Sep-2025)

	Ref	Expression
Hypotheses	gpgnbgr.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	gpgnbgr.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
	gpgnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	gpgnbgr.u	⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
Assertion	gpg3nbgrvtx1	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ♯ ‘ 𝑈 ) = 3 )

Proof

Step	Hyp	Ref	Expression
1		gpgnbgr.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2		gpgnbgr.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
3		gpgnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4		gpgnbgr.u	⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
5	1 2 3 4	gpgnbgrvtx1	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → 𝑈 = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } )
6	5	fveq2d	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ) )
7		ax-1ne0	⊢ 1 ≠ 0
8	7	a1i	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → 1 ≠ 0 )
9	8	orcd	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( 1 ≠ 0 ∨ ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ≠ ( 2nd ‘ 𝑋 ) ) )
10		1ex	⊢ 1 ∈ V
11		ovex	⊢ ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ∈ V
12	10 11	opthne	⊢ ( ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ↔ ( 1 ≠ 0 ∨ ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ≠ ( 2nd ‘ 𝑋 ) ) )
13	9 12	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ )
14		0ne1	⊢ 0 ≠ 1
15	14	a1i	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → 0 ≠ 1 )
16	15	orcd	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( 0 ≠ 1 ∨ ( 2nd ‘ 𝑋 ) ≠ ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ) )
17		c0ex	⊢ 0 ∈ V
18		fvex	⊢ ( 2nd ‘ 𝑋 ) ∈ V
19	17 18	opthne	⊢ ( ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ↔ ( 0 ≠ 1 ∨ ( 2nd ‘ 𝑋 ) ≠ ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ) )
20	16 19	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ )
21		simpll	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
22	1	eleq2i	⊢ ( 𝐾 ∈ 𝐽 ↔ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
23	22	biimpi	⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
24	23	ad2antlr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
25		eqid	⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
26	25 1 2 3	gpgvtxel2	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) )
27	26	adantrr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) )
28		gpg3nbgrvtxlem	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ∧ ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) )
29	21 24 27 28	syl3anc	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) )
30	29	necomd	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) )
31	30	olcd	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( 1 ≠ 1 ∨ ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ) )
32		ovex	⊢ ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ∈ V
33	10 32	opthne	⊢ ( ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ↔ ( 1 ≠ 1 ∨ ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ) )
34	31 33	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ )
35	13 20 34	3jca	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∧ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ) )
36		opex	⊢ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ V
37		opex	⊢ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ V
38		opex	⊢ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ V
39		hashtpg	⊢ ( ( ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ V ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ V ∧ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ V ) → ( ( ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∧ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ) ↔ ( ♯ ‘ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ) = 3 ) )
40	36 37 38 39	mp3an	⊢ ( ( ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∧ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ) ↔ ( ♯ ‘ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ) = 3 )
41	35 40	sylib	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ♯ ‘ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ) = 3 )
42	6 41	eqtrd	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ♯ ‘ 𝑈 ) = 3 )