Theorem clwlknon2num

Description: There are k walks of length 2 on each vertex X in a k-regular simple graph. Variant of clwwlknon2num , using the general definition of walks instead of walks as words. (Contributed by AV, 4-Jun-2022)

	Ref	Expression
Hypothesis	clwlknon2num.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	clwlknon2num	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		clwlknon2num.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		rusgrusgr	⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph )
3		usgruspgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
4	2 3	syl	⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USPGraph )
5	4	3ad2ant2	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝐺 ∈ USPGraph )
6	1	eleq2i	⊢ ( 𝑋 ∈ 𝑉 ↔ 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
7	6	biimpi	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
8	7	3ad2ant3	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
9		2nn	⊢ 2 ∈ ℕ
10	9	a1i	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 2 ∈ ℕ )
11		clwwlknonclwlknonen	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 2 ∈ ℕ ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ≈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) )
12	5 8 10 11	syl3anc	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ≈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) )
13	2	anim2i	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑉 ∈ Fin ∧ 𝐺 ∈ USGraph ) )
14	13	ancomd	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
15	1	isfusgr	⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
16	14 15	sylibr	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐺 ∈ FinUSGraph )
17	16	3adant3	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝐺 ∈ FinUSGraph )
18		2nn0	⊢ 2 ∈ ℕ0
19	18	a1i	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 2 ∈ ℕ0 )
20		wlksnfi	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 2 ∈ ℕ0 ) → { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 } ∈ Fin )
21	17 19 20	syl2anc	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 } ∈ Fin )
22		clwlkswks	⊢ ( ClWalks ‘ 𝐺 ) ⊆ ( Walks ‘ 𝐺 )
23	22	a1i	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ClWalks ‘ 𝐺 ) ⊆ ( Walks ‘ 𝐺 ) )
24		simp2l	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ∧ 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ) → ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 )
25	23 24	rabssrabd	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ⊆ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 } )
26	21 25	ssfid	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ∈ Fin )
27	1	clwwlknonfin	⊢ ( 𝑉 ∈ Fin → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ∈ Fin )
28	27	3ad2ant1	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ∈ Fin )
29		hashen	⊢ ( ( { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ∈ Fin ∧ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ∈ Fin ) → ( ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) ↔ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ≈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) )
30	26 28 29	syl2anc	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) ↔ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ≈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) )
31	12 30	mpbird	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) )
32	7	anim2i	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) )
33	32	3adant1	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) )
34		clwwlknon2num	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 )
35	33 34	syl	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 )
36	31 35	eqtrd	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 2 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = 𝐾 )