Metamath Proof Explorer

Theorem wlkl1loop

Description: A walk of length 1 from a vertex to itself is a loop. (Contributed by AV, 23-Apr-2021)

Ref Expression
Assertion wlkl1loop 
|- ( ( ( Fun ( iEdg ` G ) /\ F ( Walks ` G ) P ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> { ( P ` 0 ) } e. ( Edg ` G ) )

Proof

Step Hyp Ref Expression
1 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
2 simp3l 
 |-  ( ( G e. _V /\ F ( Walks ` G ) P /\ ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) ) -> Fun ( iEdg ` G ) )
3 simp2 
 |-  ( ( G e. _V /\ F ( Walks ` G ) P /\ ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) ) -> F ( Walks ` G ) P )
4 c0ex 
 |-  0 e. _V
5 4 snid 
 |-  0 e. { 0 }
6 oveq2 
 |-  ( ( # ` F ) = 1 -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 1 ) )
7 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
8 6 7 eqtrdi 
 |-  ( ( # ` F ) = 1 -> ( 0 ..^ ( # ` F ) ) = { 0 } )
9 5 8 eleqtrrid 
 |-  ( ( # ` F ) = 1 -> 0 e. ( 0 ..^ ( # ` F ) ) )
10 9 ad2antrl 
 |-  ( ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> 0 e. ( 0 ..^ ( # ` F ) ) )
11 10 3ad2ant3 
 |-  ( ( G e. _V /\ F ( Walks ` G ) P /\ ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) ) -> 0 e. ( 0 ..^ ( # ` F ) ) )
12 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
13 12 iedginwlk 
 |-  ( ( Fun ( iEdg ` G ) /\ F ( Walks ` G ) P /\ 0 e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` 0 ) ) e. ran ( iEdg ` G ) )
14 2 3 11 13 syl3anc 
 |-  ( ( G e. _V /\ F ( Walks ` G ) P /\ ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) ) -> ( ( iEdg ` G ) ` ( F ` 0 ) ) e. ran ( iEdg ` G ) )
15 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
16 15 12 iswlkg 
 |-  ( G e. _V -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
17 8 raleqdv 
 |-  ( ( # ` F ) = 1 -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) <-> A. k e. { 0 } if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
18 oveq1 
 |-  ( k = 0 -> ( k + 1 ) = ( 0 + 1 ) )
19 0p1e1 
 |-  ( 0 + 1 ) = 1
20 18 19 eqtrdi 
 |-  ( k = 0 -> ( k + 1 ) = 1 )
21 wkslem2 
 |-  ( ( k = 0 /\ ( k + 1 ) = 1 ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) <-> if- ( ( P ` 0 ) = ( P ` 1 ) , ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( ( iEdg ` G ) ` ( F ` 0 ) ) ) ) )
22 20 21 mpdan 
 |-  ( k = 0 -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) <-> if- ( ( P ` 0 ) = ( P ` 1 ) , ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( ( iEdg ` G ) ` ( F ` 0 ) ) ) ) )
23 4 22 ralsn 
 |-  ( A. k e. { 0 } if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) <-> if- ( ( P ` 0 ) = ( P ` 1 ) , ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( ( iEdg ` G ) ` ( F ` 0 ) ) ) )
24 17 23 bitrdi 
 |-  ( ( # ` F ) = 1 -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) <-> if- ( ( P ` 0 ) = ( P ` 1 ) , ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( ( iEdg ` G ) ` ( F ` 0 ) ) ) ) )
25 24 ad2antrl 
 |-  ( ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) <-> if- ( ( P ` 0 ) = ( P ` 1 ) , ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( ( iEdg ` G ) ` ( F ` 0 ) ) ) ) )
26 ifptru 
 |-  ( ( P ` 0 ) = ( P ` 1 ) -> ( if- ( ( P ` 0 ) = ( P ` 1 ) , ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( ( iEdg ` G ) ` ( F ` 0 ) ) ) <-> ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) } ) )
27 26 biimpa 
 |-  ( ( ( P ` 0 ) = ( P ` 1 ) /\ if- ( ( P ` 0 ) = ( P ` 1 ) , ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( ( iEdg ` G ) ` ( F ` 0 ) ) ) ) -> ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) } )
28 27 eqcomd 
 |-  ( ( ( P ` 0 ) = ( P ` 1 ) /\ if- ( ( P ` 0 ) = ( P ` 1 ) , ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( ( iEdg ` G ) ` ( F ` 0 ) ) ) ) -> { ( P ` 0 ) } = ( ( iEdg ` G ) ` ( F ` 0 ) ) )
29 28 ex 
 |-  ( ( P ` 0 ) = ( P ` 1 ) -> ( if- ( ( P ` 0 ) = ( P ` 1 ) , ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( ( iEdg ` G ) ` ( F ` 0 ) ) ) -> { ( P ` 0 ) } = ( ( iEdg ` G ) ` ( F ` 0 ) ) ) )
30 29 ad2antll 
 |-  ( ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> ( if- ( ( P ` 0 ) = ( P ` 1 ) , ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( ( iEdg ` G ) ` ( F ` 0 ) ) ) -> { ( P ` 0 ) } = ( ( iEdg ` G ) ` ( F ` 0 ) ) ) )
31 25 30 sylbid 
 |-  ( ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> { ( P ` 0 ) } = ( ( iEdg ` G ) ` ( F ` 0 ) ) ) )
32 31 com12 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> ( ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> { ( P ` 0 ) } = ( ( iEdg ` G ) ` ( F ` 0 ) ) ) )
33 32 3ad2ant3 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> { ( P ` 0 ) } = ( ( iEdg ` G ) ` ( F ` 0 ) ) ) )
34 16 33 syl6bi 
 |-  ( G e. _V -> ( F ( Walks ` G ) P -> ( ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> { ( P ` 0 ) } = ( ( iEdg ` G ) ` ( F ` 0 ) ) ) ) )
35 34 3imp 
 |-  ( ( G e. _V /\ F ( Walks ` G ) P /\ ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) ) -> { ( P ` 0 ) } = ( ( iEdg ` G ) ` ( F ` 0 ) ) )
36 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
37 36 a1i 
 |-  ( ( G e. _V /\ F ( Walks ` G ) P /\ ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) ) -> ( Edg ` G ) = ran ( iEdg ` G ) )
38 14 35 37 3eltr4d 
 |-  ( ( G e. _V /\ F ( Walks ` G ) P /\ ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) ) -> { ( P ` 0 ) } e. ( Edg ` G ) )
39 38 3exp 
 |-  ( G e. _V -> ( F ( Walks ` G ) P -> ( ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> { ( P ` 0 ) } e. ( Edg ` G ) ) ) )
40 39 3ad2ant1 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( Walks ` G ) P -> ( ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> { ( P ` 0 ) } e. ( Edg ` G ) ) ) )
41 1 40 mpcom 
 |-  ( F ( Walks ` G ) P -> ( ( Fun ( iEdg ` G ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> { ( P ` 0 ) } e. ( Edg ` G ) ) )
42 41 expd 
 |-  ( F ( Walks ` G ) P -> ( Fun ( iEdg ` G ) -> ( ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) -> { ( P ` 0 ) } e. ( Edg ` G ) ) ) )
43 42 impcom 
 |-  ( ( Fun ( iEdg ` G ) /\ F ( Walks ` G ) P ) -> ( ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) -> { ( P ` 0 ) } e. ( Edg ` G ) ) )
44 43 imp 
 |-  ( ( ( Fun ( iEdg ` G ) /\ F ( Walks ` G ) P ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> { ( P ` 0 ) } e. ( Edg ` G ) )