Metamath Proof Explorer

Theorem numclwlk1lem2

Description: Lemma 2 for numclwlk1 (Statement 9 in Huneke p. 2 for n>2). This theorem corresponds to numclwwlk1 , using the general definition of walks instead of walks as words. (Contributed by AV, 4-Jun-2022)

Ref Expression
Hypotheses numclwlk1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
numclwlk1.c ⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
numclwlk1.f ⊢ 𝐹 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) }
Assertion numclwlk1lem2 ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 numclwlk1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 numclwlk1.c ⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
3 numclwlk1.f ⊢ 𝐹 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) }
4 rusgrusgr ⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph )
5 usgruspgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
6 4 5 syl ⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USPGraph )
7 6 ad2antlr ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝐺 ∈ USPGraph )
8 simpl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑋 ∈ 𝑉 )
9 8 adantl ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝑋 ∈ 𝑉 )
10 uzuzle23 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
11 10 ad2antll ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
12 eqid ⊢ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 }
13 1 2 12 dlwwlknondlwlknonen ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐶 ≈ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
14 7 9 11 13 syl3anc ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝐶 ≈ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
15 4 anim2i ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑉 ∈ Fin ∧ 𝐺 ∈ USGraph ) )
16 15 ancomd ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
17 1 isfusgr ⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
18 16 17 sylibr ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐺 ∈ FinUSGraph )
19 eluzge3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
20 19 nnnn0d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ0 )
21 20 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑁 ∈ ℕ0 )
22 wlksnfi ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0 ) → { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } ∈ Fin )
23 18 21 22 syl2an ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } ∈ Fin )
24 clwlkswks ⊢ ( ClWalks ‘ 𝐺 ) ⊆ ( Walks ‘ 𝐺 )
25 24 a1i ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ClWalks ‘ 𝐺 ) ⊆ ( Walks ‘ 𝐺 ) )
26 simp21 ⊢ ( ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ) → ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 )
27 25 26 rabssrabd ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } ⊆ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } )
28 23 27 ssfid ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } ∈ Fin )
29 2 28 eqeltrid ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝐶 ∈ Fin )
30 1 clwwlknonfin ⊢ ( 𝑉 ∈ Fin → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin )
31 30 ad2antrr ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin )
32 ssrab2 ⊢ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ⊆ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 )
33 32 a1i ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ⊆ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
34 31 33 ssfid ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ∈ Fin )
35 hashen ⊢ ( ( 𝐶 ∈ Fin ∧ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ∈ Fin ) → ( ( ♯ ‘ 𝐶 ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) ↔ 𝐶 ≈ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) )
36 29 34 35 syl2anc ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( ♯ ‘ 𝐶 ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) ↔ 𝐶 ≈ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) )
37 14 36 mpbird ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ 𝐶 ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) )
38 eqidd ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) )
39 oveq12 ⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
40 fvoveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑤 ‘ ( 𝑛 − 2 ) ) = ( 𝑤 ‘ ( 𝑁 − 2 ) ) )
41 40 adantl ⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → ( 𝑤 ‘ ( 𝑛 − 2 ) ) = ( 𝑤 ‘ ( 𝑁 − 2 ) ) )
42 simpl ⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → 𝑣 = 𝑋 )
43 41 42 eqeq12d ⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → ( ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 ↔ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
44 39 43 rabeqbidv ⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
45 44 adantl ⊢ ( ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) ) → { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
46 ovex ⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ V
47 46 rabex ⊢ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ∈ V
48 47 a1i ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ∈ V )
49 38 45 9 11 48 ovmpod ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑋 ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
50 49 fveq2d ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) 𝑁 ) ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) )
51 eqid ⊢ ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
52 eqid ⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
53 1 51 52 numclwwlk1 ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) 𝑁 ) ) = ( 𝐾 · ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) )
54 8 1 eleqtrdi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
55 54 adantl ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
56 uz3m2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℕ )
57 56 ad2antll ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑁 − 2 ) ∈ ℕ )
58 clwwlknonclwlknonen ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 − 2 ) ∈ ℕ ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ≈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) )
59 7 55 57 58 syl3anc ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ≈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) )
60 3 59 eqbrtrid ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝐹 ≈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) )
61 uznn0sub ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 2 ) ∈ ℕ0 )
62 10 61 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℕ0 )
63 62 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 − 2 ) ∈ ℕ0 )
64 wlksnfi ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ ( 𝑁 − 2 ) ∈ ℕ0 ) → { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) } ∈ Fin )
65 18 63 64 syl2an ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) } ∈ Fin )
66 simp2l ⊢ ( ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ∧ 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ) → ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) )
67 25 66 rabssrabd ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ⊆ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) } )
68 65 67 ssfid ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ∈ Fin )
69 3 68 eqeltrid ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝐹 ∈ Fin )
70 1 clwwlknonfin ⊢ ( 𝑉 ∈ Fin → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∈ Fin )
71 70 ad2antrr ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∈ Fin )
72 hashen ⊢ ( ( 𝐹 ∈ Fin ∧ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∈ Fin ) → ( ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ↔ 𝐹 ≈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) )
73 69 71 72 syl2anc ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ↔ 𝐹 ≈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) )
74 60 73 mpbird ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) )
75 74 eqcomd ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) = ( ♯ ‘ 𝐹 ) )
76 75 oveq2d ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝐾 · ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )
77 53 76 eqtrd ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) 𝑁 ) ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )
78 37 50 77 3eqtr2d ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )