fusgreghash2wsp

Description: In a finite k-regular graph with N vertices there are N times "k choose 2" paths with length 2, according to statement 8 in Huneke p. 2: "... giving n * ( k 2 ) total paths of length two.", if the direction of traversing the path is not respected. For simple paths of length 2 represented by length 3 strings, however, we have again n*k*(k-1) such paths. (Contributed by Alexander van der Vekens, 11-Mar-2018) (Revised by AV, 19-May-2021) (Proof shortened by AV, 12-Jan-2022)

		Ref	Expression
	Hypothesis	fusgreghash2wsp.v	$⊢ V = Vtx (G)$
	Assertion	fusgreghash2wsp	$⊢ (G \in FinUSGraph \land V \neq \emptyset) \to (\forall v \in V VtxDeg (G) (v) = K \to \|2 WSPathsN G\| = \|V\| K (K - 1))$

Proof

Step	Hyp	Ref	Expression
1		fusgreghash2wsp.v	$⊢ V = Vtx (G)$
2		fveq1	$⊢ s = t \to s (1) = t (1)$
3	2	eqeq1d	$⊢ s = t \to (s (1) = a \leftrightarrow t (1) = a)$
4	3	cbvrabv	$⊢ \{s \in (2 WSPathsN G) \| s (1) = a\} = \{t \in (2 WSPathsN G) \| t (1) = a\}$
5	4	mpteq2i	$⊢ (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) = (a \in V ⟼ \{t \in (2 WSPathsN G) \| t (1) = a\})$
6	1 5	fusgreg2wsp	$⊢ G \in FinUSGraph \to 2 WSPathsN G = ⋃_{y \in V} (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)$
7	6	ad2antrr	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V VtxDeg (G) (v) = K) \to 2 WSPathsN G = ⋃_{y \in V} (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)$
8	7	fveq2d	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V VtxDeg (G) (v) = K) \to \|2 WSPathsN G\| = \|⋃_{y \in V} (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)\|$
9	1	fusgrvtxfi	$⊢ G \in FinUSGraph \to V \in Fin$
10		eqeq2	$⊢ a = y \to (s (1) = a \leftrightarrow s (1) = y)$
11	10	rabbidv	$⊢ a = y \to \{s \in (2 WSPathsN G) \| s (1) = a\} = \{s \in (2 WSPathsN G) \| s (1) = y\}$
12		eqid	$⊢ (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) = (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\})$
13		ovex	$⊢ 2 WSPathsN G \in V$
14	13	rabex	$⊢ \{s \in (2 WSPathsN G) \| s (1) = y\} \in V$
15	11 12 14	fvmpt	$⊢ y \in V \to (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y) = \{s \in (2 WSPathsN G) \| s (1) = y\}$
16	15	adantl	$⊢ (G \in FinUSGraph \land y \in V) \to (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y) = \{s \in (2 WSPathsN G) \| s (1) = y\}$
17		eqid	$⊢ Vtx (G) = Vtx (G)$
18	17	fusgrvtxfi	$⊢ G \in FinUSGraph \to Vtx (G) \in Fin$
19		wspthnfi	$⊢ Vtx (G) \in Fin \to 2 WSPathsN G \in Fin$
20		rabfi	$⊢ 2 WSPathsN G \in Fin \to \{s \in (2 WSPathsN G) \| s (1) = y\} \in Fin$
21	18 19 20	3syl	$⊢ G \in FinUSGraph \to \{s \in (2 WSPathsN G) \| s (1) = y\} \in Fin$
22	21	adantr	$⊢ (G \in FinUSGraph \land y \in V) \to \{s \in (2 WSPathsN G) \| s (1) = y\} \in Fin$
23	16 22	eqeltrd	$⊢ (G \in FinUSGraph \land y \in V) \to (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y) \in Fin$
24	1 5	2wspmdisj	$⊢ \underset{y \in V}{Disj} (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)$
25	24	a1i	$⊢ G \in FinUSGraph \to \underset{y \in V}{Disj} (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)$
26	9 23 25	hashiun	$⊢ G \in FinUSGraph \to \|⋃_{y \in V} (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)\| = \sum_{y \in V} \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)\|$
27	26	ad2antrr	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V VtxDeg (G) (v) = K) \to \|⋃_{y \in V} (a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)\| = \sum_{y \in V} \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)\|$
28	1 5	fusgreghash2wspv	$⊢ G \in FinUSGraph \to \forall v \in V (VtxDeg (G) (v) = K \to \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (v)\| = K (K - 1))$
29		ralim	$⊢ \forall v \in V (VtxDeg (G) (v) = K \to \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (v)\| = K (K - 1)) \to (\forall v \in V VtxDeg (G) (v) = K \to \forall v \in V \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (v)\| = K (K - 1))$
30	28 29	syl	$⊢ G \in FinUSGraph \to (\forall v \in V VtxDeg (G) (v) = K \to \forall v \in V \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (v)\| = K (K - 1))$
31	30	adantr	$⊢ (G \in FinUSGraph \land V \neq \emptyset) \to (\forall v \in V VtxDeg (G) (v) = K \to \forall v \in V \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (v)\| = K (K - 1))$
32	31	imp	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V VtxDeg (G) (v) = K) \to \forall v \in V \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (v)\| = K (K - 1)$
33		2fveq3	$⊢ v = y \to \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (v)\| = \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)\|$
34	33	eqeq1d	$⊢ v = y \to (\|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (v)\| = K (K - 1) \leftrightarrow \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)\| = K (K - 1))$
35	34	rspccva	$⊢ (\forall v \in V \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (v)\| = K (K - 1) \land y \in V) \to \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)\| = K (K - 1)$
36	32 35	sylan	$⊢ (((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V VtxDeg (G) (v) = K) \land y \in V) \to \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)\| = K (K - 1)$
37	36	sumeq2dv	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V VtxDeg (G) (v) = K) \to \sum_{y \in V} \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)\| = \sum_{y \in V} K (K - 1)$
38	9	adantr	$⊢ (G \in FinUSGraph \land V \neq \emptyset) \to V \in Fin$
39		eqid	$⊢ VtxDeg (G) = VtxDeg (G)$
40	1 39	fusgrregdegfi	$⊢ (G \in FinUSGraph \land V \neq \emptyset) \to (\forall v \in V VtxDeg (G) (v) = K \to K \in ℕ_{0})$
41	40	imp	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V VtxDeg (G) (v) = K) \to K \in ℕ_{0}$
42	41	nn0cnd	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V VtxDeg (G) (v) = K) \to K \in ℂ$
43		kcnktkm1cn	$⊢ K \in ℂ \to K (K - 1) \in ℂ$
44	42 43	syl	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V VtxDeg (G) (v) = K) \to K (K - 1) \in ℂ$
45		fsumconst	$⊢ (V \in Fin \land K (K - 1) \in ℂ) \to \sum_{y \in V} K (K - 1) = \|V\| K (K - 1)$
46	38 44 45	syl2an2r	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V VtxDeg (G) (v) = K) \to \sum_{y \in V} K (K - 1) = \|V\| K (K - 1)$
47	37 46	eqtrd	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V VtxDeg (G) (v) = K) \to \sum_{y \in V} \|(a \in V ⟼ \{s \in (2 WSPathsN G) \| s (1) = a\}) (y)\| = \|V\| K (K - 1)$
48	8 27 47	3eqtrd	$⊢ ((G \in FinUSGraph \land V \neq \emptyset) \land \forall v \in V VtxDeg (G) (v) = K) \to \|2 WSPathsN G\| = \|V\| K (K - 1)$
49	48	ex	$⊢ (G \in FinUSGraph \land V \neq \emptyset) \to (\forall v \in V VtxDeg (G) (v) = K \to \|2 WSPathsN G\| = \|V\| K (K - 1))$

Metamath Proof Explorer

Theorem fusgreghash2wsp

Proof