Theorem rusgrnumwrdl2

Description: In a k-regular simple graph, the number of edges resp. walks of length 1 (represented as words of length 2) starting at a fixed vertex is k. (Contributed by Alexander van der Vekens, 28-Jul-2018) (Revised by AV, 6-May-2021)

	Ref	Expression
Hypothesis	rusgrnumwrdl2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	rusgrnumwrdl2	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwrdl2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	fvexi	⊢ 𝑉 ∈ V
3	2	wrdexi	⊢ Word 𝑉 ∈ V
4	3	rabex	⊢ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } ∈ V
5	2	a1i	⊢ ( 𝐺 RegUSGraph 𝐾 → 𝑉 ∈ V )
6		wrd2f1tovbij	⊢ ( ( 𝑉 ∈ V ∧ 𝑃 ∈ 𝑉 ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } –1-1-onto→ { 𝑠 ∈ 𝑉 ∣ { 𝑃 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } )
7	5 6	sylan	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } –1-1-onto→ { 𝑠 ∈ 𝑉 ∣ { 𝑃 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } )
8		hasheqf1oi	⊢ ( { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } ∈ V → ( ∃ 𝑓 𝑓 : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } –1-1-onto→ { 𝑠 ∈ 𝑉 ∣ { 𝑃 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = ( ♯ ‘ { 𝑠 ∈ 𝑉 ∣ { 𝑃 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } ) ) )
9	4 7 8	mpsyl	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = ( ♯ ‘ { 𝑠 ∈ 𝑉 ∣ { 𝑃 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } ) )
10	1	rusgrpropadjvtx	⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑝 ∈ 𝑉 ( ♯ ‘ { 𝑠 ∈ 𝑉 ∣ { 𝑝 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) )
11		preq1	⊢ ( 𝑝 = 𝑃 → { 𝑝 , 𝑠 } = { 𝑃 , 𝑠 } )
12	11	eleq1d	⊢ ( 𝑝 = 𝑃 → ( { 𝑝 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑃 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) ) )
13	12	rabbidv	⊢ ( 𝑝 = 𝑃 → { 𝑠 ∈ 𝑉 ∣ { 𝑝 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } = { 𝑠 ∈ 𝑉 ∣ { 𝑃 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } )
14	13	fveqeq2d	⊢ ( 𝑝 = 𝑃 → ( ( ♯ ‘ { 𝑠 ∈ 𝑉 ∣ { 𝑝 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ↔ ( ♯ ‘ { 𝑠 ∈ 𝑉 ∣ { 𝑃 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) )
15	14	rspccv	⊢ ( ∀ 𝑝 ∈ 𝑉 ( ♯ ‘ { 𝑠 ∈ 𝑉 ∣ { 𝑝 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 → ( 𝑃 ∈ 𝑉 → ( ♯ ‘ { 𝑠 ∈ 𝑉 ∣ { 𝑃 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) )
16	15	3ad2ant3	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑝 ∈ 𝑉 ( ♯ ‘ { 𝑠 ∈ 𝑉 ∣ { 𝑝 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) → ( 𝑃 ∈ 𝑉 → ( ♯ ‘ { 𝑠 ∈ 𝑉 ∣ { 𝑃 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) )
17	10 16	syl	⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝑃 ∈ 𝑉 → ( ♯ ‘ { 𝑠 ∈ 𝑉 ∣ { 𝑃 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) )
18	17	imp	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ♯ ‘ { 𝑠 ∈ 𝑉 ∣ { 𝑃 , 𝑠 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 )
19	9 18	eqtrd	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = 𝐾 )