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