Metamath Proof Explorer

Theorem clwwlkn2

Description: A closed walk of length 2 represented as word is a word consisting of 2 symbols representing (not necessarily different) vertices connected by (at least) one edge. (Contributed by Alexander van der Vekens, 19-Sep-2018) (Revised by AV, 25-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4 2 3 isclwwlknx ⊢ ( 2 ∈ ℕ → ( 𝑊 ∈ ( 2 ClWWalksN 𝐺 ) ↔ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 2 ) ) )
5 1 4 ax-mp ⊢ ( 𝑊 ∈ ( 2 ClWWalksN 𝐺 ) ↔ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 2 ) )
6 3anass ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
7 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = 2 → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( 2 − 1 ) )
8 2m1e1 ⊢ ( 2 − 1 ) = 1
9 7 8 eqtrdi ⊢ ( ( ♯ ‘ 𝑊 ) = 2 → ( ( ♯ ‘ 𝑊 ) − 1 ) = 1 )
10 9 oveq2d ⊢ ( ( ♯ ‘ 𝑊 ) = 2 → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 0 ..^ 1 ) )
11 fzo01 ⊢ ( 0 ..^ 1 ) = { 0 }
12 10 11 eqtrdi ⊢ ( ( ♯ ‘ 𝑊 ) = 2 → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = { 0 } )
13 12 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) = 2 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = { 0 } )
14 13 raleqdv ⊢ ( ( ( ♯ ‘ 𝑊 ) = 2 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ { 0 } { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
15 c0ex ⊢ 0 ∈ V
16 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )
17 fv0p1e1 ⊢ ( 𝑖 = 0 → ( 𝑊 ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ 1 ) )
18 16 17 preq12d ⊢ ( 𝑖 = 0 → { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } )
19 18 eleq1d ⊢ ( 𝑖 = 0 → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
20 15 19 ralsn ⊢ ( ∀ 𝑖 ∈ { 0 } { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) )
21 14 20 bitrdi ⊢ ( ( ( ♯ ‘ 𝑊 ) = 2 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
22 prcom ⊢ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } = { ( 𝑊 ‘ 0 ) , ( lastS ‘ 𝑊 ) }
23 lsw ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
24 9 fveq2d ⊢ ( ( ♯ ‘ 𝑊 ) = 2 → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ 1 ) )
25 23 24 sylan9eqr ⊢ ( ( ( ♯ ‘ 𝑊 ) = 2 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ 1 ) )
26 25 preq2d ⊢ ( ( ( ♯ ‘ 𝑊 ) = 2 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → { ( 𝑊 ‘ 0 ) , ( lastS ‘ 𝑊 ) } = { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } )
27 22 26 eqtrid ⊢ ( ( ( ♯ ‘ 𝑊 ) = 2 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } = { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } )
28 27 eleq1d ⊢ ( ( ( ♯ ‘ 𝑊 ) = 2 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
29 21 28 anbi12d ⊢ ( ( ( ♯ ‘ 𝑊 ) = 2 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
30 anidm ⊢ ( ( { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) )
31 29 30 bitrdi ⊢ ( ( ( ♯ ‘ 𝑊 ) = 2 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
32 31 pm5.32da ⊢ ( ( ♯ ‘ 𝑊 ) = 2 → ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ↔ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
33 6 32 syl5bb ⊢ ( ( ♯ ‘ 𝑊 ) = 2 → ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
34 33 pm5.32ri ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 2 ) ↔ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 2 ) )
35 3anass ⊢ ( ( ( ♯ ‘ 𝑊 ) = 2 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( ♯ ‘ 𝑊 ) = 2 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
36 ancom ⊢ ( ( ( ♯ ‘ 𝑊 ) = 2 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ↔ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 2 ) )
37 35 36 bitr2i ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = 2 ) ↔ ( ( ♯ ‘ 𝑊 ) = 2 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
38 5 34 37 3bitri ⊢ ( 𝑊 ∈ ( 2 ClWWalksN 𝐺 ) ↔ ( ( ♯ ‘ 𝑊 ) = 2 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )