Theorem gpgprismgr4cycllem6

Description: Lemma 6 for gpgprismgr4cycl0 : the cycle <. P , F >. is closed, i.e., the first and the last vertex are identical. (Contributed by AV, 1-Nov-2025)

	Ref	Expression
Hypothesis	gpgprismgr4cycl.p	$$⊢P=⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩$$
Assertion	gpgprismgr4cycllem6	$$⊢P\left(0\right)=P\left(4\right)$$

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	$$⊢P=⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩$$
2		opex	$$⊢⟨0,0⟩\in \mathrm{V}$$
3		df-s5	$$⊢⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩=⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩”⟩\mathrm{++}⟨“⟨0,0⟩”⟩$$
4		s4cli	$$⊢⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩”⟩\in \mathrm{Word}\mathrm{V}$$
5		s4len	$$⊢\left|⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩”⟩\right|=4$$
6		s4fv0	$$⊢⟨0,0⟩\in \mathrm{V}\to ⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩”⟩\left(0\right)=⟨0,0⟩$$
7		0nn0	$$⊢0\in {\mathbb{N}}_0$$
8		4pos	$$⊢0<4$$
9	3 4 5 6 7 8	cats1fv	$$⊢⟨0,0⟩\in \mathrm{V}\to ⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\left(0\right)=⟨0,0⟩$$
10	2 9	ax-mp	$$⊢⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\left(0\right)=⟨0,0⟩$$
11	3 4 5	cats1fvn	$$⊢⟨0,0⟩\in \mathrm{V}\to ⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\left(4\right)=⟨0,0⟩$$
12	2 11	ax-mp	$$⊢⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\left(4\right)=⟨0,0⟩$$
13	10 12	eqtr4i	$$⊢⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\left(0\right)=⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\left(4\right)$$
14	1	fveq1i	$$⊢P\left(0\right)=⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\left(0\right)$$
15	1	fveq1i	$$⊢P\left(4\right)=⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩\left(4\right)$$
16	13 14 15	3eqtr4i	$$⊢P\left(0\right)=P\left(4\right)$$