Metamath Proof Explorer

Theorem isclwwlknx

Description: Characterization of a word representing a closed walk of a fixed length, definition of ClWWalks expanded. (Contributed by AV, 25-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Hypotheses isclwwlknx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isclwwlknx.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion isclwwlknx ( 𝑁 ∈ ℕ → ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 isclwwlknx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isclwwlknx.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 eleq1 ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ 𝑁 ∈ ℕ ) )
4 len0nnbi ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ≠ ∅ ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
5 4 biimprcd ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( 𝑊 ∈ Word 𝑉 → 𝑊 ≠ ∅ ) )
6 3 5 syl6bir ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑁 ∈ ℕ → ( 𝑊 ∈ Word 𝑉 → 𝑊 ≠ ∅ ) ) )
7 6 impcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( 𝑊 ∈ Word 𝑉 → 𝑊 ≠ ∅ ) )
8 7 imp ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑊 ∈ Word 𝑉 ) → 𝑊 ≠ ∅ )
9 8 biantrurd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑊 ∈ Word 𝑉 ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ↔ ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) )
10 9 bicomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑊 ∈ Word 𝑉 ) → ( ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) )
11 10 pm5.32da ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) )
12 11 ex ⊢ ( 𝑁 ∈ ℕ → ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) ) )
13 12 pm5.32rd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) )
14 isclwwlkn ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
15 1 2 isclwwlk ⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
16 3anass ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) )
17 anass ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) )
18 16 17 bitri ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) )
19 15 18 bitri ⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) )
20 19 anbi1i ⊢ ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
21 14 20 bitri ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
22 3anass ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) )
23 22 anbi1i ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
24 13 21 23 3bitr4g ⊢ ( 𝑁 ∈ ℕ → ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) )