Metamath Proof Explorer

Theorem clwwlknp

Description: Properties of a set being a closed walk (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 24-Apr-2021) (Proof shortened by AV, 23-Mar-2022)

Ref Expression
Hypotheses isclwwlknx.v ⊢V=Vtx⁡G
isclwwlknx.e ⊢E=Edg⁡G
Assertion clwwlknp ⊢W∈NClWWalksNG→W∈WordV∧W=N∧∀i∈0..^N−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E

Proof

Step Hyp Ref Expression
1 isclwwlknx.v ⊢V=Vtx⁡G
2 isclwwlknx.e ⊢E=Edg⁡G
3 1 clwwlknbp ⊢W∈NClWWalksNG→W∈WordV∧W=N
4 simpr ⊢W∈NClWWalksNG∧W∈WordV∧W=N→W∈WordV∧W=N
5 clwwlknnn ⊢W∈NClWWalksNG→N∈ℕ
6 1 2 isclwwlknx ⊢N∈ℕ→W∈NClWWalksNG↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N
7 3simpc ⊢W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E→∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
8 7 adantr ⊢W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N→∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
9 6 8 syl6bi ⊢N∈ℕ→W∈NClWWalksNG→∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
10 5 9 mpcom ⊢W∈NClWWalksNG→∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
11 10 adantr ⊢W∈NClWWalksNG∧W∈WordV∧W=N→∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
12 oveq1 ⊢W=N→W−1=N−1
13 12 oveq2d ⊢W=N→0..^W−1=0..^N−1
14 13 raleqdv ⊢W=N→∀i∈0..^W−1W⁡iW⁡i+1∈E↔∀i∈0..^N−1W⁡iW⁡i+1∈E
15 14 anbi1d ⊢W=N→∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E↔∀i∈0..^N−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
16 15 ad2antll ⊢W∈NClWWalksNG∧W∈WordV∧W=N→∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E↔∀i∈0..^N−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
17 11 16 mpbid ⊢W∈NClWWalksNG∧W∈WordV∧W=N→∀i∈0..^N−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
18 4 17 jca ⊢W∈NClWWalksNG∧W∈WordV∧W=N→W∈WordV∧W=N∧∀i∈0..^N−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
19 3 18 mpdan ⊢W∈NClWWalksNG→W∈WordV∧W=N∧∀i∈0..^N−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
20 3anass ⊢W∈WordV∧W=N∧∀i∈0..^N−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E↔W∈WordV∧W=N∧∀i∈0..^N−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
21 19 20 sylibr ⊢W∈NClWWalksNG→W∈WordV∧W=N∧∀i∈0..^N−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E