Metamath Proof Explorer


Definition df-ewlks

Description: Define the set of all s-walks of edges (in a hypergraph) corresponding to s-walks "on the edge level" discussed in Aksoy et al. For an extended nonnegative integer s, an s-walk is a sequence of hyperedges, e(0), e(1), ... , e(k), where e(j-1) and e(j) have at least s vertices in common (for j=1, ... , k). In contrast to the definition in Aksoy et al., s = 0 (a 0-walk is an arbitrary sequence of hyperedges) and s = +oo (then the number of common vertices of two adjacent hyperedges must be infinite) are allowed. Furthermore, it is not forbidden that adjacent hyperedges are equal. (Contributed by AV, 4-Jan-2021)

Ref Expression
Assertion df-ewlks EdgWalks = ( 𝑔 ∈ V , 𝑠 ∈ ℕ0* ↦ { 𝑓[ ( iEdg ‘ 𝑔 ) / 𝑖 ] ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓𝑘 ) ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cewlks EdgWalks
1 vg 𝑔
2 cvv V
3 vs 𝑠
4 cxnn0 0*
5 vf 𝑓
6 ciedg iEdg
7 1 cv 𝑔
8 7 6 cfv ( iEdg ‘ 𝑔 )
9 vi 𝑖
10 5 cv 𝑓
11 9 cv 𝑖
12 11 cdm dom 𝑖
13 12 cword Word dom 𝑖
14 10 13 wcel 𝑓 ∈ Word dom 𝑖
15 vk 𝑘
16 c1 1
17 cfzo ..^
18 chash
19 10 18 cfv ( ♯ ‘ 𝑓 )
20 16 19 17 co ( 1 ..^ ( ♯ ‘ 𝑓 ) )
21 3 cv 𝑠
22 cle
23 15 cv 𝑘
24 cmin
25 23 16 24 co ( 𝑘 − 1 )
26 25 10 cfv ( 𝑓 ‘ ( 𝑘 − 1 ) )
27 26 11 cfv ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) )
28 23 10 cfv ( 𝑓𝑘 )
29 28 11 cfv ( 𝑖 ‘ ( 𝑓𝑘 ) )
30 27 29 cin ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓𝑘 ) ) )
31 30 18 cfv ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓𝑘 ) ) ) )
32 21 31 22 wbr 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓𝑘 ) ) ) )
33 32 15 20 wral 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓𝑘 ) ) ) )
34 14 33 wa ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓𝑘 ) ) ) ) )
35 34 9 8 wsbc [ ( iEdg ‘ 𝑔 ) / 𝑖 ] ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓𝑘 ) ) ) ) )
36 35 5 cab { 𝑓[ ( iEdg ‘ 𝑔 ) / 𝑖 ] ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓𝑘 ) ) ) ) ) }
37 1 3 2 4 36 cmpo ( 𝑔 ∈ V , 𝑠 ∈ ℕ0* ↦ { 𝑓[ ( iEdg ‘ 𝑔 ) / 𝑖 ] ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓𝑘 ) ) ) ) ) } )
38 0 37 wceq EdgWalks = ( 𝑔 ∈ V , 𝑠 ∈ ℕ0* ↦ { 𝑓[ ( iEdg ‘ 𝑔 ) / 𝑖 ] ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓𝑘 ) ) ) ) ) } )