Metamath Proof Explorer

Theorem gpg5gricstgr3

Description: Each closed neighborhood in a generalized Petersen graph G(N,K) of order 10 ( N = 5 ), which is either the Petersen graph G(5,2) or the 5-prism G(5,1), is isomorphic to a 3-star. (Contributed by AV, 13-Sep-2025)

Ref Expression
Hypothesis gpg5gricstgr3.g ⊢ 𝐺 = ( 5 gPetersenGr 𝐾 )
Assertion gpg5gricstgr3 ( ( 𝐾 ∈ ( 1 ... 2 ) ∧ 𝑉 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑉 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )

Proof

Step Hyp Ref Expression
1 gpg5gricstgr3.g ⊢ 𝐺 = ( 5 gPetersenGr 𝐾 )
2 5eluz3 ⊢ 5 ∈ ( ℤ≥ ‘ 3 )
3 2z ⊢ 2 ∈ ℤ
4 fzval3 ⊢ ( 2 ∈ ℤ → ( 1 ... 2 ) = ( 1 ..^ ( 2 + 1 ) ) )
5 3 4 ax-mp ⊢ ( 1 ... 2 ) = ( 1 ..^ ( 2 + 1 ) )
6 2p1e3 ⊢ ( 2 + 1 ) = 3
7 6 oveq2i ⊢ ( 1 ..^ ( 2 + 1 ) ) = ( 1 ..^ 3 )
8 ceil5half3 ⊢ ( ⌈ ‘ ( 5 / 2 ) ) = 3
9 8 eqcomi ⊢ 3 = ( ⌈ ‘ ( 5 / 2 ) )
10 9 oveq2i ⊢ ( 1 ..^ 3 ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
11 5 7 10 3eqtri ⊢ ( 1 ... 2 ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
12 11 eleq2i ⊢ ( 𝐾 ∈ ( 1 ... 2 ) ↔ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
13 12 biimpi ⊢ ( 𝐾 ∈ ( 1 ... 2 ) → 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
14 gpgusgra ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( 5 gPetersenGr 𝐾 ) ∈ USGraph )
15 1 14 eqeltrid ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → 𝐺 ∈ USGraph )
16 2 13 15 sylancr ⊢ ( 𝐾 ∈ ( 1 ... 2 ) → 𝐺 ∈ USGraph )
17 16 anim1i ⊢ ( ( 𝐾 ∈ ( 1 ... 2 ) ∧ 𝑉 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ ( Vtx ‘ 𝐺 ) ) )
18 eqidd ⊢ ( ( 𝐾 ∈ ( 1 ... 2 ) ∧ 𝑉 ∈ ( Vtx ‘ 𝐺 ) ) → 5 = 5 )
19 13 adantr ⊢ ( ( 𝐾 ∈ ( 1 ... 2 ) ∧ 𝑉 ∈ ( Vtx ‘ 𝐺 ) ) → 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
20 simpr ⊢ ( ( 𝐾 ∈ ( 1 ... 2 ) ∧ 𝑉 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑉 ∈ ( Vtx ‘ 𝐺 ) )
21 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
22 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
23 eqid ⊢ ( 𝐺 NeighbVtx 𝑉 ) = ( 𝐺 NeighbVtx 𝑉 )
24 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
25 21 1 22 23 24 gpg5nbgr3star ⊢ ( ( 5 = 5 ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ∧ 𝑉 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑉 ) ) = 3 ∧ ∀ 𝑥 ∈ ( 𝐺 NeighbVtx 𝑉 ) ∀ 𝑦 ∈ ( 𝐺 NeighbVtx 𝑉 ) { 𝑥 , 𝑦 } ∉ ( Edg ‘ 𝐺 ) ) )
26 18 19 20 25 syl3anc ⊢ ( ( 𝐾 ∈ ( 1 ... 2 ) ∧ 𝑉 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑉 ) ) = 3 ∧ ∀ 𝑥 ∈ ( 𝐺 NeighbVtx 𝑉 ) ∀ 𝑦 ∈ ( 𝐺 NeighbVtx 𝑉 ) { 𝑥 , 𝑦 } ∉ ( Edg ‘ 𝐺 ) ) )
27 eqid ⊢ ( 𝐺 ClNeighbVtx 𝑉 ) = ( 𝐺 ClNeighbVtx 𝑉 )
28 3nn0 ⊢ 3 ∈ ℕ0
29 eqid ⊢ ( StarGr ‘ 3 ) = ( StarGr ‘ 3 )
30 eqid ⊢ ( Vtx ‘ ( StarGr ‘ 3 ) ) = ( Vtx ‘ ( StarGr ‘ 3 ) )
31 22 23 27 28 29 30 24 isubgr3stgr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑉 ) ) = 3 ∧ ∀ 𝑥 ∈ ( 𝐺 NeighbVtx 𝑉 ) ∀ 𝑦 ∈ ( 𝐺 NeighbVtx 𝑉 ) { 𝑥 , 𝑦 } ∉ ( Edg ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑉 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) ) )
32 17 26 31 sylc ⊢ ( ( 𝐾 ∈ ( 1 ... 2 ) ∧ 𝑉 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑉 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )