Theorem gpg3nbgrvtx1

Description: In a generalized Petersen graph G , every inside vertex has exactly three (different) neighbors. (Contributed by AV, 3-Sep-2025) (Proof shortened by AV, 22-Nov-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		eqid	⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
23	22 1 2 3	gpgvtxel2	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) )
24	23	adantrr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) )
25		simplr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → 𝐾 ∈ 𝐽 )
26	1 22	modmknepk	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ 𝐽 ) → ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) )
27	21 24 25 26	syl3anc	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) )
28	27	olcd	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( 1 ≠ 1 ∨ ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ) )
29		ovex	⊢ ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ∈ V
30	10 29	opthne	⊢ ( ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ↔ ( 1 ≠ 1 ∨ ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ) )
31	28 30	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ )
32	13 20 31	3jca	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∧ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ) )
33		opex	⊢ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ V
34		opex	⊢ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ V
35		opex	⊢ ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ V
36		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 ) )
37	33 34 35 36	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 )
38	32 37	sylib	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ♯ ‘ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ) = 3 )
39	6 38	eqtrd	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ♯ ‘ 𝑈 ) = 3 )