Metamath Proof Explorer


Theorem wlkl0

Description: There is exactly one walk of length 0 on each vertex X . (Contributed by AV, 4-Jun-2022)

Ref Expression
Hypothesis clwlknon2num.v V = Vtx G
Assertion wlkl0 X V w ClWalks G | 1 st w = 0 2 nd w 0 = X = 0 X

Proof

Step Hyp Ref Expression
1 clwlknon2num.v V = Vtx G
2 clwlkwlk w ClWalks G w Walks G
3 wlkop w Walks G w = 1 st w 2 nd w
4 2 3 syl w ClWalks G w = 1 st w 2 nd w
5 fvex 1 st w V
6 hasheq0 1 st w V 1 st w = 0 1 st w =
7 5 6 ax-mp 1 st w = 0 1 st w =
8 7 biimpi 1 st w = 0 1 st w =
9 8 adantr 1 st w = 0 2 nd w 0 = X 1 st w =
10 9 3ad2ant3 X V 1 st w ClWalks G 2 nd w 1 st w = 0 2 nd w 0 = X 1 st w =
11 9 adantl X V 1 st w = 0 2 nd w 0 = X 1 st w =
12 11 breq1d X V 1 st w = 0 2 nd w 0 = X 1 st w ClWalks G 2 nd w ClWalks G 2 nd w
13 1 1vgrex X V G V
14 1 0clwlk G V ClWalks G 2 nd w 2 nd w : 0 0 V
15 13 14 syl X V ClWalks G 2 nd w 2 nd w : 0 0 V
16 15 adantr X V 1 st w = 0 2 nd w 0 = X ClWalks G 2 nd w 2 nd w : 0 0 V
17 12 16 bitrd X V 1 st w = 0 2 nd w 0 = X 1 st w ClWalks G 2 nd w 2 nd w : 0 0 V
18 fz0sn 0 0 = 0
19 18 feq2i 2 nd w : 0 0 V 2 nd w : 0 V
20 c0ex 0 V
21 20 fsn2 2 nd w : 0 V 2 nd w 0 V 2 nd w = 0 2 nd w 0
22 simprr X V 1 st w = 0 2 nd w 0 = X 2 nd w 0 V 2 nd w = 0 2 nd w 0 2 nd w = 0 2 nd w 0
23 simprr X V 1 st w = 0 2 nd w 0 = X 2 nd w 0 = X
24 23 adantr X V 1 st w = 0 2 nd w 0 = X 2 nd w 0 V 2 nd w = 0 2 nd w 0 2 nd w 0 = X
25 24 opeq2d X V 1 st w = 0 2 nd w 0 = X 2 nd w 0 V 2 nd w = 0 2 nd w 0 0 2 nd w 0 = 0 X
26 25 sneqd X V 1 st w = 0 2 nd w 0 = X 2 nd w 0 V 2 nd w = 0 2 nd w 0 0 2 nd w 0 = 0 X
27 22 26 eqtrd X V 1 st w = 0 2 nd w 0 = X 2 nd w 0 V 2 nd w = 0 2 nd w 0 2 nd w = 0 X
28 27 ex X V 1 st w = 0 2 nd w 0 = X 2 nd w 0 V 2 nd w = 0 2 nd w 0 2 nd w = 0 X
29 21 28 syl5bi X V 1 st w = 0 2 nd w 0 = X 2 nd w : 0 V 2 nd w = 0 X
30 19 29 syl5bi X V 1 st w = 0 2 nd w 0 = X 2 nd w : 0 0 V 2 nd w = 0 X
31 17 30 sylbid X V 1 st w = 0 2 nd w 0 = X 1 st w ClWalks G 2 nd w 2 nd w = 0 X
32 31 ex X V 1 st w = 0 2 nd w 0 = X 1 st w ClWalks G 2 nd w 2 nd w = 0 X
33 32 com23 X V 1 st w ClWalks G 2 nd w 1 st w = 0 2 nd w 0 = X 2 nd w = 0 X
34 33 3imp X V 1 st w ClWalks G 2 nd w 1 st w = 0 2 nd w 0 = X 2 nd w = 0 X
35 10 34 opeq12d X V 1 st w ClWalks G 2 nd w 1 st w = 0 2 nd w 0 = X 1 st w 2 nd w = 0 X
36 35 3exp X V 1 st w ClWalks G 2 nd w 1 st w = 0 2 nd w 0 = X 1 st w 2 nd w = 0 X
37 eleq1 w = 1 st w 2 nd w w ClWalks G 1 st w 2 nd w ClWalks G
38 df-br 1 st w ClWalks G 2 nd w 1 st w 2 nd w ClWalks G
39 37 38 bitr4di w = 1 st w 2 nd w w ClWalks G 1 st w ClWalks G 2 nd w
40 eqeq1 w = 1 st w 2 nd w w = 0 X 1 st w 2 nd w = 0 X
41 40 imbi2d w = 1 st w 2 nd w 1 st w = 0 2 nd w 0 = X w = 0 X 1 st w = 0 2 nd w 0 = X 1 st w 2 nd w = 0 X
42 39 41 imbi12d w = 1 st w 2 nd w w ClWalks G 1 st w = 0 2 nd w 0 = X w = 0 X 1 st w ClWalks G 2 nd w 1 st w = 0 2 nd w 0 = X 1 st w 2 nd w = 0 X
43 36 42 syl5ibr w = 1 st w 2 nd w X V w ClWalks G 1 st w = 0 2 nd w 0 = X w = 0 X
44 43 com23 w = 1 st w 2 nd w w ClWalks G X V 1 st w = 0 2 nd w 0 = X w = 0 X
45 4 44 mpcom w ClWalks G X V 1 st w = 0 2 nd w 0 = X w = 0 X
46 45 com12 X V w ClWalks G 1 st w = 0 2 nd w 0 = X w = 0 X
47 46 impd X V w ClWalks G 1 st w = 0 2 nd w 0 = X w = 0 X
48 eqidd X V =
49 20 a1i X V 0 V
50 snidg X V X X
51 49 50 fsnd X V 0 X : 0 X
52 1 0clwlkv X V = 0 X : 0 X ClWalks G 0 X
53 48 51 52 mpd3an23 X V ClWalks G 0 X
54 hash0 = 0
55 54 a1i X V = 0
56 fvsng 0 V X V 0 X 0 = X
57 20 56 mpan X V 0 X 0 = X
58 53 55 57 jca32 X V ClWalks G 0 X = 0 0 X 0 = X
59 eleq1 w = 0 X w ClWalks G 0 X ClWalks G
60 df-br ClWalks G 0 X 0 X ClWalks G
61 59 60 bitr4di w = 0 X w ClWalks G ClWalks G 0 X
62 0ex V
63 snex 0 X V
64 62 63 op1std w = 0 X 1 st w =
65 64 fveqeq2d w = 0 X 1 st w = 0 = 0
66 62 63 op2ndd w = 0 X 2 nd w = 0 X
67 66 fveq1d w = 0 X 2 nd w 0 = 0 X 0
68 67 eqeq1d w = 0 X 2 nd w 0 = X 0 X 0 = X
69 65 68 anbi12d w = 0 X 1 st w = 0 2 nd w 0 = X = 0 0 X 0 = X
70 61 69 anbi12d w = 0 X w ClWalks G 1 st w = 0 2 nd w 0 = X ClWalks G 0 X = 0 0 X 0 = X
71 58 70 syl5ibrcom X V w = 0 X w ClWalks G 1 st w = 0 2 nd w 0 = X
72 47 71 impbid X V w ClWalks G 1 st w = 0 2 nd w 0 = X w = 0 X
73 72 alrimiv X V w w ClWalks G 1 st w = 0 2 nd w 0 = X w = 0 X
74 rabeqsn w ClWalks G | 1 st w = 0 2 nd w 0 = X = 0 X w w ClWalks G 1 st w = 0 2 nd w 0 = X w = 0 X
75 73 74 sylibr X V w ClWalks G | 1 st w = 0 2 nd w 0 = X = 0 X