Metamath Proof Explorer

Theorem clwwnonrepclwwnon

Description: If the initial vertex of a closed walk occurs another time in the walk, the walk starts with a closed walk on this vertex. See also the remarks in clwwnrepclwwn . (Contributed by AV, 24-Apr-2022) (Revised by AV, 10-May-2022) (Revised by AV, 30-Oct-2022)

Ref Expression
Assertion clwwnonrepclwwnon ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X → W prefix N − 2 ∈ X ClWWalksNOn ⁡ G N − 2

Proof

Step Hyp Ref Expression
1 simp1 ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X → N ∈ ℤ ≥ 3
2 isclwwlknon ⊢ W ∈ X ClWWalksNOn ⁡ G N ↔ W ∈ N ClWWalksN G ∧ W ⁡ 0 = X
3 2 simplbi ⊢ W ∈ X ClWWalksNOn ⁡ G N → W ∈ N ClWWalksN G
4 3 3ad2ant2 ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X → W ∈ N ClWWalksN G
5 simpr ⊢ W ∈ N ClWWalksN G ∧ W ⁡ 0 = X → W ⁡ 0 = X
6 5 eqcomd ⊢ W ∈ N ClWWalksN G ∧ W ⁡ 0 = X → X = W ⁡ 0
7 2 6 sylbi ⊢ W ∈ X ClWWalksNOn ⁡ G N → X = W ⁡ 0
8 7 eqeq2d ⊢ W ∈ X ClWWalksNOn ⁡ G N → W ⁡ N − 2 = X ↔ W ⁡ N − 2 = W ⁡ 0
9 8 biimpa ⊢ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X → W ⁡ N − 2 = W ⁡ 0
10 9 3adant1 ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X → W ⁡ N − 2 = W ⁡ 0
11 clwwnrepclwwn ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ N ClWWalksN G ∧ W ⁡ N − 2 = W ⁡ 0 → W prefix N − 2 ∈ N − 2 ClWWalksN G
12 1 4 10 11 syl3anc ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X → W prefix N − 2 ∈ N − 2 ClWWalksN G
13 2clwwlklem ⊢ W ∈ N ClWWalksN G ∧ N ∈ ℤ ≥ 3 → W prefix N − 2 ⁡ 0 = W ⁡ 0
14 3 13 sylan ⊢ W ∈ X ClWWalksNOn ⁡ G N ∧ N ∈ ℤ ≥ 3 → W prefix N − 2 ⁡ 0 = W ⁡ 0
15 14 ancoms ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ X ClWWalksNOn ⁡ G N → W prefix N − 2 ⁡ 0 = W ⁡ 0
16 15 3adant3 ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X → W prefix N − 2 ⁡ 0 = W ⁡ 0
17 2 simprbi ⊢ W ∈ X ClWWalksNOn ⁡ G N → W ⁡ 0 = X
18 17 3ad2ant2 ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X → W ⁡ 0 = X
19 16 18 eqtrd ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X → W prefix N − 2 ⁡ 0 = X
20 isclwwlknon ⊢ W prefix N − 2 ∈ X ClWWalksNOn ⁡ G N − 2 ↔ W prefix N − 2 ∈ N − 2 ClWWalksN G ∧ W prefix N − 2 ⁡ 0 = X
21 12 19 20 sylanbrc ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X → W prefix N − 2 ∈ X ClWWalksNOn ⁡ G N − 2