Theorem fusgreghash2wspv 30629

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 30626. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 12-Feb-2022.)

Hypotheses

Ref	Expression
frgrhash2wsp.v	⊢ 𝑉 = (Vtx‘𝐺)
fusgreg2wsp.m	⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})

Assertion

Ref	Expression
fusgreghash2wspv	⊢ (𝐺 ∈ FinUSGraph → ∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (♯‘(𝑀‘𝑣)) = (𝐾 · (𝐾 − 1))))

Distinct variable groups:   𝐺,𝑎   𝑉,𝑎   𝑤,𝐺,𝑎,𝑣

Allowed substitution hints:   𝐾(𝑤,𝑣,𝑎)   𝑀(𝑤,𝑣,𝑎)   𝑉(𝑤,𝑣)

Proof of Theorem fusgreghash2wspv

Dummy variables 𝑐 𝑑 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  ∀wral 3085  {crab 3423  Vcvv 3463   ∖ cdif 3910   ⊆ wss 3913  {csn 4594  ∪ ciun 4960  Disj wdisj 5080   ↦ cmpt 5196  ‘cfv 6539  (class class class)co 7413  Fincfn 8945  1c1 11103   · cmul 11107   − cmin 11443  2c2 12297  ♯chash 14368  Word cword 14552  ⟨“cs3 14881  Vtxcvtx 29289  USGraphcusgr 29442  FinUSGraphcfusgr 29609   NeighbVtx cnbgr 29625  VtxDegcvtxdg 29758   WSPathsN cwwspthsn 30120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5273  ax-pow 5339  ax-pr 5407  ax-un 7735  ax-inf2 9612  ax-cnex 11158  ax-resscn 11159  ax-1cn 11160  ax-icn 11161  ax-addcl 11162  ax-addrcl 11163  ax-mulcl 11164  ax-mulrcl 11165  ax-mulcom 11166  ax-addass 11167  ax-mulass 11168  ax-distr 11169  ax-i2m1 11170  ax-1ne0 11171  ax-1rid 11172  ax-rnegex 11173  ax-rrecex 11174  ax-cnre 11175  ax-pre-lttri 11176  ax-pre-lttrn 11177  ax-pre-ltadd 11178  ax-pre-mulgt0 11179  ax-pre-sup 11180

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ifp 1077  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-disj 5081  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-se 5618  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6305  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6495  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-isom 6548  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7865  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-oadd 8459  df-er 8696  df-map 8828  df-pm 8829  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-sup 9404  df-oi 9474  df-dju 9889  df-card 9927  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11445  df-neg 11446  df-div 11874  df-nn 12236  df-2 12305  df-3 12306  df-n0 12507  df-xnn0 12580  df-z 12594  df-uz 12865  df-rp 13019  df-xadd 13140  df-fz 13538  df-fzo 13685  df-seq 14040  df-exp 14100  df-hash 14369  df-word 14553  df-concat 14610  df-s1 14636  df-s2 14887  df-s3 14888  df-cj 15152  df-re 15153  df-im 15154  df-sqrt 15288  df-abs 15289  df-clim 15541  df-sum 15740  df-vtx 29291  df-iedg 29292  df-edg 29341  df-uhgr 29351  df-ushgr 29352  df-upgr 29375  df-umgr 29376  df-uspgr 29443  df-usgr 29444  df-fusgr 29610  df-nbgr 29626  df-vtxdg 29759  df-wlks 29892  df-wlkson 29893  df-trls 29983  df-trlson 29984  df-pths 30006  df-spths 30007  df-pthson 30008  df-spthson 30009  df-wwlks 30122  df-wwlksn 30123  df-wwlksnon 30124  df-wspthsn 30125  df-wspthsnon 30126

This theorem is referenced by:  fusgreghash2wsp  30632