Metamath Proof Explorer

Theorem numclwwlk2lem3

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∈V,n∈ℕ⟼w∈nWWalksNG|w⁡0=v∧lastS⁡w≠v
numclwwlk.h ⊢H=v∈V,n∈ℤ≥2⟼w∈vClWWalksNOn⁡Gn|w⁡n−2≠v
Assertion numclwwlk2lem3 ⊢G∈FriendGraph∧X∈V∧N∈ℕ→XQN=XHN+2

Proof

Step Hyp Ref Expression
1 numclwwlk.v ⊢V=Vtx⁡G
2 numclwwlk.q ⊢Q=v∈V,n∈ℕ⟼w∈nWWalksNG|w⁡0=v∧lastS⁡w≠v
3 numclwwlk.h ⊢H=v∈V,n∈ℤ≥2⟼w∈vClWWalksNOn⁡Gn|w⁡n−2≠v
4 ovexd ⊢G∈FriendGraph∧X∈V∧N∈ℕ→XHN+2∈V
5 eqid ⊢h∈XHN+2⟼hprefixN+1=h∈XHN+2⟼hprefixN+1
6 1 2 3 5 numclwlk2lem2f1o ⊢G∈FriendGraph∧X∈V∧N∈ℕ→h∈XHN+2⟼hprefixN+1:XHN+2⟶1-1 ontoXQN
7 4 6 hasheqf1od ⊢G∈FriendGraph∧X∈V∧N∈ℕ→XHN+2=XQN
8 7 eqcomd ⊢G∈FriendGraph∧X∈V∧N∈ℕ→XQN=XHN+2