Description: In a friendship graph, the size of the set of walks of length N starting with a fixed vertex X and ending not at this vertex equals the size of the set of all closed walks of length ( N + 2 ) starting at this vertex X and not having this vertex as last but 2 vertex. (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 31-May-2021) (Proof shortened by AV, 3-Nov-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | numclwwlk.v | |- V = ( Vtx ` G ) |
|
| numclwwlk.q | |- Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } ) |
||
| numclwwlk.h | |- H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } ) |
||
| Assertion | numclwwlk2lem3 | |- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( # ` ( X Q N ) ) = ( # ` ( X H ( N + 2 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | numclwwlk.v | |- V = ( Vtx ` G ) |
|
| 2 | numclwwlk.q | |- Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } ) |
|
| 3 | numclwwlk.h | |- H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } ) |
|
| 4 | ovexd | |- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( X H ( N + 2 ) ) e. _V ) |
|
| 5 | eqid | |- ( h e. ( X H ( N + 2 ) ) |-> ( h prefix ( N + 1 ) ) ) = ( h e. ( X H ( N + 2 ) ) |-> ( h prefix ( N + 1 ) ) ) |
|
| 6 | 1 2 3 5 | numclwlk2lem2f1o | |- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( h e. ( X H ( N + 2 ) ) |-> ( h prefix ( N + 1 ) ) ) : ( X H ( N + 2 ) ) -1-1-onto-> ( X Q N ) ) |
| 7 | 4 6 | hasheqf1od | |- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( # ` ( X H ( N + 2 ) ) ) = ( # ` ( X Q N ) ) ) |
| 8 | 7 | eqcomd | |- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( # ` ( X Q N ) ) = ( # ` ( X H ( N + 2 ) ) ) ) |