Metamath Proof Explorer

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 ` 0 ) = ( P ` 4 )

Proof

Step Hyp Ref Expression
1 gpgprismgr4cycl.p 
 |-  P = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. ">
2 opex 
 |-  <. 0 , 0 >. e. _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 >. "> e. Word _V
5 s4len 
 |-  ( # ` <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ) = 4
6 s4fv0 
 |-  ( <. 0 , 0 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ` 0 ) = <. 0 , 0 >. )
7 0nn0 
 |-  0 e. NN0
8 4pos 
 |-  0 < 4
9 3 4 5 6 7 8 cats1fv 
 |-  ( <. 0 , 0 >. e. _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 >. e. _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 
 |-  ( P ` 0 ) = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 0 )
15 1 fveq1i 
 |-  ( P ` 4 ) = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 4 )
16 13 14 15 3eqtr4i 
 |-  ( P ` 0 ) = ( P ` 4 )