Theorem 2wlkdlem1

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

	Ref	Expression
Hypotheses	2wlkd.p	$$⊢P=⟨“ABC”⟩$$
	2wlkd.f	$$⊢F=⟨“JK”⟩$$
Assertion	2wlkdlem1	$$⊢\left|P\right|=\left|F\right|+1$$

Proof

Step	Hyp	Ref	Expression
1		2wlkd.p	$$⊢P=⟨“ABC”⟩$$
2		2wlkd.f	$$⊢F=⟨“JK”⟩$$
3	1	fveq2i	$$⊢\left|P\right|=\left|⟨“ABC”⟩\right|$$
4		s3len	$$⊢\left|⟨“ABC”⟩\right|=3$$
5		df-3	$$⊢3=2+1$$
6	4 5	eqtri	$$⊢\left|⟨“ABC”⟩\right|=2+1$$
7	2	fveq2i	$$⊢\left|F\right|=\left|⟨“JK”⟩\right|$$
8		s2len	$$⊢\left|⟨“JK”⟩\right|=2$$
9	7 8	eqtr2i	$$⊢2=\left|F\right|$$
10	9	oveq1i	$$⊢2+1=\left|F\right|+1$$
11	6 10	eqtri	$$⊢\left|⟨“ABC”⟩\right|=\left|F\right|+1$$
12	3 11	eqtri	$$⊢\left|P\right|=\left|F\right|+1$$