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		eluz3nn	$$⊢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		0elpr01	$$⊢0\in \left\{0,1\right\}$$
16	15	a1i	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to 0\in \left\{0,1\right\}$$
17		simpl	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to 0\in \left(0..^N\right)$$
18	16 17	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)$$
19		simpr	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to 1\in \left(0..^N\right)$$
20	16 19	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)$$
21		1elpr01	$$⊢1\in \left\{0,1\right\}$$
22	21	a1i	$$⊢\left(0\in \left(0..^N\right)\wedge 1\in \left(0..^N\right)\right)\to 1\in \left\{0,1\right\}$$
23	22 19	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)$$
24	22 17	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)$$
25	18 20 23 24 18	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)$$
26	6 14 25	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)$$
27	3	fveq2i	Could not format ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr 1 ) ) : No typesetting found for |- ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr 1 ) ) with typecode |-
28		1elfzo1ceilhalf1	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \left(1..^⌈\frac{N}{2}⌉\right)$$
29		eqid	$$⊢\left(1..^⌈\frac{N}{2}⌉\right)=\left(1..^⌈\frac{N}{2}⌉\right)$$
30		eqid	$$⊢\left(0..^N\right)=\left(0..^N\right)$$
31	29 30	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 |-
32	4 28 31	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 |-
33	27 32	eqtrid	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \mathrm{Vtx}\left(G\right)=\left\{0,1\right\}\times \left(0..^N\right)$$
34		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)$$
35	33 34	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)$$
36	26 35	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)$$
37	1 36	eqeltrid	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to P\in \mathrm{Word}\mathrm{Vtx}\left(G\right)$$
38		wrdf	$$⊢P\in \mathrm{Word}\mathrm{Vtx}\left(G\right)\to P:\left(0..^\left|P\right|\right)⟶\mathrm{Vtx}\left(G\right)$$
39	37 38	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to P:\left(0..^\left|P\right|\right)⟶\mathrm{Vtx}\left(G\right)$$
40		4z	$$⊢4\in \mathbb{Z}$$
41		fzval3	$$⊢4\in \mathbb{Z}\to \left(0\dots 4\right)=\left(0..^4+1\right)$$
42	40 41	ax-mp	$$⊢\left(0\dots 4\right)=\left(0..^4+1\right)$$
43	2	gpgprismgr4cycllem1	$$⊢\left|F\right|=4$$
44	43	oveq2i	$$⊢\left(0\dots \left|F\right|\right)=\left(0\dots 4\right)$$
45	1	gpgprismgr4cycllem4	$$⊢\left|P\right|=5$$
46		df-5	$$⊢5=4+1$$
47	45 46	eqtri	$$⊢\left|P\right|=4+1$$
48	47	oveq2i	$$⊢\left(0..^\left|P\right|\right)=\left(0..^4+1\right)$$
49	42 44 48	3eqtr4i	$$⊢\left(0\dots \left|F\right|\right)=\left(0..^\left|P\right|\right)$$
50	49	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(0\dots \left|F\right|\right)=\left(0..^\left|P\right|\right)$$
51	50	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)$$
52	39 51	mpbird	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)$$