Theorem clwwlknon2num

Description: In a K-regular graph G , there are K closed walks on vertex X of length 2 . (Contributed by Alexander van der Vekens, 19-Sep-2018) (Revised by AV, 28-May-2021) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 25-Mar-2022)

	Ref	Expression
Assertion	clwwlknon2num	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ClWWalksNOn ‘ 𝐺 ) = ( ClWWalksNOn ‘ 𝐺 )
2		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4	1 2 3	clwwlknon2x	⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) = { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
5	4	a1i	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) = { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } )
6	5	fveq2d	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = ( ♯ ‘ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) )
7		3ancomb	⊢ ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
8	7	rabbii	⊢ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } = { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
9	8	fveq2i	⊢ ( ♯ ‘ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = ( ♯ ‘ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } )
10	2	rusgrnumwrdl2	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = 𝐾 )
11	9 10	eqtr3id	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) = 𝐾 )
12	6 11	eqtrd	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 )