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 eluzge3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 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 c0ex ⊢ 0 ∈ V
14 13 prid1 ⊢ 0 ∈ { 0 , 1 }
15 14 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 0 ∈ { 0 , 1 } )
16 elfzoelz ⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑦 ∈ ℤ )
17 16 peano2zd ⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 + 1 ) ∈ ℤ )
18 zmodfzo ⊢ ( ( ( 𝑦 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑦 + 1 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
19 17 8 18 syl2anr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑦 + 1 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
20 15 19 opelxpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
21 simpr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) )
22 15 21 opelxpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 0 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
23 1zzd ⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 1 ∈ ℤ )
24 16 23 zsubcld ⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 − 1 ) ∈ ℤ )
25 zmodfzo ⊢ ( ( ( 𝑦 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑦 − 1 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
26 24 8 25 syl2anr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑦 − 1 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
27 15 26 opelxpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
28 20 22 27 3jca ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
29 28 ad2ant2rl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
30 29 adantr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
31 eleq2 ⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
32 eleq2 ⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ↔ ⟨ 0 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
33 eleq2 ⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
34 31 32 33 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 ..^ 𝑁 ) ) ) ) )
35 34 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 ..^ 𝑁 ) ) ) ) )
36 30 35 mpbird ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
37 12 36 mpdan ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
38 vex ⊢ 𝑥 ∈ V
39 vex ⊢ 𝑦 ∈ V
40 38 39 op2ndd ⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑋 ) = 𝑦 )
41 oveq1 ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( 2nd ‘ 𝑋 ) + 1 ) = ( 𝑦 + 1 ) )
42 41 oveq1d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) = ( ( 𝑦 + 1 ) mod 𝑁 ) )
43 42 opeq2d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ )
44 43 eleq1d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
45 opeq2 ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ = ⟨ 0 , 𝑦 ⟩ )
46 45 eleq1d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ↔ ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ) )
47 oveq1 ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( 2nd ‘ 𝑋 ) − 1 ) = ( 𝑦 − 1 ) )
48 47 oveq1d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) = ( ( 𝑦 − 1 ) mod 𝑁 ) )
49 48 opeq2d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ )
50 49 eleq1d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
51 44 46 50 3anbi123d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
52 40 51 syl ⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
53 37 52 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
54 53 rexlimdvva ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
55 5 54 sylbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
56 55 imp ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )