Theorem gpgprismgr4cyclex

Description: The generalized Petersen graphs G(N,1), which are the N-prisms, have (at least) one cycle of length 4. (Contributed by AV, 5-Nov-2025)

	Ref	Expression
Assertion	gpgprismgr4cyclex	Could not format assertion : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> E. p E. f ( f ( Cycles ` ( N gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		s5cli	$$⊢⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\in \mathrm{Word}\mathrm{V}$$
2		s4cli	$$⊢⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\in \mathrm{Word}\mathrm{V}$$
3	1 2	pm3.2i	$$⊢\left(⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\in \mathrm{Word}\mathrm{V}\wedge ⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\in \mathrm{Word}\mathrm{V}\right)$$
4		eqid	$$⊢⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩=⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩$$
5		eqid	$$⊢⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩$$
6		eqid	Could not format ( N gPetersenGr 1 ) = ( N gPetersenGr 1 ) : No typesetting found for |- ( N gPetersenGr 1 ) = ( N gPetersenGr 1 ) with typecode |-
7	4 5 6	gpgprismgr4cycl0	Could not format ( N e. ( ZZ>= ` 3 ) -> ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ( Cycles ` ( N gPetersenGr 1 ) ) <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> /\ ( # ` <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ) = 4 ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ( Cycles ` ( N gPetersenGr 1 ) ) <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> /\ ( # ` <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ) = 4 ) ) with typecode |-
8		breq12	Could not format ( ( f = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> /\ p = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ) -> ( f ( Cycles ` ( N gPetersenGr 1 ) ) p <-> <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ( Cycles ` ( N gPetersenGr 1 ) ) <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ) ) : No typesetting found for |- ( ( f = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> /\ p = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ) -> ( f ( Cycles ` ( N gPetersenGr 1 ) ) p <-> <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ( Cycles ` ( N gPetersenGr 1 ) ) <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ) ) with typecode |-
9	8	ancoms	Could not format ( ( p = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> /\ f = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ) -> ( f ( Cycles ` ( N gPetersenGr 1 ) ) p <-> <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ( Cycles ` ( N gPetersenGr 1 ) ) <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ) ) : No typesetting found for |- ( ( p = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> /\ f = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ) -> ( f ( Cycles ` ( N gPetersenGr 1 ) ) p <-> <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ( Cycles ` ( N gPetersenGr 1 ) ) <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ) ) with typecode |-
10		fveqeq2	$$⊢f=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\to \left(\left|f\right|=4\leftrightarrow \left|⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\right|=4\right)$$
11	10	adantl	$$⊢\left(p=⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\wedge f=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\right)\to \left(\left|f\right|=4\leftrightarrow \left|⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\right|=4\right)$$
12	9 11	anbi12d	Could not format ( ( p = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> /\ f = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ) -> ( ( f ( Cycles ` ( N gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) <-> ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ( Cycles ` ( N gPetersenGr 1 ) ) <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> /\ ( # ` <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ) = 4 ) ) ) : No typesetting found for |- ( ( p = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> /\ f = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ) -> ( ( f ( Cycles ` ( N gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) <-> ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ( Cycles ` ( N gPetersenGr 1 ) ) <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> /\ ( # ` <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ) = 4 ) ) ) with typecode |-
13	12	spc2egv	Could not format ( ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> e. Word _V /\ <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> e. Word _V ) -> ( ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ( Cycles ` ( N gPetersenGr 1 ) ) <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> /\ ( # ` <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ) = 4 ) -> E. p E. f ( f ( Cycles ` ( N gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) ) ) : No typesetting found for |- ( ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> e. Word _V /\ <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> e. Word _V ) -> ( ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ( Cycles ` ( N gPetersenGr 1 ) ) <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> /\ ( # ` <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ) = 4 ) -> E. p E. f ( f ( Cycles ` ( N gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) ) ) with typecode |-
14	3 7 13	mpsyl	Could not format ( N e. ( ZZ>= ` 3 ) -> E. p E. f ( f ( Cycles ` ( N gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> E. p E. f ( f ( Cycles ` ( N gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) ) with typecode |-