df-wlks

Description: Define the set of all walks (in a hypergraph). Such walks correspond to the s-walks "on the vertex level" (with s = 1), and also to 1-walks "on the edge level" (see wlk1walk ) discussed in Aksoy et al. The predicate F ( WalksG ) P can be read as "The pair <. F , P >. represents a walk in a graph G ", see also iswlk .

The condition { ( pk ) , ( p( k + 1 ) ) } C_ ( ( iEdgg )( fk ) ) (hereinafter referred to as C) would not be sufficient, because the repetition of a vertex in a walk (i.e. ( pk ) = ( p( k + 1 ) ) should be allowed only if there is a loop at ( pk ) . Otherwise, C would be fulfilled by each edge containing ( pk ) .

According to the definition of Bollobas p. 4.: "A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) ...", a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by AV, 30-Dec-2020)

		Ref	Expression
	Assertion	df-wlks	$⊢ Walks = (g \in V ⟼ \{⟨f, p⟩ \| (f \in Word dom iEdg (g) \land p : (0 \dots \|f\|) ⟶ Vtx (g) \land \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), iEdg (g) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k))))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwlks	$class Walks$
1		vg	$setvar g$
2		cvv	$class V$
3		vf	$setvar f$
4		vp	$setvar p$
5	3	cv	$setvar f$
6		ciedg	$class iEdg$
7	1	cv	$setvar g$
8	7 6	cfv	$class iEdg (g)$
9	8	cdm	$class dom iEdg (g)$
10	9	cword	$class Word dom iEdg (g)$
11	5 10	wcel	$wff f \in Word dom iEdg (g)$
12	4	cv	$setvar p$
13		cc0	$class 0$
14		cfz	$class \dots$
15		chash	$class \|.\|$
16	5 15	cfv	$class \|f\|$
17	13 16 14	co	$class (0 \dots \|f\|)$
18		cvtx	$class Vtx$
19	7 18	cfv	$class Vtx (g)$
20	17 19 12	wf	$wff p : (0 \dots \|f\|) ⟶ Vtx (g)$
21		vk	$setvar k$
22		cfzo	$class ..^$
23	13 16 22	co	$class (0 ..^\|f\|)$
24	21	cv	$setvar k$
25	24 12	cfv	$class p (k)$
26		caddc	$class +$
27		c1	$class 1$
28	24 27 26	co	$class (k + 1)$
29	28 12	cfv	$class p (k + 1)$
30	25 29	wceq	$wff p (k) = p (k + 1)$
31	24 5	cfv	$class f (k)$
32	31 8	cfv	$class iEdg (g) (f (k))$
33	25	csn	$class \{p (k)\}$
34	32 33	wceq	$wff iEdg (g) (f (k)) = \{p (k)\}$
35	25 29	cpr	$class \{p (k), p (k + 1)\}$
36	35 32	wss	$wff \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k))$
37	30 34 36	wif	$wff if- (p (k) = p (k + 1), iEdg (g) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k)))$
38	37 21 23	wral	$wff \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), iEdg (g) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k)))$
39	11 20 38	w3a	$wff (f \in Word dom iEdg (g) \land p : (0 \dots \|f\|) ⟶ Vtx (g) \land \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), iEdg (g) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k))))$
40	39 3 4	copab	$class \{⟨f, p⟩ \| (f \in Word dom iEdg (g) \land p : (0 \dots \|f\|) ⟶ Vtx (g) \land \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), iEdg (g) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k))))\}$
41	1 2 40	cmpt	$class (g \in V ⟼ \{⟨f, p⟩ \| (f \in Word dom iEdg (g) \land p : (0 \dots \|f\|) ⟶ Vtx (g) \land \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), iEdg (g) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k))))\})$
42	0 41	wceq	$wff Walks = (g \in V ⟼ \{⟨f, p⟩ \| (f \in Word dom iEdg (g) \land p : (0 \dots \|f\|) ⟶ Vtx (g) \land \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), iEdg (g) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k))))\})$

Metamath Proof Explorer

Definition df-wlks

Detailed syntax breakdown