Metamath Proof Explorer

Theorem gpgprismgr4cycllem11

Description: Lemma 11 for gpgprismgr4cycl0 . (Contributed by AV, 5-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 gpgprismgr4cycllem11 
|- ( N e. ( ZZ>= ` 3 ) -> F ( Cycles ` G ) P )

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 1 gpgprismgr4cycllem5 
 |-  P e. Word _V
5 4 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> P e. Word _V )
6 1 gpgprismgr4cycllem4 
 |-  ( # ` P ) = 5
7 6 oveq1i 
 |-  ( ( # ` P ) - 1 ) = ( 5 - 1 )
8 5m1e4 
 |-  ( 5 - 1 ) = 4
9 7 8 eqtri 
 |-  ( ( # ` P ) - 1 ) = 4
10 9 eqcomi 
 |-  4 = ( ( # ` P ) - 1 )
11 1 gpgprismgr4cycllem7 
 |-  ( ( x e. ( 0 ..^ ( # ` P ) ) /\ y e. ( 1 ..^ 4 ) ) -> ( x =/= y -> ( P ` x ) =/= ( P ` y ) ) )
12 11 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( x e. ( 0 ..^ ( # ` P ) ) /\ y e. ( 1 ..^ 4 ) ) ) -> ( x =/= y -> ( P ` x ) =/= ( P ` y ) ) )
13 12 ralrimivva 
 |-  ( N e. ( ZZ>= ` 3 ) -> A. x e. ( 0 ..^ ( # ` P ) ) A. y e. ( 1 ..^ 4 ) ( x =/= y -> ( P ` x ) =/= ( P ` y ) ) )
14 2 gpgprismgr4cycllem1 
 |-  ( # ` F ) = 4
15 1 2 3 gpgprismgr4cycllem8 
 |-  ( N e. ( ZZ>= ` 3 ) -> F e. Word dom ( iEdg ` G ) )
16 1 2 3 gpgprismgr4cycllem9 
 |-  ( N e. ( ZZ>= ` 3 ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
17 1 2 3 gpgprismgr4cycllem10 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ x e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` x ) ) = { ( P ` x ) , ( P ` ( x + 1 ) ) } )
18 17 ralrimiva 
 |-  ( N e. ( ZZ>= ` 3 ) -> A. x e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` x ) ) = { ( P ` x ) , ( P ` ( x + 1 ) ) } )
19 gpgprismgrusgra 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N gPetersenGr 1 ) e. USGraph )
20 3 eleq1i 
 |-  ( G e. USGraph <-> ( N gPetersenGr 1 ) e. USGraph )
21 usgrupgr 
 |-  ( G e. USGraph -> G e. UPGraph )
22 20 21 sylbir 
 |-  ( ( N gPetersenGr 1 ) e. USGraph -> G e. UPGraph )
23 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
24 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
25 23 24 upgriswlk 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. x e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` x ) ) = { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) )
26 19 22 25 3syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. x e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` x ) ) = { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) )
27 15 16 18 26 mpbir3and 
 |-  ( N e. ( ZZ>= ` 3 ) -> F ( Walks ` G ) P )
28 2 gpgprismgr4cycllem2 
 |-  Fun `' F
29 istrl 
 |-  ( F ( Trails ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' F ) )
30 27 28 29 sylanblrc 
 |-  ( N e. ( ZZ>= ` 3 ) -> F ( Trails ` G ) P )
31 5 10 13 14 30 pthd 
 |-  ( N e. ( ZZ>= ` 3 ) -> F ( Paths ` G ) P )
32 1 gpgprismgr4cycllem6 
 |-  ( P ` 0 ) = ( P ` 4 )
33 14 eqcomi 
 |-  4 = ( # ` F )
34 33 fveq2i 
 |-  ( P ` 4 ) = ( P ` ( # ` F ) )
35 32 34 eqtri 
 |-  ( P ` 0 ) = ( P ` ( # ` F ) )
36 iscycl 
 |-  ( F ( Cycles ` G ) P <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
37 31 35 36 sylanblrc 
 |-  ( N e. ( ZZ>= ` 3 ) -> F ( Cycles ` G ) P )