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

Proof

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