Theorem 2clwwlklem

Description: Lemma for clwwnonrepclwwnon and extwwlkfab . (Contributed by Alexander van der Vekens, 18-Sep-2018) (Revised by AV, 10-May-2022) (Revised by AV, 30-Oct-2022)

	Ref	Expression
Assertion	2clwwlklem	⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2	1	clwwlknwrd	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
3		ige3m2fz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ( 1 ... 𝑁 ) )
4	3	adantl	⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 − 2 ) ∈ ( 1 ... 𝑁 ) )
5		clwwlknlen	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ♯ ‘ 𝑊 ) = 𝑁 )
6	5	oveq2d	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 1 ... ( ♯ ‘ 𝑊 ) ) = ( 1 ... 𝑁 ) )
7	6	eleq2d	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝑁 − 2 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 − 2 ) ∈ ( 1 ... 𝑁 ) ) )
8	7	adantr	⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑁 − 2 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 − 2 ) ∈ ( 1 ... 𝑁 ) ) )
9	4 8	mpbird	⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 − 2 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
10		pfxfv0	⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 − 2 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
11	2 9 10	syl2an2r	⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )