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 e. 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 >. "> e. Word _V
3 1 2 eqeltri 
 |-  P e. Word _V