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 ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) )

Proof

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