gpgcubic

Description: Every generalized Petersen graph is acubic graph, i.e., it is a 3-regular graph, i.e., every vertex has degree 3 (see gpgvtxdg3 ), i.e., every vertex has exactly three (different) neighbors. (Contributed by AV, 3-Sep-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	gpgcubic	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to \|U\| = 3$

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		eqid	$⊢ (0 ..^N) = (0 ..^N)$
6	5 1 2 3	gpgvtxel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (X \in V \leftrightarrow \exists x \in \{0, 1\} \exists y \in (0 ..^N) X = ⟨x, y⟩)$
7	6	biimp3a	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to \exists x \in \{0, 1\} \exists y \in (0 ..^N) X = ⟨x, y⟩$
8		elpri	$⊢ x \in \{0, 1\} \to (x = 0 \lor x = 1)$
9		opeq1	$⊢ x = 0 \to ⟨x, y⟩ = ⟨0, y⟩$
10	9	eqeq2d	$⊢ x = 0 \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨0, y⟩)$
11	10	adantr	$⊢ (x = 0 \land (N \in ℤ_{\geq 3} \land K \in J \land X \in V)) \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨0, y⟩)$
12		c0ex	$⊢ 0 \in V$
13		vex	$⊢ y \in V$
14	12 13	op1std	$⊢ X = ⟨0, y⟩ \to 1^{st} (X) = 0$
15	1 2 3 4	gpg3nbgrvtx0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \|U\| = 3$
16	15	exp43	$⊢ N \in ℤ_{\geq 3} \to (K \in J \to (X \in V \to (1^{st} (X) = 0 \to \|U\| = 3)))$
17	16	3imp	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to (1^{st} (X) = 0 \to \|U\| = 3)$
18	14 17	syl5	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to (X = ⟨0, y⟩ \to \|U\| = 3)$
19	18	adantl	$⊢ (x = 0 \land (N \in ℤ_{\geq 3} \land K \in J \land X \in V)) \to (X = ⟨0, y⟩ \to \|U\| = 3)$
20	11 19	sylbid	$⊢ (x = 0 \land (N \in ℤ_{\geq 3} \land K \in J \land X \in V)) \to (X = ⟨x, y⟩ \to \|U\| = 3)$
21	20	ex	$⊢ x = 0 \to ((N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to (X = ⟨x, y⟩ \to \|U\| = 3))$
22		opeq1	$⊢ x = 1 \to ⟨x, y⟩ = ⟨1, y⟩$
23	22	eqeq2d	$⊢ x = 1 \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨1, y⟩)$
24	23	adantr	$⊢ (x = 1 \land (N \in ℤ_{\geq 3} \land K \in J \land X \in V)) \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨1, y⟩)$
25		1ex	$⊢ 1 \in V$
26	25 13	op1std	$⊢ X = ⟨1, y⟩ \to 1^{st} (X) = 1$
27	1 2 3 4	gpg3nbgrvtx1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \|U\| = 3$
28	27	exp43	$⊢ N \in ℤ_{\geq 3} \to (K \in J \to (X \in V \to (1^{st} (X) = 1 \to \|U\| = 3)))$
29	28	3imp	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to (1^{st} (X) = 1 \to \|U\| = 3)$
30	26 29	syl5	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to (X = ⟨1, y⟩ \to \|U\| = 3)$
31	30	adantl	$⊢ (x = 1 \land (N \in ℤ_{\geq 3} \land K \in J \land X \in V)) \to (X = ⟨1, y⟩ \to \|U\| = 3)$
32	24 31	sylbid	$⊢ (x = 1 \land (N \in ℤ_{\geq 3} \land K \in J \land X \in V)) \to (X = ⟨x, y⟩ \to \|U\| = 3)$
33	32	ex	$⊢ x = 1 \to ((N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to (X = ⟨x, y⟩ \to \|U\| = 3))$
34	21 33	jaoi	$⊢ (x = 0 \lor x = 1) \to ((N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to (X = ⟨x, y⟩ \to \|U\| = 3))$
35	8 34	syl	$⊢ x \in \{0, 1\} \to ((N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to (X = ⟨x, y⟩ \to \|U\| = 3))$
36	35	impcom	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in V) \land x \in \{0, 1\}) \to (X = ⟨x, y⟩ \to \|U\| = 3)$
37	36	a1d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in V) \land x \in \{0, 1\}) \to (y \in (0 ..^N) \to (X = ⟨x, y⟩ \to \|U\| = 3))$
38	37	expimpd	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to ((x \in \{0, 1\} \land y \in (0 ..^N)) \to (X = ⟨x, y⟩ \to \|U\| = 3))$
39	38	rexlimdvv	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to (\exists x \in \{0, 1\} \exists y \in (0 ..^N) X = ⟨x, y⟩ \to \|U\| = 3)$
40	7 39	mpd	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in V) \to \|U\| = 3$

Metamath Proof Explorer

Theorem gpgcubic

Proof