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 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgnbgr.g 
|- G = ( N gPetersenGr K )
gpgnbgr.v 
|- V = ( Vtx ` G )
gpgnbgr.u 
|- U = ( G NeighbVtx X )
Assertion gpgcubic 
|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( # ` U ) = 3 )

Proof

Step Hyp Ref Expression
1 gpgnbgr.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpgnbgr.g 
 |-  G = ( N gPetersenGr K )
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 e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. V <-> E. x e. { 0 , 1 } E. y e. ( 0 ..^ N ) X = <. x , y >. ) )
7 6 biimp3a 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> E. x e. { 0 , 1 } E. y e. ( 0 ..^ N ) X = <. x , y >. )
8 elpri 
 |-  ( x e. { 0 , 1 } -> ( x = 0 \/ x = 1 ) )
9 opeq1 
 |-  ( x = 0 -> <. x , y >. = <. 0 , y >. )
10 9 eqeq2d 
 |-  ( x = 0 -> ( X = <. x , y >. <-> X = <. 0 , y >. ) )
11 10 adantr 
 |-  ( ( x = 0 /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) ) -> ( X = <. x , y >. <-> X = <. 0 , y >. ) )
12 c0ex 
 |-  0 e. _V
13 vex 
 |-  y e. _V
14 12 13 op1std 
 |-  ( X = <. 0 , y >. -> ( 1st ` X ) = 0 )
15 1 2 3 4 gpg3nbgrvtx0 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( # ` U ) = 3 )
16 15 exp43 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( K e. J -> ( X e. V -> ( ( 1st ` X ) = 0 -> ( # ` U ) = 3 ) ) ) )
17 16 3imp 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( ( 1st ` X ) = 0 -> ( # ` U ) = 3 ) )
18 14 17 syl5 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( X = <. 0 , y >. -> ( # ` U ) = 3 ) )
19 18 adantl 
 |-  ( ( x = 0 /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) ) -> ( X = <. 0 , y >. -> ( # ` U ) = 3 ) )
20 11 19 sylbid 
 |-  ( ( x = 0 /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) ) -> ( X = <. x , y >. -> ( # ` U ) = 3 ) )
21 20 ex 
 |-  ( x = 0 -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( X = <. x , y >. -> ( # ` U ) = 3 ) ) )
22 opeq1 
 |-  ( x = 1 -> <. x , y >. = <. 1 , y >. )
23 22 eqeq2d 
 |-  ( x = 1 -> ( X = <. x , y >. <-> X = <. 1 , y >. ) )
24 23 adantr 
 |-  ( ( x = 1 /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) ) -> ( X = <. x , y >. <-> X = <. 1 , y >. ) )
25 1ex 
 |-  1 e. _V
26 25 13 op1std 
 |-  ( X = <. 1 , y >. -> ( 1st ` X ) = 1 )
27 1 2 3 4 gpg3nbgrvtx1 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( # ` U ) = 3 )
28 27 exp43 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( K e. J -> ( X e. V -> ( ( 1st ` X ) = 1 -> ( # ` U ) = 3 ) ) ) )
29 28 3imp 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( ( 1st ` X ) = 1 -> ( # ` U ) = 3 ) )
30 26 29 syl5 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( X = <. 1 , y >. -> ( # ` U ) = 3 ) )
31 30 adantl 
 |-  ( ( x = 1 /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) ) -> ( X = <. 1 , y >. -> ( # ` U ) = 3 ) )
32 24 31 sylbid 
 |-  ( ( x = 1 /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) ) -> ( X = <. x , y >. -> ( # ` U ) = 3 ) )
33 32 ex 
 |-  ( x = 1 -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( X = <. x , y >. -> ( # ` U ) = 3 ) ) )
34 21 33 jaoi 
 |-  ( ( x = 0 \/ x = 1 ) -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( X = <. x , y >. -> ( # ` U ) = 3 ) ) )
35 8 34 syl 
 |-  ( x e. { 0 , 1 } -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( X = <. x , y >. -> ( # ` U ) = 3 ) ) )
36 35 impcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) /\ x e. { 0 , 1 } ) -> ( X = <. x , y >. -> ( # ` U ) = 3 ) )
37 36 a1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) /\ x e. { 0 , 1 } ) -> ( y e. ( 0 ..^ N ) -> ( X = <. x , y >. -> ( # ` U ) = 3 ) ) )
38 37 expimpd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) -> ( X = <. x , y >. -> ( # ` U ) = 3 ) ) )
39 38 rexlimdvv 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( E. x e. { 0 , 1 } E. y e. ( 0 ..^ N ) X = <. x , y >. -> ( # ` U ) = 3 ) )
40 7 39 mpd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( # ` U ) = 3 )