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