Metamath Proof Explorer

Theorem gpgprismgr4cycllem9

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

Ref Expression
Hypotheses gpgprismgr4cycl.p 
|- P = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. ">
gpgprismgr4cycl.f 
|- F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
gpgprismgr4cycl.g 
|- G = ( N gPetersenGr 1 )
Assertion gpgprismgr4cycllem9 
|- ( N e. ( ZZ>= ` 3 ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )

Proof

Step Hyp Ref Expression
1 gpgprismgr4cycl.p 
 |-  P = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. ">
2 gpgprismgr4cycl.f 
 |-  F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
3 gpgprismgr4cycl.g 
 |-  G = ( N gPetersenGr 1 )
4 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
5 lbfzo0 
 |-  ( 0 e. ( 0 ..^ N ) <-> N e. NN )
6 4 5 sylibr 
 |-  ( N e. ( ZZ>= ` 3 ) -> 0 e. ( 0 ..^ N ) )
7 1nn0 
 |-  1 e. NN0
8 7 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. NN0 )
9 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
10 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
11 eluz2gt1 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )
12 10 11 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 < N )
13 elfzo0z 
 |-  ( 1 e. ( 0 ..^ N ) <-> ( 1 e. NN0 /\ N e. ZZ /\ 1 < N ) )
14 8 9 12 13 syl3anbrc 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 0 ..^ N ) )
15 c0ex 
 |-  0 e. _V
16 15 prid1 
 |-  0 e. { 0 , 1 }
17 16 a1i 
 |-  ( ( 0 e. ( 0 ..^ N ) /\ 1 e. ( 0 ..^ N ) ) -> 0 e. { 0 , 1 } )
18 simpl 
 |-  ( ( 0 e. ( 0 ..^ N ) /\ 1 e. ( 0 ..^ N ) ) -> 0 e. ( 0 ..^ N ) )
19 17 18 opelxpd 
 |-  ( ( 0 e. ( 0 ..^ N ) /\ 1 e. ( 0 ..^ N ) ) -> <. 0 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
20 simpr 
 |-  ( ( 0 e. ( 0 ..^ N ) /\ 1 e. ( 0 ..^ N ) ) -> 1 e. ( 0 ..^ N ) )
21 17 20 opelxpd 
 |-  ( ( 0 e. ( 0 ..^ N ) /\ 1 e. ( 0 ..^ N ) ) -> <. 0 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
22 1ex 
 |-  1 e. _V
23 22 prid2 
 |-  1 e. { 0 , 1 }
24 23 a1i 
 |-  ( ( 0 e. ( 0 ..^ N ) /\ 1 e. ( 0 ..^ N ) ) -> 1 e. { 0 , 1 } )
25 24 20 opelxpd 
 |-  ( ( 0 e. ( 0 ..^ N ) /\ 1 e. ( 0 ..^ N ) ) -> <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
26 24 18 opelxpd 
 |-  ( ( 0 e. ( 0 ..^ N ) /\ 1 e. ( 0 ..^ N ) ) -> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
27 19 21 25 26 19 s5cld 
 |-  ( ( 0 e. ( 0 ..^ N ) /\ 1 e. ( 0 ..^ N ) ) -> <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> e. Word ( { 0 , 1 } X. ( 0 ..^ N ) ) )
28 6 14 27 syl2anc 
 |-  ( N e. ( ZZ>= ` 3 ) -> <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> e. Word ( { 0 , 1 } X. ( 0 ..^ N ) ) )
29 3 fveq2i 
 |-  ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr 1 ) )
30 1elfzo1ceilhalf1 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
31 eqid 
 |-  ( 1 ..^ ( |^ ` ( N / 2 ) ) ) = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
32 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
33 31 32 gpgvtx 
 |-  ( ( N e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) )
34 4 30 33 syl2anc 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( Vtx ` ( N gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) )
35 29 34 eqtrid 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( Vtx ` G ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) )
36 wrdeq 
 |-  ( ( Vtx ` G ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) -> Word ( Vtx ` G ) = Word ( { 0 , 1 } X. ( 0 ..^ N ) ) )
37 35 36 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> Word ( Vtx ` G ) = Word ( { 0 , 1 } X. ( 0 ..^ N ) ) )
38 28 37 eleqtrrd 
 |-  ( N e. ( ZZ>= ` 3 ) -> <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> e. Word ( Vtx ` G ) )
39 1 38 eqeltrid 
 |-  ( N e. ( ZZ>= ` 3 ) -> P e. Word ( Vtx ` G ) )
40 wrdf 
 |-  ( P e. Word ( Vtx ` G ) -> P : ( 0 ..^ ( # ` P ) ) --> ( Vtx ` G ) )
41 39 40 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> P : ( 0 ..^ ( # ` P ) ) --> ( Vtx ` G ) )
42 4z 
 |-  4 e. ZZ
43 fzval3 
 |-  ( 4 e. ZZ -> ( 0 ... 4 ) = ( 0 ..^ ( 4 + 1 ) ) )
44 42 43 ax-mp 
 |-  ( 0 ... 4 ) = ( 0 ..^ ( 4 + 1 ) )
45 2 gpgprismgr4cycllem1 
 |-  ( # ` F ) = 4
46 45 oveq2i 
 |-  ( 0 ... ( # ` F ) ) = ( 0 ... 4 )
47 1 gpgprismgr4cycllem4 
 |-  ( # ` P ) = 5
48 df-5 
 |-  5 = ( 4 + 1 )
49 47 48 eqtri 
 |-  ( # ` P ) = ( 4 + 1 )
50 49 oveq2i 
 |-  ( 0 ..^ ( # ` P ) ) = ( 0 ..^ ( 4 + 1 ) )
51 44 46 50 3eqtr4i 
 |-  ( 0 ... ( # ` F ) ) = ( 0 ..^ ( # ` P ) )
52 51 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 0 ... ( # ` F ) ) = ( 0 ..^ ( # ` P ) ) )
53 52 feq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) <-> P : ( 0 ..^ ( # ` P ) ) --> ( Vtx ` G ) ) )
54 41 53 mpbird 
 |-  ( N e. ( ZZ>= ` 3 ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )