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 ) )