Metamath Proof Explorer

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 ⊢ W ∈ N ClWWalksN G ∧ N ∈ ℤ ≥ 3 → W prefix N − 2 ⁡ 0 = W ⁡ 0

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 clwwlknwrd ⊢ W ∈ N ClWWalksN G → W ∈ Word Vtx ⁡ G
3 ige3m2fz ⊢ N ∈ ℤ ≥ 3 → N − 2 ∈ 1 … N
4 3 adantl ⊢ W ∈ N ClWWalksN G ∧ N ∈ ℤ ≥ 3 → N − 2 ∈ 1 … N
5 clwwlknlen ⊢ W ∈ N ClWWalksN G → W = N
6 5 oveq2d ⊢ W ∈ N ClWWalksN G → 1 … W = 1 … N
7 6 eleq2d ⊢ W ∈ N ClWWalksN G → N − 2 ∈ 1 … W ↔ N − 2 ∈ 1 … N
8 7 adantr ⊢ W ∈ N ClWWalksN G ∧ N ∈ ℤ ≥ 3 → N − 2 ∈ 1 … W ↔ N − 2 ∈ 1 … N
9 4 8 mpbird ⊢ W ∈ N ClWWalksN G ∧ N ∈ ℤ ≥ 3 → N − 2 ∈ 1 … W
10 pfxfv0 ⊢ W ∈ Word Vtx ⁡ G ∧ N − 2 ∈ 1 … W → W prefix N − 2 ⁡ 0 = W ⁡ 0
11 2 9 10 syl2an2r ⊢ W ∈ N ClWWalksN G ∧ N ∈ ℤ ≥ 3 → W prefix N − 2 ⁡ 0 = W ⁡ 0