Metamath Proof Explorer

Theorem gpgvtx0

Description: The outside vertices in a generalized Petersen graph G . (Contributed by AV, 30-Aug-2025)

Ref Expression
Hypotheses gpgvtx0.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
gpgvtx0.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
gpgvtx0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion gpgvtx0 ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 gpgvtx0.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2 gpgvtx0.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
3 gpgvtx0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4 eqid ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
5 4 1 2 3 gpgvtxel ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) )
6 2 fveq2i ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) )
7 3 6 eqtri ⊢ 𝑉 = ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) )
8 eluz3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
9 1 4 gpgvtx ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
10 8 9 sylan ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
11 10 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
12 7 11 eqtrid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
13 0elpr01 ⊢ 0 ∈ { 0 , 1 }
14 13 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 0 ∈ { 0 , 1 } )
15 elfzoelz ⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑦 ∈ ℤ )
16 15 peano2zd ⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 + 1 ) ∈ ℤ )
17 zmodfzo ⊢ ( ( ( 𝑦 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑦 + 1 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
18 16 8 17 syl2anr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑦 + 1 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
19 14 18 opelxpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
20 simpr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) )
21 14 20 opelxpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 0 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
22 1zzd ⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 1 ∈ ℤ )
23 15 22 zsubcld ⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 − 1 ) ∈ ℤ )
24 zmodfzo ⊢ ( ( ( 𝑦 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑦 − 1 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
25 23 8 24 syl2anr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑦 − 1 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
26 14 25 opelxpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
27 19 21 26 3jca ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
28 27 ad2ant2rl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
29 28 adantr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
30 eleq2 ⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
31 eleq2 ⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ↔ ⟨ 0 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
32 eleq2 ⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
33 30 31 32 3anbi123d ⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) ) )
34 33 adantl ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) → ( ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) ) )
35 29 34 mpbird ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
36 12 35 mpdan ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
37 vex ⊢ 𝑥 ∈ V
38 vex ⊢ 𝑦 ∈ V
39 37 38 op2ndd ⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑋 ) = 𝑦 )
40 oveq1 ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( 2nd ‘ 𝑋 ) + 1 ) = ( 𝑦 + 1 ) )
41 40 oveq1d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) = ( ( 𝑦 + 1 ) mod 𝑁 ) )
42 41 opeq2d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ )
43 42 eleq1d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
44 opeq2 ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ = ⟨ 0 , 𝑦 ⟩ )
45 44 eleq1d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ↔ ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ) )
46 oveq1 ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( 2nd ‘ 𝑋 ) − 1 ) = ( 𝑦 − 1 ) )
47 46 oveq1d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) = ( ( 𝑦 − 1 ) mod 𝑁 ) )
48 47 opeq2d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ )
49 48 eleq1d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
50 43 45 49 3anbi123d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
51 39 50 syl ⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
52 36 51 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
53 52 rexlimdvva ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
54 5 53 sylbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
55 54 imp ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )