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 
|- G = ( 5 gPetersenGr K )
Assertion gpg5gricstgr3 
|- ( ( K e. ( 1 ... 2 ) /\ V e. ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx V ) ) ~=gr ( StarGr ` 3 ) )

Proof

Step Hyp Ref Expression
1 gpg5gricstgr3.g 
 |-  G = ( 5 gPetersenGr K )
2 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
3 2z 
 |-  2 e. ZZ
4 fzval3 
 |-  ( 2 e. ZZ -> ( 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 
 |-  ( K e. ( 1 ... 2 ) <-> K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
13 12 biimpi 
 |-  ( K e. ( 1 ... 2 ) -> K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
14 gpgusgra 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr K ) e. USGraph )
15 1 14 eqeltrid 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> G e. USGraph )
16 2 13 15 sylancr 
 |-  ( K e. ( 1 ... 2 ) -> G e. USGraph )
17 16 anim1i 
 |-  ( ( K e. ( 1 ... 2 ) /\ V e. ( Vtx ` G ) ) -> ( G e. USGraph /\ V e. ( Vtx ` G ) ) )
18 eqidd 
 |-  ( ( K e. ( 1 ... 2 ) /\ V e. ( Vtx ` G ) ) -> 5 = 5 )
19 13 adantr 
 |-  ( ( K e. ( 1 ... 2 ) /\ V e. ( Vtx ` G ) ) -> K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
20 simpr 
 |-  ( ( K e. ( 1 ... 2 ) /\ V e. ( Vtx ` G ) ) -> V e. ( Vtx ` G ) )
21 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
22 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
23 eqid 
 |-  ( G NeighbVtx V ) = ( G NeighbVtx V )
24 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
25 21 1 22 23 24 gpg5nbgr3star 
 |-  ( ( 5 = 5 /\ K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) /\ V e. ( Vtx ` G ) ) -> ( ( # ` ( G NeighbVtx V ) ) = 3 /\ A. x e. ( G NeighbVtx V ) A. y e. ( G NeighbVtx V ) { x , y } e/ ( Edg ` G ) ) )
26 18 19 20 25 syl3anc 
 |-  ( ( K e. ( 1 ... 2 ) /\ V e. ( Vtx ` G ) ) -> ( ( # ` ( G NeighbVtx V ) ) = 3 /\ A. x e. ( G NeighbVtx V ) A. y e. ( G NeighbVtx V ) { x , y } e/ ( Edg ` G ) ) )
27 eqid 
 |-  ( G ClNeighbVtx V ) = ( G ClNeighbVtx V )
28 3nn0 
 |-  3 e. NN0
29 eqid 
 |-  ( StarGr ` 3 ) = ( StarGr ` 3 )
30 eqid 
 |-  ( Vtx ` ( StarGr ` 3 ) ) = ( Vtx ` ( StarGr ` 3 ) )
31 22 23 27 28 29 30 24 isubgr3stgr 
 |-  ( ( G e. USGraph /\ V e. ( Vtx ` G ) ) -> ( ( ( # ` ( G NeighbVtx V ) ) = 3 /\ A. x e. ( G NeighbVtx V ) A. y e. ( G NeighbVtx V ) { x , y } e/ ( Edg ` G ) ) -> ( G ISubGr ( G ClNeighbVtx V ) ) ~=gr ( StarGr ` 3 ) ) )
32 17 26 31 sylc 
 |-  ( ( K e. ( 1 ... 2 ) /\ V e. ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx V ) ) ~=gr ( StarGr ` 3 ) )