clwwlknun

Description: The set of closed walks of fixed length N in a simple graph G is the union of the closed walks of the fixed length N on each of the vertices of graph G . (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 28-May-2021) (Revised by AV, 3-Mar-2022) (Proof shortened by AV, 28-Mar-2022)

		Ref	Expression
	Hypothesis	clwwlknun.v	$⊢ V = Vtx (G)$
	Assertion	clwwlknun	$⊢ G \in USGraph \to N ClWWalksN G = ⋃_{x \in V} (x ClWWalksNOn (G) N)$

Proof

Step	Hyp	Ref	Expression
1		clwwlknun.v	$⊢ V = Vtx (G)$
2		eliun	$⊢ y \in ⋃_{x \in V} (x ClWWalksNOn (G) N) \leftrightarrow \exists x \in V y \in (x ClWWalksNOn (G) N)$
3		isclwwlknon	$⊢ y \in (x ClWWalksNOn (G) N) \leftrightarrow (y \in (N ClWWalksN G) \land y (0) = x)$
4	3	rexbii	$⊢ \exists x \in V y \in (x ClWWalksNOn (G) N) \leftrightarrow \exists x \in V (y \in (N ClWWalksN G) \land y (0) = x)$
5		simpl	$⊢ (y \in (N ClWWalksN G) \land y (0) = x) \to y \in (N ClWWalksN G)$
6	5	rexlimivw	$⊢ \exists x \in V (y \in (N ClWWalksN G) \land y (0) = x) \to y \in (N ClWWalksN G)$
7		eqid	$⊢ Edg (G) = Edg (G)$
8	1 7	clwwlknp	$⊢ y \in (N ClWWalksN G) \to ((y \in Word V \land \|y\| = N) \land \forall i \in (0 ..^N - 1) \{y (i), y (i + 1)\} \in Edg (G) \land \{lastS (y), y (0)\} \in Edg (G))$
9	8	anim2i	$⊢ (G \in USGraph \land y \in (N ClWWalksN G)) \to (G \in USGraph \land ((y \in Word V \land \|y\| = N) \land \forall i \in (0 ..^N - 1) \{y (i), y (i + 1)\} \in Edg (G) \land \{lastS (y), y (0)\} \in Edg (G)))$
10	7 1	usgrpredgv	$⊢ (G \in USGraph \land \{lastS (y), y (0)\} \in Edg (G)) \to (lastS (y) \in V \land y (0) \in V)$
11	10	ex	$⊢ G \in USGraph \to (\{lastS (y), y (0)\} \in Edg (G) \to (lastS (y) \in V \land y (0) \in V))$
12		simpr	$⊢ (lastS (y) \in V \land y (0) \in V) \to y (0) \in V$
13	11 12	syl6com	$⊢ \{lastS (y), y (0)\} \in Edg (G) \to (G \in USGraph \to y (0) \in V)$
14	13	3ad2ant3	$⊢ ((y \in Word V \land \|y\| = N) \land \forall i \in (0 ..^N - 1) \{y (i), y (i + 1)\} \in Edg (G) \land \{lastS (y), y (0)\} \in Edg (G)) \to (G \in USGraph \to y (0) \in V)$
15	14	impcom	$⊢ (G \in USGraph \land ((y \in Word V \land \|y\| = N) \land \forall i \in (0 ..^N - 1) \{y (i), y (i + 1)\} \in Edg (G) \land \{lastS (y), y (0)\} \in Edg (G))) \to y (0) \in V$
16		simpr	$⊢ ((G \in USGraph \land ((y \in Word V \land \|y\| = N) \land \forall i \in (0 ..^N - 1) \{y (i), y (i + 1)\} \in Edg (G) \land \{lastS (y), y (0)\} \in Edg (G))) \land x = y (0)) \to x = y (0)$
17	16	eqcomd	$⊢ ((G \in USGraph \land ((y \in Word V \land \|y\| = N) \land \forall i \in (0 ..^N - 1) \{y (i), y (i + 1)\} \in Edg (G) \land \{lastS (y), y (0)\} \in Edg (G))) \land x = y (0)) \to y (0) = x$
18	17	biantrud	$⊢ ((G \in USGraph \land ((y \in Word V \land \|y\| = N) \land \forall i \in (0 ..^N - 1) \{y (i), y (i + 1)\} \in Edg (G) \land \{lastS (y), y (0)\} \in Edg (G))) \land x = y (0)) \to (y \in (N ClWWalksN G) \leftrightarrow (y \in (N ClWWalksN G) \land y (0) = x))$
19	18	bicomd	$⊢ ((G \in USGraph \land ((y \in Word V \land \|y\| = N) \land \forall i \in (0 ..^N - 1) \{y (i), y (i + 1)\} \in Edg (G) \land \{lastS (y), y (0)\} \in Edg (G))) \land x = y (0)) \to ((y \in (N ClWWalksN G) \land y (0) = x) \leftrightarrow y \in (N ClWWalksN G))$
20	15 19	rspcedv	$⊢ (G \in USGraph \land ((y \in Word V \land \|y\| = N) \land \forall i \in (0 ..^N - 1) \{y (i), y (i + 1)\} \in Edg (G) \land \{lastS (y), y (0)\} \in Edg (G))) \to (y \in (N ClWWalksN G) \to \exists x \in V (y \in (N ClWWalksN G) \land y (0) = x))$
21	20	adantld	$⊢ (G \in USGraph \land ((y \in Word V \land \|y\| = N) \land \forall i \in (0 ..^N - 1) \{y (i), y (i + 1)\} \in Edg (G) \land \{lastS (y), y (0)\} \in Edg (G))) \to ((G \in USGraph \land y \in (N ClWWalksN G)) \to \exists x \in V (y \in (N ClWWalksN G) \land y (0) = x))$
22	9 21	mpcom	$⊢ (G \in USGraph \land y \in (N ClWWalksN G)) \to \exists x \in V (y \in (N ClWWalksN G) \land y (0) = x)$
23	22	ex	$⊢ G \in USGraph \to (y \in (N ClWWalksN G) \to \exists x \in V (y \in (N ClWWalksN G) \land y (0) = x))$
24	6 23	impbid2	$⊢ G \in USGraph \to (\exists x \in V (y \in (N ClWWalksN G) \land y (0) = x) \leftrightarrow y \in (N ClWWalksN G))$
25	4 24	bitrid	$⊢ G \in USGraph \to (\exists x \in V y \in (x ClWWalksNOn (G) N) \leftrightarrow y \in (N ClWWalksN G))$
26	2 25	bitr2id	$⊢ G \in USGraph \to (y \in (N ClWWalksN G) \leftrightarrow y \in ⋃_{x \in V} (x ClWWalksNOn (G) N))$
27	26	eqrdv	$⊢ G \in USGraph \to N ClWWalksN G = ⋃_{x \in V} (x ClWWalksNOn (G) N)$

Metamath Proof Explorer

Theorem clwwlknun

Proof