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

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$