Theorem 2wlkdlem1

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

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

Proof

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