Metamath Proof Explorer


Theorem rusgrnumwwlkl1

Description: In a k-regular graph, there are k walks (as word) of length 1 starting at each vertex. (Contributed by Alexander van der Vekens, 28-Jul-2018) (Revised by AV, 7-May-2021)

Ref Expression
Hypothesis rusgrnumwwlkl1.v V = Vtx G
Assertion rusgrnumwwlkl1 G RegUSGraph K P V w 1 WWalksN G | w 0 = P = K

Proof

Step Hyp Ref Expression
1 rusgrnumwwlkl1.v V = Vtx G
2 1nn0 1 0
3 iswwlksn 1 0 w 1 WWalksN G w WWalks G w = 1 + 1
4 2 3 ax-mp w 1 WWalksN G w WWalks G w = 1 + 1
5 eqid Edg G = Edg G
6 1 5 iswwlks w WWalks G w w Word V i 0 ..^ w 1 w i w i + 1 Edg G
7 6 anbi1i w WWalks G w = 1 + 1 w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w = 1 + 1
8 4 7 bitri w 1 WWalksN G w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w = 1 + 1
9 8 a1i G RegUSGraph K P V w 1 WWalksN G w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w = 1 + 1
10 9 anbi1d G RegUSGraph K P V w 1 WWalksN G w 0 = P w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w = 1 + 1 w 0 = P
11 1p1e2 1 + 1 = 2
12 11 eqeq2i w = 1 + 1 w = 2
13 12 a1i G RegUSGraph K P V w = 1 + 1 w = 2
14 13 anbi2d G RegUSGraph K P V w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w = 1 + 1 w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w = 2
15 3anass w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w w Word V i 0 ..^ w 1 w i w i + 1 Edg G
16 15 a1i G RegUSGraph K P V w = 2 w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w w Word V i 0 ..^ w 1 w i w i + 1 Edg G
17 fveq2 w = w =
18 hash0 = 0
19 17 18 eqtrdi w = w = 0
20 2ne0 2 0
21 20 nesymi ¬ 0 = 2
22 eqeq1 w = 0 w = 2 0 = 2
23 21 22 mtbiri w = 0 ¬ w = 2
24 19 23 syl w = ¬ w = 2
25 24 necon2ai w = 2 w
26 25 adantl G RegUSGraph K P V w = 2 w
27 26 biantrurd G RegUSGraph K P V w = 2 w Word V i 0 ..^ w 1 w i w i + 1 Edg G w w Word V i 0 ..^ w 1 w i w i + 1 Edg G
28 oveq1 w = 2 w 1 = 2 1
29 2m1e1 2 1 = 1
30 28 29 eqtrdi w = 2 w 1 = 1
31 30 oveq2d w = 2 0 ..^ w 1 = 0 ..^ 1
32 31 adantl G RegUSGraph K P V w = 2 0 ..^ w 1 = 0 ..^ 1
33 32 raleqdv G RegUSGraph K P V w = 2 i 0 ..^ w 1 w i w i + 1 Edg G i 0 ..^ 1 w i w i + 1 Edg G
34 fzo01 0 ..^ 1 = 0
35 34 raleqi i 0 ..^ 1 w i w i + 1 Edg G i 0 w i w i + 1 Edg G
36 c0ex 0 V
37 fveq2 i = 0 w i = w 0
38 fv0p1e1 i = 0 w i + 1 = w 1
39 37 38 preq12d i = 0 w i w i + 1 = w 0 w 1
40 39 eleq1d i = 0 w i w i + 1 Edg G w 0 w 1 Edg G
41 36 40 ralsn i 0 w i w i + 1 Edg G w 0 w 1 Edg G
42 35 41 bitri i 0 ..^ 1 w i w i + 1 Edg G w 0 w 1 Edg G
43 33 42 bitrdi G RegUSGraph K P V w = 2 i 0 ..^ w 1 w i w i + 1 Edg G w 0 w 1 Edg G
44 43 anbi2d G RegUSGraph K P V w = 2 w Word V i 0 ..^ w 1 w i w i + 1 Edg G w Word V w 0 w 1 Edg G
45 16 27 44 3bitr2d G RegUSGraph K P V w = 2 w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w Word V w 0 w 1 Edg G
46 45 ex G RegUSGraph K P V w = 2 w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w Word V w 0 w 1 Edg G
47 46 pm5.32rd G RegUSGraph K P V w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w = 2 w Word V w 0 w 1 Edg G w = 2
48 14 47 bitrd G RegUSGraph K P V w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w = 1 + 1 w Word V w 0 w 1 Edg G w = 2
49 48 anbi1d G RegUSGraph K P V w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w = 1 + 1 w 0 = P w Word V w 0 w 1 Edg G w = 2 w 0 = P
50 anass w Word V w 0 w 1 Edg G w = 2 w 0 = P w Word V w 0 w 1 Edg G w = 2 w 0 = P
51 49 50 bitrdi G RegUSGraph K P V w w Word V i 0 ..^ w 1 w i w i + 1 Edg G w = 1 + 1 w 0 = P w Word V w 0 w 1 Edg G w = 2 w 0 = P
52 anass w Word V w 0 w 1 Edg G w = 2 w 0 = P w Word V w 0 w 1 Edg G w = 2 w 0 = P
53 ancom w 0 w 1 Edg G w = 2 w 0 = P w = 2 w 0 = P w 0 w 1 Edg G
54 df-3an w = 2 w 0 = P w 0 w 1 Edg G w = 2 w 0 = P w 0 w 1 Edg G
55 53 54 bitr4i w 0 w 1 Edg G w = 2 w 0 = P w = 2 w 0 = P w 0 w 1 Edg G
56 55 anbi2i w Word V w 0 w 1 Edg G w = 2 w 0 = P w Word V w = 2 w 0 = P w 0 w 1 Edg G
57 52 56 bitri w Word V w 0 w 1 Edg G w = 2 w 0 = P w Word V w = 2 w 0 = P w 0 w 1 Edg G
58 57 a1i G RegUSGraph K P V w Word V w 0 w 1 Edg G w = 2 w 0 = P w Word V w = 2 w 0 = P w 0 w 1 Edg G
59 10 51 58 3bitrd G RegUSGraph K P V w 1 WWalksN G w 0 = P w Word V w = 2 w 0 = P w 0 w 1 Edg G
60 59 rabbidva2 G RegUSGraph K P V w 1 WWalksN G | w 0 = P = w Word V | w = 2 w 0 = P w 0 w 1 Edg G
61 60 fveq2d G RegUSGraph K P V w 1 WWalksN G | w 0 = P = w Word V | w = 2 w 0 = P w 0 w 1 Edg G
62 1 rusgrnumwrdl2 G RegUSGraph K P V w Word V | w = 2 w 0 = P w 0 w 1 Edg G = K
63 61 62 eqtrd G RegUSGraph K P V w 1 WWalksN G | w 0 = P = K