Metamath Proof Explorer


Theorem gpgprismgr4cycllem5

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

Ref Expression
Hypothesis gpgprismgr4cycl.p P = ⟨“ 0 0 0 1 1 1 1 0 0 0 ”⟩
Assertion gpgprismgr4cycllem5 P Word V

Proof

Step Hyp Ref Expression
1 gpgprismgr4cycl.p 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 P Word V