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 syl5eq ( ( ( ♯ ‘ 𝑊 ) = 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 ‘ 𝐺 ) ) )