Theorem 2wlkdlem1

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

	Ref	Expression
Hypotheses	2wlkd.p	⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
	2wlkd.f	⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
Assertion	2wlkdlem1	⊢ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 )

Proof

Step	Hyp	Ref	Expression
1		2wlkd.p	⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2		2wlkd.f	⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
3	1	fveq2i	⊢ ( ♯ ‘ 𝑃 ) = ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
4		s3len	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
5		df-3	⊢ 3 = ( 2 + 1 )
6	4 5	eqtri	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 2 + 1 )
7	2	fveq2i	⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ⟨“ 𝐽 𝐾 ”⟩ )
8		s2len	⊢ ( ♯ ‘ ⟨“ 𝐽 𝐾 ”⟩ ) = 2
9	7 8	eqtr2i	⊢ 2 = ( ♯ ‘ 𝐹 )
10	9	oveq1i	⊢ ( 2 + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 )
11	6 10	eqtri	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( ( ♯ ‘ 𝐹 ) + 1 )
12	3 11	eqtri	⊢ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 )