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 e. V ) -> ( # ` { w e. ( 1 WWalksN G ) | ( w ` 0 ) = P } ) = K )

Proof

Step Hyp Ref Expression
1 rusgrnumwwlkl1.v 
 |-  V = ( Vtx ` G )
2 1nn0 
 |-  1 e. NN0
3 iswwlksn 
 |-  ( 1 e. NN0 -> ( w e. ( 1 WWalksN G ) <-> ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( 1 + 1 ) ) ) )
4 2 3 ax-mp 
 |-  ( w e. ( 1 WWalksN G ) <-> ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( 1 + 1 ) ) )
5 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
6 1 5 iswwlks 
 |-  ( w e. ( WWalks ` G ) <-> ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
7 6 anbi1i 
 |-  ( ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( 1 + 1 ) ) <-> ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( 1 + 1 ) ) )
8 4 7 bitri 
 |-  ( w e. ( 1 WWalksN G ) <-> ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( 1 + 1 ) ) )
9 8 a1i 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( w e. ( 1 WWalksN G ) <-> ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( 1 + 1 ) ) ) )
10 9 anbi1d 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( ( w e. ( 1 WWalksN G ) /\ ( w ` 0 ) = P ) <-> ( ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( 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 e. V ) -> ( ( # ` w ) = ( 1 + 1 ) <-> ( # ` w ) = 2 ) )
14 13 anbi2d 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( 1 + 1 ) ) <-> ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = 2 ) ) )
15 3anass 
 |-  ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( w =/= (/) /\ ( w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
16 15 a1i 
 |-  ( ( ( G RegUSGraph K /\ P e. V ) /\ ( # ` w ) = 2 ) -> ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( w =/= (/) /\ ( w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( 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 e. V ) /\ ( # ` w ) = 2 ) -> w =/= (/) )
27 26 biantrurd 
 |-  ( ( ( G RegUSGraph K /\ P e. V ) /\ ( # ` w ) = 2 ) -> ( ( w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( w =/= (/) /\ ( w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( 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 e. V ) /\ ( # ` w ) = 2 ) -> ( 0 ..^ ( ( # ` w ) - 1 ) ) = ( 0 ..^ 1 ) )
33 32 raleqdv 
 |-  ( ( ( G RegUSGraph K /\ P e. V ) /\ ( # ` w ) = 2 ) -> ( A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ 1 ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
34 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
35 34 raleqi 
 |-  ( A. i e. ( 0 ..^ 1 ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. { 0 } { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) )
36 c0ex 
 |-  0 e. _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 ) ) } e. ( Edg ` G ) <-> { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) )
41 36 40 ralsn 
 |-  ( A. i e. { 0 } { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) )
42 35 41 bitri 
 |-  ( A. i e. ( 0 ..^ 1 ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) )
43 33 42 bitrdi 
 |-  ( ( ( G RegUSGraph K /\ P e. V ) /\ ( # ` w ) = 2 ) -> ( A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) )
44 43 anbi2d 
 |-  ( ( ( G RegUSGraph K /\ P e. V ) /\ ( # ` w ) = 2 ) -> ( ( w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( w e. Word V /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) ) )
45 16 27 44 3bitr2d 
 |-  ( ( ( G RegUSGraph K /\ P e. V ) /\ ( # ` w ) = 2 ) -> ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( w e. Word V /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) ) )
46 45 ex 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( ( # ` w ) = 2 -> ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( w e. Word V /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) ) ) )
47 46 pm5.32rd 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = 2 ) <-> ( ( w e. Word V /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( # ` w ) = 2 ) ) )
48 14 47 bitrd 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( 1 + 1 ) ) <-> ( ( w e. Word V /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( # ` w ) = 2 ) ) )
49 48 anbi1d 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( ( ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( 1 + 1 ) ) /\ ( w ` 0 ) = P ) <-> ( ( ( w e. Word V /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( # ` w ) = 2 ) /\ ( w ` 0 ) = P ) ) )
50 anass 
 |-  ( ( ( ( w e. Word V /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( # ` w ) = 2 ) /\ ( w ` 0 ) = P ) <-> ( ( w e. Word V /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P ) ) )
51 49 50 bitrdi 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( ( ( ( w =/= (/) /\ w e. Word V /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( 1 + 1 ) ) /\ ( w ` 0 ) = P ) <-> ( ( w e. Word V /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P ) ) ) )
52 anass 
 |-  ( ( ( w e. Word V /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P ) ) <-> ( w e. Word V /\ ( { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P ) ) ) )
53 ancom 
 |-  ( ( { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P ) ) <-> ( ( ( # ` w ) = 2 /\ ( w ` 0 ) = P ) /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) )
54 df-3an 
 |-  ( ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) <-> ( ( ( # ` w ) = 2 /\ ( w ` 0 ) = P ) /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) )
55 53 54 bitr4i 
 |-  ( ( { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P ) ) <-> ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) )
56 55 anbi2i 
 |-  ( ( w e. Word V /\ ( { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P ) ) ) <-> ( w e. Word V /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) ) )
57 52 56 bitri 
 |-  ( ( ( w e. Word V /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P ) ) <-> ( w e. Word V /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) ) )
58 57 a1i 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( ( ( w e. Word V /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P ) ) <-> ( w e. Word V /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) ) ) )
59 10 51 58 3bitrd 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( ( w e. ( 1 WWalksN G ) /\ ( w ` 0 ) = P ) <-> ( w e. Word V /\ ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) ) ) )
60 59 rabbidva2 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> { w e. ( 1 WWalksN G ) | ( w ` 0 ) = P } = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } )
61 60 fveq2d 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( # ` { w e. ( 1 WWalksN G ) | ( w ` 0 ) = P } ) = ( # ` { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } ) )
62 1 rusgrnumwrdl2 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( # ` { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } ) = K )
63 61 62 eqtrd 
 |-  ( ( G RegUSGraph K /\ P e. V ) -> ( # ` { w e. ( 1 WWalksN G ) | ( w ` 0 ) = P } ) = K )