This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Walks, paths and cycles Walks 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 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } )