Metamath Proof Explorer

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 ) ) ) )