Theorem 3wlkdlem1

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

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

Proof

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