This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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$