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 ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑊 ∈ ( ( 𝑁 − 1 ) WWalksN 𝐺 ) )

Proof

Step Hyp Ref Expression
1 clwwlknnn ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑁 ∈ ℕ )
2 idd ⊢ ( 𝑁 ∈ ℕ → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) )
3 idd ⊢ ( 𝑁 ∈ ℕ → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
4 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
5 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
6 4 5 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
7 6 eqcomd ⊢ ( 𝑁 ∈ ℕ → 𝑁 = ( ( 𝑁 − 1 ) + 1 ) )
8 7 eqeq2d ⊢ ( 𝑁 ∈ ℕ → ( ( ♯ ‘ 𝑊 ) = 𝑁 ↔ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 − 1 ) + 1 ) ) )
9 8 biimpd ⊢ ( 𝑁 ∈ ℕ → ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( ♯ ‘ 𝑊 ) = ( ( 𝑁 − 1 ) + 1 ) ) )
10 2 3 9 3anim123d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 − 1 ) + 1 ) ) ) )
11 10 com12 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( 𝑁 ∈ ℕ → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 − 1 ) + 1 ) ) ) )
12 11 3exp ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑁 ∈ ℕ → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 − 1 ) + 1 ) ) ) ) ) )
13 12 a1dd ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑁 ∈ ℕ → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 − 1 ) + 1 ) ) ) ) ) ) )
14 13 adantr ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑁 ∈ ℕ → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 − 1 ) + 1 ) ) ) ) ) ) )
15 14 3imp1 ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( 𝑁 ∈ ℕ → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 − 1 ) + 1 ) ) ) )
16 15 com12 ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 − 1 ) + 1 ) ) ) )
17 isclwwlkn ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
18 17 a1i ⊢ ( 𝑁 ∈ ℕ → ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) )
19 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
20 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
21 19 20 isclwwlk ⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
22 21 anbi1i ⊢ ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ↔ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
23 18 22 bitrdi ⊢ ( 𝑁 ∈ ℕ → ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) )
24 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
25 19 20 iswwlksnx ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 − 1 ) WWalksN 𝐺 ) ↔ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 − 1 ) + 1 ) ) ) )
26 24 25 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑊 ∈ ( ( 𝑁 − 1 ) WWalksN 𝐺 ) ↔ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 − 1 ) + 1 ) ) ) )
27 16 23 26 3imtr4d ⊢ ( 𝑁 ∈ ℕ → ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑊 ∈ ( ( 𝑁 − 1 ) WWalksN 𝐺 ) ) )
28 1 27 mpcom ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑊 ∈ ( ( 𝑁 − 1 ) WWalksN 𝐺 ) )