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	bilani	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → ( Vtx ‘ 𝐺 ) ∈ Fin )
10	9	adantr	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( Vtx ‘ 𝐺 ) ∈ Fin )
11		wwlksnfi	⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WWalksN 𝐺 ) ∈ Fin )
12		rabfi	⊢ ( ( 𝑁 WWalksN 𝐺 ) ∈ Fin → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∈ Fin )
13	10 11 12	3syl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∈ Fin )
14	3	iswwlksnon	⊢ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) }
15		ancom	⊢ ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) ↔ ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
16	15	rabbii	⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
17	14 16	eqtri	⊢ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
18	17	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } )
19	2 18	eqtrid	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝐵 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } )
20		simpr	⊢ ( ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( 𝑤 ‘ 0 ) = 𝑋 )
21	20	a1i	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( 𝑤 ‘ 0 ) = 𝑋 ) )
22	21	ss2rabi	⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ⊆ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
23	19 22	eqsstrdi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ⊆ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
24	23	adantl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝐵 ⊆ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
25		hashssdif	⊢ ( ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∈ Fin ∧ 𝐵 ⊆ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) → ( ♯ ‘ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∖ 𝐵 ) ) = ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) − ( ♯ ‘ 𝐵 ) ) )
26	13 24 25	syl2anc	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∖ 𝐵 ) ) = ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) − ( ♯ ‘ 𝐵 ) ) )
27		simpl	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → 𝐺 RegUSGraph 𝐾 )
28	27	adantr	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝐺 RegUSGraph 𝐾 )
29		simpr	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → 𝑉 ∈ Fin )
30	29	adantr	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑉 ∈ Fin )
31		simpl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝑋 ∈ 𝑉 )
32	31	adantl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑋 ∈ 𝑉 )
33		simpr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
34	33	adantl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℕ0 )
35	3	rusgrnumwwlkg	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) = ( 𝐾 ↑ 𝑁 ) )
36	28 30 32 34 35	syl13anc	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) = ( 𝐾 ↑ 𝑁 ) )
37	36	oveq1d	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) − ( ♯ ‘ 𝐵 ) ) = ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ 𝐵 ) ) )
38	7 26 37	3eqtrd	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ 𝐴 ) = ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ 𝐵 ) ) )