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 ⊢GRegUSGraphK∧P∈V→w∈1WWalksNG|w⁡0=P=K

Proof

Step Hyp Ref Expression
1 rusgrnumwwlkl1.v ⊢V=Vtx⁡G
2 1nn0 ⊢1∈ℕ0
3 iswwlksn ⊢1∈ℕ0→w∈1WWalksNG↔w∈WWalks⁡G∧w=1+1
4 2 3 ax-mp ⊢w∈1WWalksNG↔w∈WWalks⁡G∧w=1+1
5 eqid ⊢Edg⁡G=Edg⁡G
6 1 5 iswwlks ⊢w∈WWalks⁡G↔w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G
7 6 anbi1i ⊢w∈WWalks⁡G∧w=1+1↔w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=1+1
8 4 7 bitri ⊢w∈1WWalksNG↔w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=1+1
9 8 a1i ⊢GRegUSGraphK∧P∈V→w∈1WWalksNG↔w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=1+1
10 9 anbi1d ⊢GRegUSGraphK∧P∈V→w∈1WWalksNG∧w⁡0=P↔w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡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 ⊢GRegUSGraphK∧P∈V→w=1+1↔w=2
14 13 anbi2d ⊢GRegUSGraphK∧P∈V→w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=1+1↔w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=2
15 3anass ⊢w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G↔w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G
16 15 a1i ⊢GRegUSGraphK∧P∈V∧w=2→w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G↔w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡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 ⊢GRegUSGraphK∧P∈V∧w=2→w≠∅
27 26 biantrurd ⊢GRegUSGraphK∧P∈V∧w=2→w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G↔w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡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 ⊢GRegUSGraphK∧P∈V∧w=2→0..^w−1=0..^1
33 32 raleqdv ⊢GRegUSGraphK∧P∈V∧w=2→∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G↔∀i∈0..^1w⁡iw⁡i+1∈Edg⁡G
34 fzo01 ⊢0..^1=0
35 34 raleqi ⊢∀i∈0..^1w⁡iw⁡i+1∈Edg⁡G↔∀i∈0w⁡iw⁡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⁡iw⁡i+1=w⁡0w⁡1
40 39 eleq1d ⊢i=0→w⁡iw⁡i+1∈Edg⁡G↔w⁡0w⁡1∈Edg⁡G
41 36 40 ralsn ⊢∀i∈0w⁡iw⁡i+1∈Edg⁡G↔w⁡0w⁡1∈Edg⁡G
42 35 41 bitri ⊢∀i∈0..^1w⁡iw⁡i+1∈Edg⁡G↔w⁡0w⁡1∈Edg⁡G
43 33 42 bitrdi ⊢GRegUSGraphK∧P∈V∧w=2→∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G↔w⁡0w⁡1∈Edg⁡G
44 43 anbi2d ⊢GRegUSGraphK∧P∈V∧w=2→w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G↔w∈WordV∧w⁡0w⁡1∈Edg⁡G
45 16 27 44 3bitr2d ⊢GRegUSGraphK∧P∈V∧w=2→w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G↔w∈WordV∧w⁡0w⁡1∈Edg⁡G
46 45 ex ⊢GRegUSGraphK∧P∈V→w=2→w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G↔w∈WordV∧w⁡0w⁡1∈Edg⁡G
47 46 pm5.32rd ⊢GRegUSGraphK∧P∈V→w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=2↔w∈WordV∧w⁡0w⁡1∈Edg⁡G∧w=2
48 14 47 bitrd ⊢GRegUSGraphK∧P∈V→w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=1+1↔w∈WordV∧w⁡0w⁡1∈Edg⁡G∧w=2
49 48 anbi1d ⊢GRegUSGraphK∧P∈V→w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=1+1∧w⁡0=P↔w∈WordV∧w⁡0w⁡1∈Edg⁡G∧w=2∧w⁡0=P
50 anass ⊢w∈WordV∧w⁡0w⁡1∈Edg⁡G∧w=2∧w⁡0=P↔w∈WordV∧w⁡0w⁡1∈Edg⁡G∧w=2∧w⁡0=P
51 49 50 bitrdi ⊢GRegUSGraphK∧P∈V→w≠∅∧w∈WordV∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=1+1∧w⁡0=P↔w∈WordV∧w⁡0w⁡1∈Edg⁡G∧w=2∧w⁡0=P
52 anass ⊢w∈WordV∧w⁡0w⁡1∈Edg⁡G∧w=2∧w⁡0=P↔w∈WordV∧w⁡0w⁡1∈Edg⁡G∧w=2∧w⁡0=P
53 ancom ⊢w⁡0w⁡1∈Edg⁡G∧w=2∧w⁡0=P↔w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G
54 df-3an ⊢w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G↔w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G
55 53 54 bitr4i ⊢w⁡0w⁡1∈Edg⁡G∧w=2∧w⁡0=P↔w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G
56 55 anbi2i ⊢w∈WordV∧w⁡0w⁡1∈Edg⁡G∧w=2∧w⁡0=P↔w∈WordV∧w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G
57 52 56 bitri ⊢w∈WordV∧w⁡0w⁡1∈Edg⁡G∧w=2∧w⁡0=P↔w∈WordV∧w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G
58 57 a1i ⊢GRegUSGraphK∧P∈V→w∈WordV∧w⁡0w⁡1∈Edg⁡G∧w=2∧w⁡0=P↔w∈WordV∧w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G
59 10 51 58 3bitrd ⊢GRegUSGraphK∧P∈V→w∈1WWalksNG∧w⁡0=P↔w∈WordV∧w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G
60 59 rabbidva2 ⊢GRegUSGraphK∧P∈V→w∈1WWalksNG|w⁡0=P=w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G
61 60 fveq2d ⊢GRegUSGraphK∧P∈V→w∈1WWalksNG|w⁡0=P=w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G
62 1 rusgrnumwrdl2 ⊢GRegUSGraphK∧P∈V→w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G=K
63 61 62 eqtrd ⊢GRegUSGraphK∧P∈V→w∈1WWalksNG|w⁡0=P=K