Metamath Proof Explorer

Theorem 3wlkdlem1

Description: Lemma 1 for 3wlkd . (Contributed by AV, 7-Feb-2021)

Ref Expression
Hypotheses 3wlkd.p 
|- P = <" A B C D ">
3wlkd.f 
|- F = <" J K L ">
Assertion 3wlkdlem1 
|- ( # ` P ) = ( ( # ` F ) + 1 )

Proof

Step Hyp Ref Expression
1 3wlkd.p 
 |-  P = <" A B C D ">
2 3wlkd.f 
 |-  F = <" J K L ">
3 1 fveq2i 
 |-  ( # ` P ) = ( # ` <" A B C D "> )
4 s4len 
 |-  ( # ` <" A B C D "> ) = 4
5 df-4 
 |-  4 = ( 3 + 1 )
6 4 5 eqtri 
 |-  ( # ` <" A B C D "> ) = ( 3 + 1 )
7 2 fveq2i 
 |-  ( # ` F ) = ( # ` <" J K L "> )
8 s3len 
 |-  ( # ` <" J K L "> ) = 3
9 7 8 eqtr2i 
 |-  3 = ( # ` F )
10 9 oveq1i 
 |-  ( 3 + 1 ) = ( ( # ` F ) + 1 )
11 6 10 eqtri 
 |-  ( # ` <" A B C D "> ) = ( ( # ` F ) + 1 )
12 3 11 eqtri 
 |-  ( # ` P ) = ( ( # ` F ) + 1 )