gpgnbgrvtx0

Description: The (open) neighborhood of a vertex of the first kind in a generalized Petersen graph G . (Contributed by AV, 28-Aug-2025)

	Ref	Expression
Hypotheses	gpgnbgr.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
	gpgnbgr.g	No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
	gpgnbgr.v	$⊢ V = Vtx (G)$
	gpgnbgr.u	$⊢ U = G NeighbVtx X$
Assertion	gpgnbgrvtx0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to U = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}$

Proof

Step	Hyp	Ref	Expression
1		gpgnbgr.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
2		gpgnbgr.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
3		gpgnbgr.v	$⊢ V = Vtx (G)$
4		gpgnbgr.u	$⊢ U = G NeighbVtx X$
5	4	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to U = G NeighbVtx X$
6	1	eleq2i	$⊢ K \in J \leftrightarrow K \in (1 ..^⌈\frac{N}{2}⌉)$
7		gpgusgra	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( \|^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) : No typesetting found for \|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( \|^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) with typecode \|-
8	6 7	sylan2b	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( N gPetersenGr K ) e. USGraph ) : No typesetting found for \|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( N gPetersenGr K ) e. USGraph ) with typecode \|-
9	2 8	eqeltrid	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to G \in USGraph$
10		simpl	$⊢ (X \in V \land 1^{st} (X) = 0) \to X \in V$
11		eqid	$⊢ Edg (G) = Edg (G)$
12	3 11	nbusgrvtx	$⊢ (G \in USGraph \land X \in V) \to G NeighbVtx X = \{y \in V \| \{X, y\} \in Edg (G)\}$
13	9 10 12	syl2an	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to G NeighbVtx X = \{y \in V \| \{X, y\} \in Edg (G)\}$
14		simpl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (N \in ℤ_{\geq 3} \land K \in J)$
15		simpr	$⊢ (X \in V \land 1^{st} (X) = 0) \to 1^{st} (X) = 0$
16	15	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 1^{st} (X) = 0$
17		simpr	$⊢ (v \in V \land \{X, v\} \in Edg (G)) \to \{X, v\} \in Edg (G)$
18	1 2 3 11	gpgvtxedg0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land \{X, v\} \in Edg (G)) \to (v = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor v = ⟨1, 2^{nd} (X)⟩ \lor v = ⟨0, (2^{nd} (X) - 1) \mod N⟩)$
19	14 16 17 18	syl2an3an	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \land (v \in V \land \{X, v\} \in Edg (G))) \to (v = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor v = ⟨1, 2^{nd} (X)⟩ \lor v = ⟨0, (2^{nd} (X) - 1) \mod N⟩)$
20	19	ex	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ((v \in V \land \{X, v\} \in Edg (G)) \to (v = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor v = ⟨1, 2^{nd} (X)⟩ \lor v = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
21	1 2 3	gpgvtx0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to (⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \land ⟨0, 2^{nd} (X)⟩ \in V \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V)$
22	21	simp1d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to ⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V$
23	22	adantrr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V$
24	1 2 3 11	gpgedgvtx0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in Edg (G) \land \{X, ⟨1, 2^{nd} (X)⟩\} \in Edg (G) \land \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in Edg (G))$
25	24	simp1d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in Edg (G)$
26	23 25	jca	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \land \{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in Edg (G))$
27		eleq1	$⊢ v = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to (v \in V \leftrightarrow ⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V)$
28		preq2	$⊢ v = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to \{X, v\} = \{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\}$
29	28	eleq1d	$⊢ v = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to (\{X, v\} \in Edg (G) \leftrightarrow \{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in Edg (G))$
30	27 29	anbi12d	$⊢ v = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to ((v \in V \land \{X, v\} \in Edg (G)) \leftrightarrow (⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \land \{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in Edg (G)))$
31	26 30	syl5ibrcom	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (v = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to (v \in V \land \{X, v\} \in Edg (G)))$
32	1 2 3	gpgvtx1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to (⟨1, (2^{nd} (X) + K) \mod N⟩ \in V \land ⟨1, 2^{nd} (X)⟩ \in V \land ⟨1, (2^{nd} (X) - K) \mod N⟩ \in V)$
33	32	simp2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to ⟨1, 2^{nd} (X)⟩ \in V$
34	33	adantrr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ⟨1, 2^{nd} (X)⟩ \in V$
35	24	simp2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \{X, ⟨1, 2^{nd} (X)⟩\} \in Edg (G)$
36	34 35	jca	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (⟨1, 2^{nd} (X)⟩ \in V \land \{X, ⟨1, 2^{nd} (X)⟩\} \in Edg (G))$
37		eleq1	$⊢ v = ⟨1, 2^{nd} (X)⟩ \to (v \in V \leftrightarrow ⟨1, 2^{nd} (X)⟩ \in V)$
38		preq2	$⊢ v = ⟨1, 2^{nd} (X)⟩ \to \{X, v\} = \{X, ⟨1, 2^{nd} (X)⟩\}$
39	38	eleq1d	$⊢ v = ⟨1, 2^{nd} (X)⟩ \to (\{X, v\} \in Edg (G) \leftrightarrow \{X, ⟨1, 2^{nd} (X)⟩\} \in Edg (G))$
40	37 39	anbi12d	$⊢ v = ⟨1, 2^{nd} (X)⟩ \to ((v \in V \land \{X, v\} \in Edg (G)) \leftrightarrow (⟨1, 2^{nd} (X)⟩ \in V \land \{X, ⟨1, 2^{nd} (X)⟩\} \in Edg (G)))$
41	36 40	syl5ibrcom	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (v = ⟨1, 2^{nd} (X)⟩ \to (v \in V \land \{X, v\} \in Edg (G)))$
42	21	simp3d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V$
43	42	adantrr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V$
44	43	adantr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \land v = ⟨0, (2^{nd} (X) - 1) \mod N⟩) \to ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V$
45		eleq1	$⊢ v = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to (v \in V \leftrightarrow ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V)$
46	45	adantl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \land v = ⟨0, (2^{nd} (X) - 1) \mod N⟩) \to (v \in V \leftrightarrow ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V)$
47	44 46	mpbird	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \land v = ⟨0, (2^{nd} (X) - 1) \mod N⟩) \to v \in V$
48	24	simp3d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in Edg (G)$
49	48	adantr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \land v = ⟨0, (2^{nd} (X) - 1) \mod N⟩) \to \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in Edg (G)$
50		preq2	$⊢ v = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to \{X, v\} = \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}$
51	50	eleq1d	$⊢ v = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to (\{X, v\} \in Edg (G) \leftrightarrow \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in Edg (G))$
52	51	adantl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \land v = ⟨0, (2^{nd} (X) - 1) \mod N⟩) \to (\{X, v\} \in Edg (G) \leftrightarrow \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in Edg (G))$
53	49 52	mpbird	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \land v = ⟨0, (2^{nd} (X) - 1) \mod N⟩) \to \{X, v\} \in Edg (G)$
54	47 53	jca	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \land v = ⟨0, (2^{nd} (X) - 1) \mod N⟩) \to (v \in V \land \{X, v\} \in Edg (G))$
55	54	ex	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (v = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to (v \in V \land \{X, v\} \in Edg (G)))$
56	31 41 55	3jaod	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ((v = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor v = ⟨1, 2^{nd} (X)⟩ \lor v = ⟨0, (2^{nd} (X) - 1) \mod N⟩) \to (v \in V \land \{X, v\} \in Edg (G)))$
57	20 56	impbid	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ((v \in V \land \{X, v\} \in Edg (G)) \leftrightarrow (v = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor v = ⟨1, 2^{nd} (X)⟩ \lor v = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
58		preq2	$⊢ y = v \to \{X, y\} = \{X, v\}$
59	58	eleq1d	$⊢ y = v \to (\{X, y\} \in Edg (G) \leftrightarrow \{X, v\} \in Edg (G))$
60	59	elrab	$⊢ v \in \{y \in V \| \{X, y\} \in Edg (G)\} \leftrightarrow (v \in V \land \{X, v\} \in Edg (G))$
61		vex	$⊢ v \in V$
62	61	eltp	$⊢ v \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \leftrightarrow (v = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor v = ⟨1, 2^{nd} (X)⟩ \lor v = ⟨0, (2^{nd} (X) - 1) \mod N⟩)$
63	57 60 62	3bitr4g	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (v \in \{y \in V \| \{X, y\} \in Edg (G)\} \leftrightarrow v \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\})$
64	63	eqrdv	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \{y \in V \| \{X, y\} \in Edg (G)\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}$
65	5 13 64	3eqtrd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to U = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}$

Metamath Proof Explorer

Theorem gpgnbgrvtx0

Proof