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	$⊢ V = Vtx (G)$
	fusgreg2wsp.m	$⊢ M = (a \in V ⟼ \{w \in (2 WSPathsN G) \| w (1) = a\})$
Assertion	fusgreghash2wspv	$⊢ G \in FinUSGraph \to \forall v \in V (VtxDeg (G) (v) = K \to \|M (v)\| = K (K - 1))$

Proof

Step	Hyp	Ref	Expression
1		frgrhash2wsp.v	$⊢ V = Vtx (G)$
2		fusgreg2wsp.m	$⊢ M = (a \in V ⟼ \{w \in (2 WSPathsN G) \| w (1) = a\})$
3	1 2	fusgr2wsp2nb	$⊢ (G \in FinUSGraph \land v \in V) \to M (v) = ⋃_{c \in G NeighbVtx v} ⋃_{d \in (G NeighbVtx v) ∖ \{c\}} \{⟨“ c v d ”⟩\}$
4	3	fveq2d	$⊢ (G \in FinUSGraph \land v \in V) \to \|M (v)\| = \|⋃_{c \in G NeighbVtx v} ⋃_{d \in (G NeighbVtx v) ∖ \{c\}} \{⟨“ c v d ”⟩\}\|$
5	4	adantr	$⊢ ((G \in FinUSGraph \land v \in V) \land VtxDeg (G) (v) = K) \to \|M (v)\| = \|⋃_{c \in G NeighbVtx v} ⋃_{d \in (G NeighbVtx v) ∖ \{c\}} \{⟨“ c v d ”⟩\}\|$
6	1	eleq2i	$⊢ v \in V \leftrightarrow v \in Vtx (G)$
7		nbfiusgrfi	$⊢ (G \in FinUSGraph \land v \in Vtx (G)) \to G NeighbVtx v \in Fin$
8	6 7	sylan2b	$⊢ (G \in FinUSGraph \land v \in V) \to G NeighbVtx v \in Fin$
9	8	adantr	$⊢ ((G \in FinUSGraph \land v \in V) \land VtxDeg (G) (v) = K) \to G NeighbVtx v \in Fin$
10		eqid	$⊢ (G NeighbVtx v) ∖ \{c\} = (G NeighbVtx v) ∖ \{c\}$
11		snfi	$⊢ \{⟨“ c v d ”⟩\} \in Fin$
12	11	a1i	$⊢ (((G \in FinUSGraph \land v \in V) \land VtxDeg (G) (v) = K) \land c \in (G NeighbVtx v) \land d \in ((G NeighbVtx v) ∖ \{c\})) \to \{⟨“ c v d ”⟩\} \in Fin$
13	1	nbgrssvtx	$⊢ G NeighbVtx v \subseteq V$
14	13	a1i	$⊢ ((G \in FinUSGraph \land v \in V) \land c \in (G NeighbVtx v)) \to G NeighbVtx v \subseteq V$
15	14	ssdifd	$⊢ ((G \in FinUSGraph \land v \in V) \land c \in (G NeighbVtx v)) \to (G NeighbVtx v) ∖ \{c\} \subseteq V ∖ \{c\}$
16		iunss1	$⊢ (G NeighbVtx v) ∖ \{c\} \subseteq V ∖ \{c\} \to ⋃_{d \in (G NeighbVtx v) ∖ \{c\}} \{⟨“ c v d ”⟩\} \subseteq ⋃_{d \in V ∖ \{c\}} \{⟨“ c v d ”⟩\}$
17	15 16	syl	$⊢ ((G \in FinUSGraph \land v \in V) \land c \in (G NeighbVtx v)) \to ⋃_{d \in (G NeighbVtx v) ∖ \{c\}} \{⟨“ c v d ”⟩\} \subseteq ⋃_{d \in V ∖ \{c\}} \{⟨“ c v d ”⟩\}$
18	17	ralrimiva	$⊢ (G \in FinUSGraph \land v \in V) \to \forall c \in (G NeighbVtx v) ⋃_{d \in (G NeighbVtx v) ∖ \{c\}} \{⟨“ c v d ”⟩\} \subseteq ⋃_{d \in V ∖ \{c\}} \{⟨“ c v d ”⟩\}$
19		simpr	$⊢ (G \in FinUSGraph \land v \in V) \to v \in V$
20		s3iunsndisj	$⊢ v \in V \to \underset{c \in G NeighbVtx v}{Disj} ⋃_{d \in V ∖ \{c\}} \{⟨“ c v d ”⟩\}$
21	19 20	syl	$⊢ (G \in FinUSGraph \land v \in V) \to \underset{c \in G NeighbVtx v}{Disj} ⋃_{d \in V ∖ \{c\}} \{⟨“ c v d ”⟩\}$
22		disjss2	$⊢ \forall c \in (G NeighbVtx v) ⋃_{d \in (G NeighbVtx v) ∖ \{c\}} \{⟨“ c v d ”⟩\} \subseteq ⋃_{d \in V ∖ \{c\}} \{⟨“ c v d ”⟩\} \to (\underset{c \in G NeighbVtx v}{Disj} ⋃_{d \in V ∖ \{c\}} \{⟨“ c v d ”⟩\} \to \underset{c \in G NeighbVtx v}{Disj} ⋃_{d \in (G NeighbVtx v) ∖ \{c\}} \{⟨“ c v d ”⟩\})$
23	18 21 22	sylc	$⊢ (G \in FinUSGraph \land v \in V) \to \underset{c \in G NeighbVtx v}{Disj} ⋃_{d \in (G NeighbVtx v) ∖ \{c\}} \{⟨“ c v d ”⟩\}$
24	23	adantr	$⊢ ((G \in FinUSGraph \land v \in V) \land VtxDeg (G) (v) = K) \to \underset{c \in G NeighbVtx v}{Disj} ⋃_{d \in (G NeighbVtx v) ∖ \{c\}} \{⟨“ c v d ”⟩\}$
25	19	adantr	$⊢ ((G \in FinUSGraph \land v \in V) \land VtxDeg (G) (v) = K) \to v \in V$
26	25	anim1ci	$⊢ (((G \in FinUSGraph \land v \in V) \land VtxDeg (G) (v) = K) \land c \in (G NeighbVtx v)) \to (c \in (G NeighbVtx v) \land v \in V)$
27		s3sndisj	$⊢ (c \in (G NeighbVtx v) \land v \in V) \to \underset{d \in (G NeighbVtx v) ∖ \{c\}}{Disj} \{⟨“ c v d ”⟩\}$
28	26 27	syl	$⊢ (((G \in FinUSGraph \land v \in V) \land VtxDeg (G) (v) = K) \land c \in (G NeighbVtx v)) \to \underset{d \in (G NeighbVtx v) ∖ \{c\}}{Disj} \{⟨“ c v d ”⟩\}$
29		s3cli	$⊢ ⟨“ c v d ”⟩ \in Word V$
30		hashsng	$⊢ ⟨“ c v d ”⟩ \in Word V \to \|\{⟨“ c v d ”⟩\}\| = 1$
31	29 30	mp1i	$⊢ (((G \in FinUSGraph \land v \in V) \land VtxDeg (G) (v) = K) \land c \in (G NeighbVtx v) \land d \in ((G NeighbVtx v) ∖ \{c\})) \to \|\{⟨“ c v d ”⟩\}\| = 1$
32	9 10 12 24 28 31	hash2iun1dif1	$⊢ ((G \in FinUSGraph \land v \in V) \land VtxDeg (G) (v) = K) \to \|⋃_{c \in G NeighbVtx v} ⋃_{d \in (G NeighbVtx v) ∖ \{c\}} \{⟨“ c v d ”⟩\}\| = \|G NeighbVtx v\| (\|G NeighbVtx v\| - 1)$
33		fusgrusgr	$⊢ G \in FinUSGraph \to G \in USGraph$
34	1	hashnbusgrvd	$⊢ (G \in USGraph \land v \in V) \to \|G NeighbVtx v\| = VtxDeg (G) (v)$
35	33 34	sylan	$⊢ (G \in FinUSGraph \land v \in V) \to \|G NeighbVtx v\| = VtxDeg (G) (v)$
36		id	$⊢ \|G NeighbVtx v\| = VtxDeg (G) (v) \to \|G NeighbVtx v\| = VtxDeg (G) (v)$
37		oveq1	$⊢ \|G NeighbVtx v\| = VtxDeg (G) (v) \to \|G NeighbVtx v\| - 1 = VtxDeg (G) (v) - 1$
38	36 37	oveq12d	$⊢ \|G NeighbVtx v\| = VtxDeg (G) (v) \to \|G NeighbVtx v\| (\|G NeighbVtx v\| - 1) = VtxDeg (G) (v) (VtxDeg (G) (v) - 1)$
39	35 38	syl	$⊢ (G \in FinUSGraph \land v \in V) \to \|G NeighbVtx v\| (\|G NeighbVtx v\| - 1) = VtxDeg (G) (v) (VtxDeg (G) (v) - 1)$
40		id	$⊢ VtxDeg (G) (v) = K \to VtxDeg (G) (v) = K$
41		oveq1	$⊢ VtxDeg (G) (v) = K \to VtxDeg (G) (v) - 1 = K - 1$
42	40 41	oveq12d	$⊢ VtxDeg (G) (v) = K \to VtxDeg (G) (v) (VtxDeg (G) (v) - 1) = K (K - 1)$
43	39 42	sylan9eq	$⊢ ((G \in FinUSGraph \land v \in V) \land VtxDeg (G) (v) = K) \to \|G NeighbVtx v\| (\|G NeighbVtx v\| - 1) = K (K - 1)$
44	5 32 43	3eqtrd	$⊢ ((G \in FinUSGraph \land v \in V) \land VtxDeg (G) (v) = K) \to \|M (v)\| = K (K - 1)$
45	44	ex	$⊢ (G \in FinUSGraph \land v \in V) \to (VtxDeg (G) (v) = K \to \|M (v)\| = K (K - 1))$
46	45	ralrimiva	$⊢ G \in FinUSGraph \to \forall v \in V (VtxDeg (G) (v) = K \to \|M (v)\| = K (K - 1))$

Metamath Proof Explorer

Theorem fusgreghash2wspv

Proof