Metamath Proof Explorer

Theorem numclwwlk3lem2

Description: Lemma 1 for numclwwlk3 : The number of closed vertices of a fixed length N on a fixed vertex V is the sum of the number of closed walks of length N at V with the last but one vertex being V and the set of closed walks of length N at V with the last but one vertex not being V . (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 1-Jun-2021) (Revised by AV, 1-May-2022)

Ref Expression
Hypotheses numclwwlk3lem2.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
numclwwlk3lem2.h ⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
Assertion numclwwlk3lem2 ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = ( ( ♯ ‘ ( 𝑋 𝐻 𝑁 ) ) + ( ♯ ‘ ( 𝑋 𝐶 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk3lem2.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
2 numclwwlk3lem2.h ⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
3 1 2 numclwwlk3lem2lem ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ( ( 𝑋 𝐻 𝑁 ) ∪ ( 𝑋 𝐶 𝑁 ) ) )
4 3 adantll ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ( ( 𝑋 𝐻 𝑁 ) ∪ ( 𝑋 𝐶 𝑁 ) ) )
5 4 fveq2d ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = ( ♯ ‘ ( ( 𝑋 𝐻 𝑁 ) ∪ ( 𝑋 𝐶 𝑁 ) ) ) )
6 2 numclwwlkovh0 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐻 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } )
7 6 adantll ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐻 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } )
8 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
9 8 fusgrvtxfi ⊢ ( 𝐺 ∈ FinUSGraph → ( Vtx ‘ 𝐺 ) ∈ Fin )
10 9 ad2antrr ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( Vtx ‘ 𝐺 ) ∈ Fin )
11 8 clwwlknonfin ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin )
12 rabfi ⊢ ( ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin → { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } ∈ Fin )
13 10 11 12 3syl ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } ∈ Fin )
14 7 13 eqeltrd ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐻 𝑁 ) ∈ Fin )
15 1 2clwwlk ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
16 15 adantll ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
17 rabfi ⊢ ( ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin → { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ∈ Fin )
18 10 11 17 3syl ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ∈ Fin )
19 16 18 eqeltrd ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐶 𝑁 ) ∈ Fin )
20 7 16 ineq12d ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑋 𝐻 𝑁 ) ∩ ( 𝑋 𝐶 𝑁 ) ) = ( { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } ∩ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) )
21 inrab ⊢ ( { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } ∩ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
22 exmid ⊢ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ∨ ¬ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 )
23 ianor ⊢ ( ¬ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ¬ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∨ ¬ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
24 nne ⊢ ( ¬ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ↔ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 )
25 24 orbi1i ⊢ ( ( ¬ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∨ ¬ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ∨ ¬ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
26 23 25 bitri ⊢ ( ¬ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ∨ ¬ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
27 22 26 mpbir ⊢ ¬ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 )
28 27 rgenw ⊢ ∀ 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ¬ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 )
29 rabeq0 ⊢ ( { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } = ∅ ↔ ∀ 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ¬ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
30 28 29 mpbir ⊢ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } = ∅
31 21 30 eqtri ⊢ ( { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } ∩ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) = ∅
32 20 31 eqtrdi ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑋 𝐻 𝑁 ) ∩ ( 𝑋 𝐶 𝑁 ) ) = ∅ )
33 hashun ⊢ ( ( ( 𝑋 𝐻 𝑁 ) ∈ Fin ∧ ( 𝑋 𝐶 𝑁 ) ∈ Fin ∧ ( ( 𝑋 𝐻 𝑁 ) ∩ ( 𝑋 𝐶 𝑁 ) ) = ∅ ) → ( ♯ ‘ ( ( 𝑋 𝐻 𝑁 ) ∪ ( 𝑋 𝐶 𝑁 ) ) ) = ( ( ♯ ‘ ( 𝑋 𝐻 𝑁 ) ) + ( ♯ ‘ ( 𝑋 𝐶 𝑁 ) ) ) )
34 14 19 32 33 syl3anc ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ♯ ‘ ( ( 𝑋 𝐻 𝑁 ) ∪ ( 𝑋 𝐶 𝑁 ) ) ) = ( ( ♯ ‘ ( 𝑋 𝐻 𝑁 ) ) + ( ♯ ‘ ( 𝑋 𝐶 𝑁 ) ) ) )
35 5 34 eqtrd ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = ( ( ♯ ‘ ( 𝑋 𝐻 𝑁 ) ) + ( ♯ ‘ ( 𝑋 𝐶 𝑁 ) ) ) )