Metamath Proof Explorer

Theorem clwwlkn1

Description: A closed walk of length 1 represented as word is a word consisting of 1 symbol representing a vertex connected to itself by (at least) one edge, that is, a loop. (Contributed by AV, 24-Apr-2021) (Revised by AV, 11-Feb-2022)

Ref Expression
Assertion clwwlkn1 ( 𝑊 ∈ ( 1 ClWWalksN 𝐺 ) ↔ ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 1nn ⊢ 1 ∈ ℕ
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4 2 3 isclwwlknx ⊢ ( 1 ∈ ℕ → ( 𝑊 ∈ ( 1 ClWWalksN 𝐺 ) ↔ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) ) )
5 1 4 ax-mp ⊢ ( 𝑊 ∈ ( 1 ClWWalksN 𝐺 ) ↔ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) )
6 3anass ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
7 ral0 ⊢ ∀ 𝑖 ∈ ∅ { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 )
8 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( 1 − 1 ) )
9 1m1e0 ⊢ ( 1 − 1 ) = 0
10 8 9 eqtrdi ⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( ( ♯ ‘ 𝑊 ) − 1 ) = 0 )
11 10 oveq2d ⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 0 ..^ 0 ) )
12 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
13 11 12 eqtrdi ⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ∅ )
14 13 raleqdv ⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ∅ { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
15 14 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ∅ { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
16 7 15 mpbiri ⊢ ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
17 16 biantrurd ⊢ ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
18 lsw1 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ 0 ) )
19 18 ancoms ⊢ ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ 0 ) )
20 19 preq1d ⊢ ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } = { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) } )
21 dfsn2 ⊢ { ( 𝑊 ‘ 0 ) } = { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) }
22 20 21 eqtr4di ⊢ ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } = { ( 𝑊 ‘ 0 ) } )
23 22 eleq1d ⊢ ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
24 17 23 bitr3d ⊢ ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
25 24 pm5.32da ⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ↔ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
26 6 25 bitrid ⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
27 26 pm5.32ri ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) ↔ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) )
28 3anass ⊢ ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
29 ancom ⊢ ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ↔ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) )
30 28 29 bitr2i ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) ↔ ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
31 5 27 30 3bitri ⊢ ( 𝑊 ∈ ( 1 ClWWalksN 𝐺 ) ↔ ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )