Metamath Proof Explorer

Theorem clwwlknwwlksn

Description: A word representing a closed walk of length N also represents a walk of length N - 1 . The walk is one edge shorter than the closed walk, because the last edge connecting the last with the first vertex is missing. For example, if <" a b c "> e. ( 3 ClWWalksN G ) represents a closed walk "abca" of length 3, then <" a b c "> e. ( 2 WWalksN G ) represents a walk "abc" (not closed if a =/= c ) of length 2, and <" a b c a "> e. ( 3 WWalksN G ) represents also a closed walk "abca" of length 3. (Contributed by AV, 24-Jan-2022) (Revised by AV, 22-Mar-2022)

Ref Expression
Assertion clwwlknwwlksn ⊢W∈NClWWalksNG→W∈N−1WWalksNG

Proof

Step Hyp Ref Expression
1 clwwlknnn ⊢W∈NClWWalksNG→N∈ℕ
2 idd ⊢N∈ℕ→W∈WordVtx⁡G→W∈WordVtx⁡G
3 idd ⊢N∈ℕ→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G
4 nncn ⊢N∈ℕ→N∈ℂ
5 npcan1 ⊢N∈ℂ→N-1+1=N
6 4 5 syl ⊢N∈ℕ→N-1+1=N
7 6 eqcomd ⊢N∈ℕ→N=N-1+1
8 7 eqeq2d ⊢N∈ℕ→W=N↔W=N-1+1
9 8 biimpd ⊢N∈ℕ→W=N→W=N-1+1
10 2 3 9 3anim123d ⊢N∈ℕ→W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N→W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N-1+1
11 10 com12 ⊢W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N→N∈ℕ→W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N-1+1
12 11 3exp ⊢W∈WordVtx⁡G→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→W=N→N∈ℕ→W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N-1+1
13 12 a1dd ⊢W∈WordVtx⁡G→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→lastS⁡WW⁡0∈Edg⁡G→W=N→N∈ℕ→W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N-1+1
14 13 adantr ⊢W∈WordVtx⁡G∧W≠∅→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→lastS⁡WW⁡0∈Edg⁡G→W=N→N∈ℕ→W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N-1+1
15 14 3imp1 ⊢W∈WordVtx⁡G∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G∧W=N→N∈ℕ→W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N-1+1
16 15 com12 ⊢N∈ℕ→W∈WordVtx⁡G∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G∧W=N→W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N-1+1
17 isclwwlkn ⊢W∈NClWWalksNG↔W∈ClWWalks⁡G∧W=N
18 17 a1i ⊢N∈ℕ→W∈NClWWalksNG↔W∈ClWWalks⁡G∧W=N
19 eqid ⊢Vtx⁡G=Vtx⁡G
20 eqid ⊢Edg⁡G=Edg⁡G
21 19 20 isclwwlk ⊢W∈ClWWalks⁡G↔W∈WordVtx⁡G∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
22 21 anbi1i ⊢W∈ClWWalks⁡G∧W=N↔W∈WordVtx⁡G∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G∧W=N
23 18 22 bitrdi ⊢N∈ℕ→W∈NClWWalksNG↔W∈WordVtx⁡G∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G∧W=N
24 nnm1nn0 ⊢N∈ℕ→N−1∈ℕ0
25 19 20 iswwlksnx ⊢N−1∈ℕ0→W∈N−1WWalksNG↔W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N-1+1
26 24 25 syl ⊢N∈ℕ→W∈N−1WWalksNG↔W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N-1+1
27 16 23 26 3imtr4d ⊢N∈ℕ→W∈NClWWalksNG→W∈N−1WWalksNG
28 1 27 mpcom ⊢W∈NClWWalksNG→W∈N−1WWalksNG