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=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩$$
	gpgprismgr4cycl.g	No typesetting found for |- G = ( N gPetersenGr 1 ) with typecode |-
Assertion	gpgprismgr4cycllem9	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	$$⊢P=⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩$$
2		gpgprismgr4cycl.f	$$⊢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\}”⟩$$
3		gpgprismgr4cycl.g	Could not format G = ( N gPetersenGr 1 ) : No typesetting found for |- G = ( N gPetersenGr 1 ) with typecode |-
4		eluzge3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
5		lbfzo0	$$⊢0\in \left(0..^N\right)\leftrightarrow N\in \mathbb{N}$$
6	4 5	sylibr	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 0\in \left(0..^N\right)$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8	7	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in {\mathbb{N}}_0$$
9		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{Z}$$
10		uzuzle23	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in {\mathbb{Z}}_{\ge 2}$$
11		eluz2gt1	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1<N$$
12	10 11	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1<N$$
13		elfzo0z	$$⊢1\in \left(0..^N\right)\leftrightarrow \left(1\in {\mathbb{N}}_0\wedge N\in \mathbb{Z}\wedge 1<N\right)$$
14	8 9 12 13	syl3anbrc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \left(0..^N\right)$$
15		c0ex	$$⊢0\in \mathrm{V}$$
16	15	prid1	$$⊢0\in \left\{0,1\right\}$$
17	16	a1i	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to 0\in \left\{0,1\right\}$$
18		simpl	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to 0\in \left(0..^N\right)$$
19	17 18	opelxpd	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to ⟨0,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
20		simpr	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to 1\in \left(0..^N\right)$$
21	17 20	opelxpd	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to ⟨0,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
22		1ex	$$⊢1\in \mathrm{V}$$
23	22	prid2	$$⊢1\in \left\{0,1\right\}$$
24	23	a1i	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to 1\in \left\{0,1\right\}$$
25	24 20	opelxpd	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to ⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
26	24 18	opelxpd	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to ⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
27	19 21 25 26 19	s5cld	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to ⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\in \mathrm{Word}\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
28	6 14 27	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\in \mathrm{Word}\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
29	3	fveq2i	Could not format ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr 1 ) ) : No typesetting found for |- ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr 1 ) ) with typecode |-
30		1elfzo1ceilhalf1	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \left(1..^⌈\frac{N}{2}⌉\right)$$
31		eqid	$$⊢\left(1..^⌈\frac{N}{2}⌉\right)=\left(1..^⌈\frac{N}{2}⌉\right)$$
32		eqid	$$⊢\left(0..^N\right)=\left(0..^N\right)$$
33	31 32	gpgvtx	Could not format ( ( N e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) : No typesetting found for |- ( ( N e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) with typecode |-
34	4 30 33	syl2anc	Could not format ( N e. ( ZZ>= ` 3 ) -> ( Vtx ` ( N gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> ( Vtx ` ( N gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) with typecode |-
35	29 34	eqtrid	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \mathrm{Vtx}\left(G\right)=\left\{0,1\right\}\times \left(0..^N\right)$$
36		wrdeq	$$⊢\mathrm{Vtx}\left(G\right)=\left\{0,1\right\}\times \left(0..^N\right)\to \mathrm{Word}\mathrm{Vtx}\left(G\right)=\mathrm{Word}\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
37	35 36	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \mathrm{Word}\mathrm{Vtx}\left(G\right)=\mathrm{Word}\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
38	28 37	eleqtrrd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\in \mathrm{Word}\mathrm{Vtx}\left(G\right)$$
39	1 38	eqeltrid	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to P\in \mathrm{Word}\mathrm{Vtx}\left(G\right)$$
40		wrdf	$$⊢P\in \mathrm{Word}\mathrm{Vtx}\left(G\right)\to P:\left(0..^\left|P\right|\right)⟶\mathrm{Vtx}\left(G\right)$$
41	39 40	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to P:\left(0..^\left|P\right|\right)⟶\mathrm{Vtx}\left(G\right)$$
42		4z	$$⊢4\in \mathbb{Z}$$
43		fzval3	$$⊢4\in \mathbb{Z}\to \left(0\dots 4\right)=\left(0..^4+1\right)$$
44	42 43	ax-mp	$$⊢\left(0\dots 4\right)=\left(0..^4+1\right)$$
45	2	gpgprismgr4cycllem1	$$⊢\left|F\right|=4$$
46	45	oveq2i	$$⊢\left(0\dots \left|F\right|\right)=\left(0\dots 4\right)$$
47	1	gpgprismgr4cycllem4	$$⊢\left|P\right|=5$$
48		df-5	$$⊢5=4+1$$
49	47 48	eqtri	$$⊢\left|P\right|=4+1$$
50	49	oveq2i	$$⊢\left(0..^\left|P\right|\right)=\left(0..^4+1\right)$$
51	44 46 50	3eqtr4i	$$⊢\left(0\dots \left|F\right|\right)=\left(0..^\left|P\right|\right)$$
52	51	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(0\dots \left|F\right|\right)=\left(0..^\left|P\right|\right)$$
53	52	feq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)\leftrightarrow P:\left(0..^\left|P\right|\right)⟶\mathrm{Vtx}\left(G\right)\right)$$
54	41 53	mpbird	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)$$