Theorem clwwlknclwwlkdifnum

Description: In a K-regular graph, the size of the set A of walks of length N starting with a fixed vertex X and ending not at this vertex is the difference between K to the power of N and the size of the set B of closed walks of length N anchored at this vertex X . (Contributed by Alexander van der Vekens, 30-Sep-2018) (Revised by AV, 7-May-2021) (Revised by AV, 8-Mar-2022) (Proof shortened by AV, 16-Mar-2022)

	Ref	Expression
Hypotheses	clwwlknclwwlkdif.a	⊢ 𝐴 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) }
	clwwlknclwwlkdif.b	⊢ 𝐵 = ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 )
	clwwlknclwwlkdifnum.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	clwwlknclwwlkdifnum	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ 𝐴 ) = ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		clwwlknclwwlkdif.a	⊢ 𝐴 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) }
2		clwwlknclwwlkdif.b	⊢ 𝐵 = ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 )
3		clwwlknclwwlkdifnum.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4		eqid	⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
5	1 2 4	clwwlknclwwlkdif	⊢ 𝐴 = ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∖ 𝐵 )
6	5	fveq2i	⊢ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∖ 𝐵 ) )
7	6	a1i	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∖ 𝐵 ) ) )
8	3	eleq1i	⊢ ( 𝑉 ∈ Fin ↔ ( Vtx ‘ 𝐺 ) ∈ Fin )
9	8	biimpi	⊢ ( 𝑉 ∈ Fin → ( Vtx ‘ 𝐺 ) ∈ Fin )
10	9	adantl	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → ( Vtx ‘ 𝐺 ) ∈ Fin )
11	10	adantr	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( Vtx ‘ 𝐺 ) ∈ Fin )
12		wwlksnfi	⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WWalksN 𝐺 ) ∈ Fin )
13		rabfi	⊢ ( ( 𝑁 WWalksN 𝐺 ) ∈ Fin → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∈ Fin )
14	11 12 13	3syl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∈ Fin )
15	3	iswwlksnon	⊢ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) }
16		ancom	⊢ ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) ↔ ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
17	16	rabbii	⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
18	15 17	eqtri	⊢ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
19	18	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } )
20	2 19	syl5eq	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝐵 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } )
21		simpr	⊢ ( ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( 𝑤 ‘ 0 ) = 𝑋 )
22	21	a1i	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( 𝑤 ‘ 0 ) = 𝑋 ) )
23	22	ss2rabi	⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ⊆ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
24	20 23	eqsstrdi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ⊆ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
25	24	adantl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝐵 ⊆ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
26		hashssdif	⊢ ( ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∈ Fin ∧ 𝐵 ⊆ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) → ( ♯ ‘ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∖ 𝐵 ) ) = ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) − ( ♯ ‘ 𝐵 ) ) )
27	14 25 26	syl2anc	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∖ 𝐵 ) ) = ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) − ( ♯ ‘ 𝐵 ) ) )
28		simpl	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → 𝐺 RegUSGraph 𝐾 )
29	28	adantr	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝐺 RegUSGraph 𝐾 )
30		simpr	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → 𝑉 ∈ Fin )
31	30	adantr	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑉 ∈ Fin )
32		simpl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝑋 ∈ 𝑉 )
33	32	adantl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑋 ∈ 𝑉 )
34		simpr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
35	34	adantl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℕ0 )
36	3	rusgrnumwwlkg	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) = ( 𝐾 ↑ 𝑁 ) )
37	29 31 33 35 36	syl13anc	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) = ( 𝐾 ↑ 𝑁 ) )
38	37	oveq1d	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) − ( ♯ ‘ 𝐵 ) ) = ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ 𝐵 ) ) )
39	7 27 38	3eqtrd	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ 𝐴 ) = ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ 𝐵 ) ) )