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

Proof

Step Hyp Ref Expression
1 1nn 
 |-  1 e. NN
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
4 2 3 isclwwlknx 
 |-  ( 1 e. NN -> ( W e. ( 1 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 ) = 1 ) ) )
5 1 4 ax-mp 
 |-  ( W e. ( 1 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 ) = 1 ) )
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 ral0 
 |-  A. i e. (/) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G )
8 oveq1 
 |-  ( ( # ` W ) = 1 -> ( ( # ` W ) - 1 ) = ( 1 - 1 ) )
9 1m1e0 
 |-  ( 1 - 1 ) = 0
10 8 9 eqtrdi 
 |-  ( ( # ` W ) = 1 -> ( ( # ` W ) - 1 ) = 0 )
11 10 oveq2d 
 |-  ( ( # ` W ) = 1 -> ( 0 ..^ ( ( # ` W ) - 1 ) ) = ( 0 ..^ 0 ) )
12 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
13 11 12 eqtrdi 
 |-  ( ( # ` W ) = 1 -> ( 0 ..^ ( ( # ` W ) - 1 ) ) = (/) )
14 13 raleqdv 
 |-  ( ( # ` W ) = 1 -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. (/) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
15 14 adantr 
 |-  ( ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. (/) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
16 7 15 mpbiri 
 |-  ( ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) ) -> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) )
17 16 biantrurd 
 |-  ( ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
18 lsw1 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 1 ) -> ( lastS ` W ) = ( W ` 0 ) )
19 18 ancoms 
 |-  ( ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) ) -> ( lastS ` W ) = ( W ` 0 ) )
20 19 preq1d 
 |-  ( ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) ) -> { ( lastS ` W ) , ( W ` 0 ) } = { ( W ` 0 ) , ( W ` 0 ) } )
21 dfsn2 
 |-  { ( W ` 0 ) } = { ( W ` 0 ) , ( W ` 0 ) }
22 20 21 eqtr4di 
 |-  ( ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) ) -> { ( lastS ` W ) , ( W ` 0 ) } = { ( W ` 0 ) } )
23 22 eleq1d 
 |-  ( ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) <-> { ( W ` 0 ) } e. ( Edg ` G ) ) )
24 17 23 bitr3d 
 |-  ( ( ( # ` W ) = 1 /\ 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 ) } e. ( Edg ` G ) ) )
25 24 pm5.32da 
 |-  ( ( # ` W ) = 1 -> ( ( 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 ) } e. ( Edg ` G ) ) ) )
26 6 25 bitrid 
 |-  ( ( # ` W ) = 1 -> ( ( 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 ) } e. ( Edg ` G ) ) ) )
27 26 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 ) = 1 ) <-> ( ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 1 ) )
28 3anass 
 |-  ( ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( ( # ` W ) = 1 /\ ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) ) )
29 ancom 
 |-  ( ( ( # ` W ) = 1 /\ ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) ) <-> ( ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 1 ) )
30 28 29 bitr2i 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 1 ) <-> ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) )
31 5 27 30 3bitri 
 |-  ( W e. ( 1 ClWWalksN G ) <-> ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) )