Theorem 3wlkdlem1

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

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

Proof

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