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 V N V
4 1 1vgrex N V G V
5 4 adantr N V N V G V
6 1 0wlk G 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 V
14 13 a1i P : 0 0 V P 0 = N V
15 1 0wlkonlem2 P : 0 0 V P 0 = N P V 𝑝𝑚 0 0
16 1 iswlkon N V N V V P V 𝑝𝑚 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