Theorem fusgreghash2wspv

Description: According to statement 7 in Huneke p. 2: "For each vertex v, there are exactly ( k 2 ) paths with length two having v in the middle, ..." in a finite k-regular graph. For directed simple paths of length 2 represented by length 3 strings, we have again k*(k-1) such paths, see also comment of frgrhash2wsp . (Contributed by Alexander van der Vekens, 10-Mar-2018) (Revised by AV, 17-May-2021) (Proof shortened by AV, 12-Feb-2022)

	Ref	Expression
Hypotheses	frgrhash2wsp.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	fusgreg2wsp.m	⊢ 𝑀 = ( 𝑎 ∈ 𝑉 ↦ { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑎 } )
Assertion	fusgreghash2wspv	⊢ ( 𝐺 ∈ FinUSGraph → ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( 𝑀 ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		frgrhash2wsp.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fusgreg2wsp.m	⊢ 𝑀 = ( 𝑎 ∈ 𝑉 ↦ { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑎 } )
3	1 2	fusgr2wsp2nb	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) → ( 𝑀 ‘ 𝑣 ) = ∪ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∪ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } )
4	3	fveq2d	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) → ( ♯ ‘ ( 𝑀 ‘ 𝑣 ) ) = ( ♯ ‘ ∪ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∪ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } ) )
5	4	adantr	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ♯ ‘ ( 𝑀 ‘ 𝑣 ) ) = ( ♯ ‘ ∪ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∪ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } ) )
6	1	eleq2i	⊢ ( 𝑣 ∈ 𝑉 ↔ 𝑣 ∈ ( Vtx ‘ 𝐺 ) )
7		nbfiusgrfi	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 NeighbVtx 𝑣 ) ∈ Fin )
8	6 7	sylan2b	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑣 ) ∈ Fin )
9	8	adantr	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 𝐺 NeighbVtx 𝑣 ) ∈ Fin )
10		eqid	⊢ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) = ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } )
11		snfi	⊢ { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } ∈ Fin
12	11	a1i	⊢ ( ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) ∧ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∧ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) ) → { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } ∈ Fin )
13	1	nbgrssvtx	⊢ ( 𝐺 NeighbVtx 𝑣 ) ⊆ 𝑉
14	13	a1i	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) → ( 𝐺 NeighbVtx 𝑣 ) ⊆ 𝑉 )
15	14	ssdifd	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) → ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) ⊆ ( 𝑉 ∖ { 𝑐 } ) )
16		iunss1	⊢ ( ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) ⊆ ( 𝑉 ∖ { 𝑐 } ) → ∪ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } ⊆ ∪ 𝑑 ∈ ( 𝑉 ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } )
17	15 16	syl	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) → ∪ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } ⊆ ∪ 𝑑 ∈ ( 𝑉 ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } )
18	17	ralrimiva	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) → ∀ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∪ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } ⊆ ∪ 𝑑 ∈ ( 𝑉 ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } )
19		simpr	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
20		s3iunsndisj	⊢ ( 𝑣 ∈ 𝑉 → Disj 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∪ 𝑑 ∈ ( 𝑉 ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } )
21	19 20	syl	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) → Disj 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∪ 𝑑 ∈ ( 𝑉 ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } )
22		disjss2	⊢ ( ∀ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∪ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } ⊆ ∪ 𝑑 ∈ ( 𝑉 ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } → ( Disj 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∪ 𝑑 ∈ ( 𝑉 ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } → Disj 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∪ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } ) )
23	18 21 22	sylc	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) → Disj 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∪ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } )
24	23	adantr	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → Disj 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∪ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } )
25	19	adantr	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → 𝑣 ∈ 𝑉 )
26	25	anim1ci	⊢ ( ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) ∧ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) → ( 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∧ 𝑣 ∈ 𝑉 ) )
27		s3sndisj	⊢ ( ( 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∧ 𝑣 ∈ 𝑉 ) → Disj 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } )
28	26 27	syl	⊢ ( ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) ∧ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) → Disj 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } )
29		s3cli	⊢ ⟨“ 𝑐 𝑣 𝑑 ”⟩ ∈ Word V
30		hashsng	⊢ ( ⟨“ 𝑐 𝑣 𝑑 ”⟩ ∈ Word V → ( ♯ ‘ { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } ) = 1 )
31	29 30	mp1i	⊢ ( ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) ∧ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∧ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) ) → ( ♯ ‘ { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } ) = 1 )
32	9 10 12 24 28 31	hash2iun1dif1	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ♯ ‘ ∪ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑣 ) ∪ 𝑑 ∈ ( ( 𝐺 NeighbVtx 𝑣 ) ∖ { 𝑐 } ) { ⟨“ 𝑐 𝑣 𝑑 ”⟩ } ) = ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) · ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) − 1 ) ) )
33		fusgrusgr	⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
34	1	hashnbusgrvd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) )
35	33 34	sylan	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) )
36		id	⊢ ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) )
37		oveq1	⊢ ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) − 1 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) − 1 ) )
38	36 37	oveq12d	⊢ ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) · ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) − 1 ) ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) · ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) − 1 ) ) )
39	35 38	syl	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) · ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) − 1 ) ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) · ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) − 1 ) ) )
40		id	⊢ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 )
41		oveq1	⊢ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) − 1 ) = ( 𝐾 − 1 ) )
42	40 41	oveq12d	⊢ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) · ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) − 1 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) )
43	39 42	sylan9eq	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) · ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) − 1 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) )
44	5 32 43	3eqtrd	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ♯ ‘ ( 𝑀 ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) )
45	44	ex	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( 𝑀 ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) )
46	45	ralrimiva	⊢ ( 𝐺 ∈ FinUSGraph → ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( 𝑀 ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) )