Theorem gpgprismgr4cycllem5

Description: Lemma 5 for gpgprismgr4cycl0 . (Contributed by AV, 1-Nov-2025)

	Ref	Expression
Hypothesis	gpgprismgr4cycl.p	⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
Assertion	gpgprismgr4cycllem5	⊢ 𝑃 ∈ Word V

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
2		s5cli	⊢ ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩ ∈ Word V
3	1 2	eqeltri	⊢ 𝑃 ∈ Word V