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	⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
Assertion	gpgprismgr4cycllem6	⊢ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 4 )

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
2		opex	⊢ ⟨ 0 , 0 ⟩ ∈ V
3		df-s5	⊢ ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ = ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ”⟩ ++ ⟨“ ⟨ 0 , 0 ⟩ ”⟩ )
4		s4cli	⊢ ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ”⟩ ∈ Word V
5		s4len	⊢ ( ♯ ‘ ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ”⟩ ) = 4
6		s4fv0	⊢ ( ⟨ 0 , 0 ⟩ ∈ V → ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ”⟩ ‘ 0 ) = ⟨ 0 , 0 ⟩ )
7		0nn0	⊢ 0 ∈ ℕ0
8		4pos	⊢ 0 < 4
9	3 4 5 6 7 8	cats1fv	⊢ ( ⟨ 0 , 0 ⟩ ∈ V → ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 0 ) = ⟨ 0 , 0 ⟩ )
10	2 9	ax-mp	⊢ ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 0 ) = ⟨ 0 , 0 ⟩
11	3 4 5	cats1fvn	⊢ ( ⟨ 0 , 0 ⟩ ∈ V → ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 4 ) = ⟨ 0 , 0 ⟩ )
12	2 11	ax-mp	⊢ ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 4 ) = ⟨ 0 , 0 ⟩
13	10 12	eqtr4i	⊢ ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 0 ) = ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 4 )
14	1	fveq1i	⊢ ( 𝑃 ‘ 0 ) = ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 0 )
15	1	fveq1i	⊢ ( 𝑃 ‘ 4 ) = ( ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ‘ 4 )
16	13 14 15	3eqtr4i	⊢ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 4 )