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 𝑉 = ( Vtx ‘ 𝐺 )
numclwwlk.q 𝑄 = ( 𝑣𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
numclwwlk.h 𝐻 = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
Assertion numclwwlk2lem3 ( ( 𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑋 𝑄 𝑁 ) ) = ( ♯ ‘ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk.v 𝑉 = ( Vtx ‘ 𝐺 )
2 numclwwlk.q 𝑄 = ( 𝑣𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
3 numclwwlk.h 𝐻 = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
4 ovexd ( ( 𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ ) → ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ∈ V )
5 eqid ( ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↦ ( prefix ( 𝑁 + 1 ) ) ) = ( ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↦ ( prefix ( 𝑁 + 1 ) ) )
6 1 2 3 5 numclwlk2lem2f1o ( ( 𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ ) → ( ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↦ ( prefix ( 𝑁 + 1 ) ) ) : ( 𝑋 𝐻 ( 𝑁 + 2 ) ) –1-1-onto→ ( 𝑋 𝑄 𝑁 ) )
7 4 6 hasheqf1od ( ( 𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) = ( ♯ ‘ ( 𝑋 𝑄 𝑁 ) ) )
8 7 eqcomd ( ( 𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑋 𝑄 𝑁 ) ) = ( ♯ ‘ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) )