Database
GRAPH THEORY
Walks, paths and cycles
Walks
df-ewlks
Metamath Proof Explorer
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 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } )