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 eluzge3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 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 c0ex ⊢ 0 ∈ V
16 15 prid1 ⊢ 0 ∈ { 0 , 1 }
17 16 a1i ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → 0 ∈ { 0 , 1 } )
18 simpl ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → 0 ∈ ( 0 ..^ 𝑁 ) )
19 17 18 opelxpd ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 0 , 0 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
20 simpr ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → 1 ∈ ( 0 ..^ 𝑁 ) )
21 17 20 opelxpd ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 0 , 1 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
22 1ex ⊢ 1 ∈ V
23 22 prid2 ⊢ 1 ∈ { 0 , 1 }
24 23 a1i ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → 1 ∈ { 0 , 1 } )
25 24 20 opelxpd ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 1 , 1 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
26 24 18 opelxpd ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → ⟨ 1 , 0 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
27 19 21 25 26 19 s5cld ⊢ ( ( 0 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ( 0 ..^ 𝑁 ) ) → ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ∈ Word ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
28 6 14 27 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ∈ Word ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
29 3 fveq2i ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ( 𝑁 gPetersenGr 1 ) )
30 1elfzo1ceilhalf1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
31 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
32 eqid ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
33 31 32 gpgvtx ⊢ ( ( 𝑁 ∈ ℕ ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( Vtx ‘ ( 𝑁 gPetersenGr 1 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
34 4 30 33 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 1 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
35 29 34 eqtrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( Vtx ‘ 𝐺 ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
36 wrdeq ⊢ ( ( Vtx ‘ 𝐺 ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → Word ( Vtx ‘ 𝐺 ) = Word ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
37 35 36 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → Word ( Vtx ‘ 𝐺 ) = Word ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
38 28 37 eleqtrrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
39 1 38 eqeltrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
40 wrdf ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
41 39 40 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
42 4z ⊢ 4 ∈ ℤ
43 fzval3 ⊢ ( 4 ∈ ℤ → ( 0 ... 4 ) = ( 0 ..^ ( 4 + 1 ) ) )
44 42 43 ax-mp ⊢ ( 0 ... 4 ) = ( 0 ..^ ( 4 + 1 ) )
45 2 gpgprismgr4cycllem1 ⊢ ( ♯ ‘ 𝐹 ) = 4
46 45 oveq2i ⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 4 )
47 1 gpgprismgr4cycllem4 ⊢ ( ♯ ‘ 𝑃 ) = 5
48 df-5 ⊢ 5 = ( 4 + 1 )
49 47 48 eqtri ⊢ ( ♯ ‘ 𝑃 ) = ( 4 + 1 )
50 49 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ..^ ( 4 + 1 ) )
51 44 46 50 3eqtr4i ⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ ( ♯ ‘ 𝑃 ) )
52 51 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
53 52 feq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
54 41 53 mpbird ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )