Metamath Proof Explorer

Theorem clwwlknonel

Description: Characterization of a word over the set of vertices representing a closed walk on vertex X of (nonzero) length N in a graph G . This theorem would not hold for N = 0 if W = X = (/) . (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 28-May-2021) (Revised by AV, 24-Mar-2022)

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

Proof

Step Hyp Ref Expression
1 clwwlknonel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 clwwlknonel.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 isclwwlk ⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
4 simpl ⊢ ( ( ( ♯ ‘ 𝑊 ) = 𝑁 ∧ 𝑊 = ∅ ) → ( ♯ ‘ 𝑊 ) = 𝑁 )
5 fveq2 ⊢ ( 𝑊 = ∅ → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ∅ ) )
6 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
7 5 6 eqtrdi ⊢ ( 𝑊 = ∅ → ( ♯ ‘ 𝑊 ) = 0 )
8 7 adantl ⊢ ( ( ( ♯ ‘ 𝑊 ) = 𝑁 ∧ 𝑊 = ∅ ) → ( ♯ ‘ 𝑊 ) = 0 )
9 4 8 eqtr3d ⊢ ( ( ( ♯ ‘ 𝑊 ) = 𝑁 ∧ 𝑊 = ∅ ) → 𝑁 = 0 )
10 9 ex ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑊 = ∅ → 𝑁 = 0 ) )
11 10 necon3d ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑁 ≠ 0 → 𝑊 ≠ ∅ ) )
12 11 impcom ⊢ ( ( 𝑁 ≠ 0 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → 𝑊 ≠ ∅ )
13 12 biantrud ⊢ ( ( 𝑁 ≠ 0 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( 𝑊 ∈ Word 𝑉 ↔ ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ) )
14 13 bicomd ⊢ ( ( 𝑁 ≠ 0 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ↔ 𝑊 ∈ Word 𝑉 ) )
15 14 3anbi1d ⊢ ( ( 𝑁 ≠ 0 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) )
16 3 15 bitrid ⊢ ( ( 𝑁 ≠ 0 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) )
17 16 a1d ⊢ ( ( 𝑁 ≠ 0 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( ( 𝑊 ‘ 0 ) = 𝑋 → ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) )
18 17 expimpd ⊢ ( 𝑁 ≠ 0 → ( ( ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) )
19 18 pm5.32rd ⊢ ( 𝑁 ≠ 0 → ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ) )
20 isclwwlknon ⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) )
21 isclwwlkn ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
22 21 anbi1i ⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ↔ ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) )
23 anass ⊢ ( ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
24 20 22 23 3bitri ⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
25 3anass ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
26 19 24 25 3bitr4g ⊢ ( 𝑁 ≠ 0 → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )