Description: A closed walk of a fixed length as word is a word over the vertices. (Contributed by AV, 30-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | clwwlknwrd.v | |- V = ( Vtx ` G ) |
|
Assertion | clwwlknwrd | |- ( W e. ( N ClWWalksN G ) -> W e. Word V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clwwlknwrd.v | |- V = ( Vtx ` G ) |
|
2 | isclwwlkn | |- ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) ) |
|
3 | 1 | clwwlkbp | |- ( W e. ( ClWWalks ` G ) -> ( G e. _V /\ W e. Word V /\ W =/= (/) ) ) |
4 | 3 | simp2d | |- ( W e. ( ClWWalks ` G ) -> W e. Word V ) |
5 | 4 | adantr | |- ( ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) -> W e. Word V ) |
6 | 2 5 | sylbi | |- ( W e. ( N ClWWalksN G ) -> W e. Word V ) |