Metamath Proof Explorer

Theorem 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 ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
gpgnbgr.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
gpgnbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
gpgnbgr.u ⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
Assertion gpgcubic ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ 𝑈 ) = 3 )

Proof

Step Hyp Ref Expression
1 gpgnbgr.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2 gpgnbgr.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
3 gpgnbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4 gpgnbgr.u ⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
5 eqid ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
6 5 1 2 3 gpgvtxel ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) )
7 6 biimp3a ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ )
8 elpri ⊢ ( 𝑥 ∈ { 0 , 1 } → ( 𝑥 = 0 ∨ 𝑥 = 1 ) )
9 opeq1 ⊢ ( 𝑥 = 0 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 0 , 𝑦 ⟩ )
10 9 eqeq2d ⊢ ( 𝑥 = 0 → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 0 , 𝑦 ⟩ ) )
11 10 adantr ⊢ ( ( 𝑥 = 0 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 0 , 𝑦 ⟩ ) )
12 c0ex ⊢ 0 ∈ V
13 vex ⊢ 𝑦 ∈ V
14 12 13 op1std ⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 1st ‘ 𝑋 ) = 0 )
15 1 2 3 4 gpg3nbgrvtx0 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ 𝑈 ) = 3 )
16 15 exp43 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐾 ∈ 𝐽 → ( 𝑋 ∈ 𝑉 → ( ( 1st ‘ 𝑋 ) = 0 → ( ♯ ‘ 𝑈 ) = 3 ) ) ) )
17 16 3imp ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ( 1st ‘ 𝑋 ) = 0 → ( ♯ ‘ 𝑈 ) = 3 ) )
18 14 17 syl5 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) )
19 18 adantl ⊢ ( ( 𝑥 = 0 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) )
20 11 19 sylbid ⊢ ( ( 𝑥 = 0 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) )
21 20 ex ⊢ ( 𝑥 = 0 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) ) )
22 opeq1 ⊢ ( 𝑥 = 1 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 1 , 𝑦 ⟩ )
23 22 eqeq2d ⊢ ( 𝑥 = 1 → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) )
24 23 adantr ⊢ ( ( 𝑥 = 1 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) )
25 1ex ⊢ 1 ∈ V
26 25 13 op1std ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( 1st ‘ 𝑋 ) = 1 )
27 1 2 3 4 gpg3nbgrvtx1 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( ♯ ‘ 𝑈 ) = 3 )
28 27 exp43 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐾 ∈ 𝐽 → ( 𝑋 ∈ 𝑉 → ( ( 1st ‘ 𝑋 ) = 1 → ( ♯ ‘ 𝑈 ) = 3 ) ) ) )
29 28 3imp ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ( 1st ‘ 𝑋 ) = 1 → ( ♯ ‘ 𝑈 ) = 3 ) )
30 26 29 syl5 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) )
31 30 adantl ⊢ ( ( 𝑥 = 1 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) )
32 24 31 sylbid ⊢ ( ( 𝑥 = 1 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) )
33 32 ex ⊢ ( 𝑥 = 1 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) ) )
34 21 33 jaoi ⊢ ( ( 𝑥 = 0 ∨ 𝑥 = 1 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) ) )
35 8 34 syl ⊢ ( 𝑥 ∈ { 0 , 1 } → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) ) )
36 35 impcom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ { 0 , 1 } ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) )
37 36 a1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ { 0 , 1 } ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) ) )
38 37 expimpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) ) )
39 38 rexlimdvv ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ♯ ‘ 𝑈 ) = 3 ) )
40 7 39 mpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ 𝑈 ) = 3 )