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 
|- ( W e. ( 2 ClWWalksN G ) <-> ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) )

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
4 2 3 isclwwlknx 
 |-  ( 2 e. NN -> ( W e. ( 2 ClWWalksN G ) <-> ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 2 ) ) )
5 1 4 ax-mp 
 |-  ( W e. ( 2 ClWWalksN G ) <-> ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 2 ) )
6 3anass 
 |-  ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( W e. Word ( Vtx ` G ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
7 oveq1 
 |-  ( ( # ` W ) = 2 -> ( ( # ` W ) - 1 ) = ( 2 - 1 ) )
8 2m1e1 
 |-  ( 2 - 1 ) = 1
9 7 8 eqtrdi 
 |-  ( ( # ` W ) = 2 -> ( ( # ` W ) - 1 ) = 1 )
10 9 oveq2d 
 |-  ( ( # ` W ) = 2 -> ( 0 ..^ ( ( # ` W ) - 1 ) ) = ( 0 ..^ 1 ) )
11 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
12 10 11 eqtrdi 
 |-  ( ( # ` W ) = 2 -> ( 0 ..^ ( ( # ` W ) - 1 ) ) = { 0 } )
13 12 adantr 
 |-  ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( 0 ..^ ( ( # ` W ) - 1 ) ) = { 0 } )
14 13 raleqdv 
 |-  ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. { 0 } { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
15 c0ex 
 |-  0 e. _V
16 fveq2 
 |-  ( i = 0 -> ( W ` i ) = ( W ` 0 ) )
17 fv0p1e1 
 |-  ( i = 0 -> ( W ` ( i + 1 ) ) = ( W ` 1 ) )
18 16 17 preq12d 
 |-  ( i = 0 -> { ( W ` i ) , ( W ` ( i + 1 ) ) } = { ( W ` 0 ) , ( W ` 1 ) } )
19 18 eleq1d 
 |-  ( i = 0 -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) )
20 15 19 ralsn 
 |-  ( A. i e. { 0 } { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) )
21 14 20 bitrdi 
 |-  ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) )
22 prcom 
 |-  { ( lastS ` W ) , ( W ` 0 ) } = { ( W ` 0 ) , ( lastS ` W ) }
23 lsw 
 |-  ( W e. Word ( Vtx ` G ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
24 9 fveq2d 
 |-  ( ( # ` W ) = 2 -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` 1 ) )
25 23 24 sylan9eqr 
 |-  ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( lastS ` W ) = ( W ` 1 ) )
26 25 preq2d 
 |-  ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> { ( W ` 0 ) , ( lastS ` W ) } = { ( W ` 0 ) , ( W ` 1 ) } )
27 22 26 syl5eq 
 |-  ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> { ( lastS ` W ) , ( W ` 0 ) } = { ( W ` 0 ) , ( W ` 1 ) } )
28 27 eleq1d 
 |-  ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) )
29 21 28 anbi12d 
 |-  ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) )
30 anidm 
 |-  ( ( { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) )
31 29 30 bitrdi 
 |-  ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) )
32 31 pm5.32da 
 |-  ( ( # ` W ) = 2 -> ( ( W e. Word ( Vtx ` G ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) <-> ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) )
33 6 32 syl5bb 
 |-  ( ( # ` W ) = 2 -> ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) )
34 33 pm5.32ri 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 2 ) <-> ( ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 2 ) )
35 3anass 
 |-  ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) <-> ( ( # ` W ) = 2 /\ ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) )
36 ancom 
 |-  ( ( ( # ` W ) = 2 /\ ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) <-> ( ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 2 ) )
37 35 36 bitr2i 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 2 ) <-> ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) )
38 5 34 37 3bitri 
 |-  ( W e. ( 2 ClWWalksN G ) <-> ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) )