This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0wlkon

Description: A walk of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 3-Jan-2021) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Hypothesis 0wlk.v 
|- V = ( Vtx ` G )
Assertion 0wlkon 
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( N ( WalksOn ` G ) N ) P )

Proof

Step Hyp Ref Expression
1 0wlk.v 
 |-  V = ( Vtx ` G )
2 simpl 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> P : ( 0 ... 0 ) --> V )
3 1 0wlkonlem1 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( N e. V /\ N e. V ) )
4 1 1vgrex 
 |-  ( N e. V -> G e. _V )
5 4 adantr 
 |-  ( ( N e. V /\ N e. V ) -> G e. _V )
6 1 0wlk 
 |-  ( G e. _V -> ( (/) ( Walks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
7 3 5 6 3syl 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( (/) ( Walks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
8 2 7 mpbird 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( Walks ` G ) P )
9 simpr 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( P ` 0 ) = N )
10 hash0 
 |-  ( # ` (/) ) = 0
11 10 fveq2i 
 |-  ( P ` ( # ` (/) ) ) = ( P ` 0 )
12 11 9 eqtrid 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( P ` ( # ` (/) ) ) = N )
13 0ex 
 |-  (/) e. _V
14 13 a1i 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) e. _V )
15 1 0wlkonlem2 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> P e. ( V ^pm ( 0 ... 0 ) ) )
16 1 iswlkon 
 |-  ( ( ( N e. V /\ N e. V ) /\ ( (/) e. _V /\ P e. ( V ^pm ( 0 ... 0 ) ) ) ) -> ( (/) ( N ( WalksOn ` G ) N ) P <-> ( (/) ( Walks ` G ) P /\ ( P ` 0 ) = N /\ ( P ` ( # ` (/) ) ) = N ) ) )
17 3 14 15 16 syl12anc 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( (/) ( N ( WalksOn ` G ) N ) P <-> ( (/) ( Walks ` G ) P /\ ( P ` 0 ) = N /\ ( P ` ( # ` (/) ) ) = N ) ) )
18 8 9 12 17 mpbir3and 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( N ( WalksOn ` G ) N ) P )