Metamath Proof Explorer

Theorem gpgprismgr4cycllem9

Description: Lemma 9 for gpgprismgr4cycl0 . (Contributed by AV, 3-Nov-2025)

Ref Expression
Hypotheses gpgprismgr4cycl.p ⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
gpgprismgr4cycl.f ⊢ 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩
gpgprismgr4cycl.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 1 )
Assertion gpgprismgr4cycllem9 ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 gpgprismgr4cycl.p ⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
2 gpgprismgr4cycl.f ⊢ 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩
3 gpgprismgr4cycl.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 1 )
4 eluz3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
5 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ℕ )
6 4 5 sylibr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 0 ∈ ( 0 ..^ 𝑁 ) )
7 1nn0 ⊢ 1 ∈ ℕ0
8 7 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ℕ0 )
9 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
10 uzuzle23 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
11 eluz2gt1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑁 )
12 10 11 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 < 𝑁 )
13 elfzo0z ⊢ ( 1 ∈ ( 0 ..^ 𝑁 ) ↔ ( 1 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) )
14 8 9 12 13 syl3anbrc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ( 0 ..^ 𝑁 ) )
15 0elpr01 ⊢ 0 ∈ { 0 , 1 }
16 15 a1i ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → 0 ∈ { 0 , 1 } )
17 simpl ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → 0 ∈ ( 0 ..^ 𝑁 ) )
18 16 17 opelxpd ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 0 , 0 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
19 simpr ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → 1 ∈ ( 0 ..^ 𝑁 ) )
20 16 19 opelxpd ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 0 , 1 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
21 1elpr01 ⊢ 1 ∈ { 0 , 1 }
22 21 a1i ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → 1 ∈ { 0 , 1 } )
23 22 19 opelxpd ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 1 , 1 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
24 22 17 opelxpd ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 1 , 0 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
25 18 20 23 24 18 s5cld ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ∈ Word ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
26 6 14 25 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ∈ Word ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
27 3 fveq2i ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ( 𝑁 gPetersenGr 1 ) )
28 1elfzo1ceilhalf1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
29 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
30 eqid ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
31 29 30 gpgvtx ⊢ ( ( 𝑁 ∈ ℕ ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( Vtx ‘ ( 𝑁 gPetersenGr 1 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
32 4 28 31 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 1 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
33 27 32 eqtrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( Vtx ‘ 𝐺 ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
34 wrdeq ⊢ ( ( Vtx ‘ 𝐺 ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → Word ( Vtx ‘ 𝐺 ) = Word ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
35 33 34 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → Word ( Vtx ‘ 𝐺 ) = Word ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
36 26 35 eleqtrrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
37 1 36 eqeltrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
38 wrdf ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
39 37 38 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
40 4z ⊢ 4 ∈ ℤ
41 fzval3 ⊢ ( 4 ∈ ℤ → ( 0 ... 4 ) = ( 0 ..^ ( 4 + 1 ) ) )
42 40 41 ax-mp ⊢ ( 0 ... 4 ) = ( 0 ..^ ( 4 + 1 ) )
43 2 gpgprismgr4cycllem1 ⊢ ( ♯ ‘ 𝐹 ) = 4
44 43 oveq2i ⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 4 )
45 1 gpgprismgr4cycllem4 ⊢ ( ♯ ‘ 𝑃 ) = 5
46 df-5 ⊢ 5 = ( 4 + 1 )
47 45 46 eqtri ⊢ ( ♯ ‘ 𝑃 ) = ( 4 + 1 )
48 47 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ..^ ( 4 + 1 ) )
49 42 44 48 3eqtr4i ⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ ( ♯ ‘ 𝑃 ) )
50 49 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
51 50 feq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
52 39 51 mpbird ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )