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∈XClWWalksNOn⁡GN∧W⁡N−2=X→WprefixN−2∈XClWWalksNOn⁡GN−2

Proof

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