| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
| 2 |
1
|
wlkf |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) |
| 3 |
2
|
adantr |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) |
| 4 |
|
pfxcl |
⊢ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( 𝐹 prefix 𝐿 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ) |
| 5 |
3 4
|
syl |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 prefix 𝐿 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ) |
| 6 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
| 7 |
6
|
wlkp |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) |
| 8 |
7
|
adantr |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) |
| 9 |
|
elfzuz3 |
⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 𝐿 ) ) |
| 10 |
|
fzss2 |
⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 𝐿 ) → ( 0 ... 𝐿 ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) |
| 11 |
9 10
|
syl |
⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 0 ... 𝐿 ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) |
| 12 |
11
|
adantl |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 0 ... 𝐿 ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) |
| 13 |
8 12
|
fssresd |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ↾ ( 0 ... 𝐿 ) ) : ( 0 ... 𝐿 ) ⟶ ( Vtx ‘ 𝐺 ) ) |
| 14 |
|
pfxlen |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) = 𝐿 ) |
| 15 |
2 14
|
sylan |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) = 𝐿 ) |
| 16 |
15
|
oveq2d |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 0 ... ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) = ( 0 ... 𝐿 ) ) |
| 17 |
16
|
feq2d |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑃 ↾ ( 0 ... 𝐿 ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ ( 𝑃 ↾ ( 0 ... 𝐿 ) ) : ( 0 ... 𝐿 ) ⟶ ( Vtx ‘ 𝐺 ) ) ) |
| 18 |
13 17
|
mpbird |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ↾ ( 0 ... 𝐿 ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) |
| 19 |
6
|
wlkpwrd |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) |
| 20 |
|
fzp1elp1 |
⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 𝐿 + 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝐹 ) + 1 ) ) ) |
| 21 |
20
|
adantl |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐿 + 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝐹 ) + 1 ) ) ) |
| 22 |
|
wlklenvp1 |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) |
| 23 |
22
|
oveq2d |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 0 ... ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ( ♯ ‘ 𝐹 ) + 1 ) ) ) |
| 24 |
23
|
adantr |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 0 ... ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ( ♯ ‘ 𝐹 ) + 1 ) ) ) |
| 25 |
21 24
|
eleqtrrd |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐿 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑃 ) ) ) |
| 26 |
|
pfxres |
⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝐿 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑃 ) ) ) → ( 𝑃 prefix ( 𝐿 + 1 ) ) = ( 𝑃 ↾ ( 0 ..^ ( 𝐿 + 1 ) ) ) ) |
| 27 |
19 25 26
|
syl2an2r |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 prefix ( 𝐿 + 1 ) ) = ( 𝑃 ↾ ( 0 ..^ ( 𝐿 + 1 ) ) ) ) |
| 28 |
|
elfzelz |
⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → 𝐿 ∈ ℤ ) |
| 29 |
|
fzval3 |
⊢ ( 𝐿 ∈ ℤ → ( 0 ... 𝐿 ) = ( 0 ..^ ( 𝐿 + 1 ) ) ) |
| 30 |
28 29
|
syl |
⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 0 ... 𝐿 ) = ( 0 ..^ ( 𝐿 + 1 ) ) ) |
| 31 |
30
|
adantl |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 0 ... 𝐿 ) = ( 0 ..^ ( 𝐿 + 1 ) ) ) |
| 32 |
31
|
reseq2d |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ↾ ( 0 ... 𝐿 ) ) = ( 𝑃 ↾ ( 0 ..^ ( 𝐿 + 1 ) ) ) ) |
| 33 |
27 32
|
eqtr4d |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 prefix ( 𝐿 + 1 ) ) = ( 𝑃 ↾ ( 0 ... 𝐿 ) ) ) |
| 34 |
33
|
feq1d |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑃 prefix ( 𝐿 + 1 ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ ( 𝑃 ↾ ( 0 ... 𝐿 ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) |
| 35 |
18 34
|
mpbird |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 prefix ( 𝐿 + 1 ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) |
| 36 |
6 1
|
wlkprop |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) |
| 37 |
36
|
simp3d |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 38 |
37
|
adantr |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 39 |
38
|
adantr |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 40 |
15
|
oveq2d |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) = ( 0 ..^ 𝐿 ) ) |
| 41 |
40
|
eleq2d |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ↔ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) ) |
| 42 |
33
|
fveq1d |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ... 𝐿 ) ) ‘ 𝑘 ) ) |
| 43 |
42
|
adantr |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ... 𝐿 ) ) ‘ 𝑘 ) ) |
| 44 |
|
fzossfz |
⊢ ( 0 ..^ 𝐿 ) ⊆ ( 0 ... 𝐿 ) |
| 45 |
44
|
a1i |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 0 ..^ 𝐿 ) ⊆ ( 0 ... 𝐿 ) ) |
| 46 |
45
|
sselda |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → 𝑘 ∈ ( 0 ... 𝐿 ) ) |
| 47 |
46
|
fvresd |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑃 ↾ ( 0 ... 𝐿 ) ) ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ) |
| 48 |
43 47
|
eqtr2d |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ) |
| 49 |
33
|
fveq1d |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 ↾ ( 0 ... 𝐿 ) ) ‘ ( 𝑘 + 1 ) ) ) |
| 50 |
49
|
adantr |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 ↾ ( 0 ... 𝐿 ) ) ‘ ( 𝑘 + 1 ) ) ) |
| 51 |
|
fzofzp1 |
⊢ ( 𝑘 ∈ ( 0 ..^ 𝐿 ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝐿 ) ) |
| 52 |
51
|
adantl |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝐿 ) ) |
| 53 |
52
|
fvresd |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑃 ↾ ( 0 ... 𝐿 ) ) ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) |
| 54 |
50 53
|
eqtr2d |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) |
| 55 |
48 54
|
jca |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ) |
| 56 |
55
|
ex |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑘 ∈ ( 0 ..^ 𝐿 ) → ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ) ) |
| 57 |
41 56
|
sylbid |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) → ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ) ) |
| 58 |
57
|
imp |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ) |
| 59 |
3
|
ancli |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) ) |
| 60 |
|
simpr |
⊢ ( ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → 𝑘 ∈ ( 0 ..^ 𝐿 ) ) |
| 61 |
60
|
fvresd |
⊢ ( ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝐹 ↾ ( 0 ..^ 𝐿 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) |
| 62 |
61
|
fveq2d |
⊢ ( ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝐿 ) ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) |
| 63 |
59 62
|
sylan |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝐿 ) ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) |
| 64 |
63
|
eqcomd |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝐿 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝐿 ) ) ‘ 𝑘 ) ) ) |
| 65 |
64
|
ex |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑘 ∈ ( 0 ..^ 𝐿 ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝐿 ) ) ‘ 𝑘 ) ) ) ) |
| 66 |
41 65
|
sylbid |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝐿 ) ) ‘ 𝑘 ) ) ) ) |
| 67 |
66
|
imp |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝐿 ) ) ‘ 𝑘 ) ) ) |
| 68 |
|
simplr |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) |
| 69 |
|
pfxres |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 prefix 𝐿 ) = ( 𝐹 ↾ ( 0 ..^ 𝐿 ) ) ) |
| 70 |
3 68 69
|
syl2an2r |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → ( 𝐹 prefix 𝐿 ) = ( 𝐹 ↾ ( 0 ..^ 𝐿 ) ) ) |
| 71 |
70
|
fveq1d |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) = ( ( 𝐹 ↾ ( 0 ..^ 𝐿 ) ) ‘ 𝑘 ) ) |
| 72 |
71
|
fveq2d |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝐿 ) ) ‘ 𝑘 ) ) ) |
| 73 |
67 72
|
eqtr4d |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) |
| 74 |
58 73
|
jca |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → ( ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) ) |
| 75 |
9
|
adantl |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 𝐿 ) ) |
| 76 |
15
|
fveq2d |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ℤ≥ ‘ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) = ( ℤ≥ ‘ 𝐿 ) ) |
| 77 |
75 76
|
eleqtrrd |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) |
| 78 |
|
fzoss2 |
⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) |
| 79 |
77 78
|
syl |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) |
| 80 |
79
|
sselda |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) |
| 81 |
|
wkslem1 |
⊢ ( 𝑥 = 𝑘 → ( if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) |
| 82 |
81
|
rspcv |
⊢ ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) → if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) |
| 83 |
80 82
|
syl |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) → if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) |
| 84 |
|
eqeq12 |
⊢ ( ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) → ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ) |
| 85 |
84
|
adantr |
⊢ ( ( ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) → ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ) |
| 86 |
|
simpr |
⊢ ( ( ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) |
| 87 |
|
sneq |
⊢ ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) → { ( 𝑃 ‘ 𝑘 ) } = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) } ) |
| 88 |
87
|
adantr |
⊢ ( ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) → { ( 𝑃 ‘ 𝑘 ) } = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) } ) |
| 89 |
88
|
adantr |
⊢ ( ( ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) → { ( 𝑃 ‘ 𝑘 ) } = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) } ) |
| 90 |
86 89
|
eqeq12d |
⊢ ( ( ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) } ) ) |
| 91 |
|
preq12 |
⊢ ( ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) } ) |
| 92 |
91
|
adantr |
⊢ ( ( ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) } ) |
| 93 |
92 86
|
sseq12d |
⊢ ( ( ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) ) |
| 94 |
85 90 93
|
ifpbi123d |
⊢ ( ( ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) → ( if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) ) ) |
| 95 |
94
|
biimpd |
⊢ ( ( ( ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) → ( if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) ) ) |
| 96 |
74 83 95
|
sylsyld |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) → if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) ) ) |
| 97 |
39 96
|
mpd |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ) → if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) ) |
| 98 |
97
|
ralrimiva |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) ) |
| 99 |
|
wlkv |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) |
| 100 |
99
|
simp1d |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐺 ∈ V ) |
| 101 |
100
|
adantr |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → 𝐺 ∈ V ) |
| 102 |
6 1
|
iswlkg |
⊢ ( 𝐺 ∈ V → ( ( 𝐹 prefix 𝐿 ) ( Walks ‘ 𝐺 ) ( 𝑃 prefix ( 𝐿 + 1 ) ) ↔ ( ( 𝐹 prefix 𝐿 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 𝑃 prefix ( 𝐿 + 1 ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) ) ) ) |
| 103 |
101 102
|
syl |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 prefix 𝐿 ) ( Walks ‘ 𝐺 ) ( 𝑃 prefix ( 𝐿 + 1 ) ) ↔ ( ( 𝐹 prefix 𝐿 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 𝑃 prefix ( 𝐿 + 1 ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) ) if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ 𝑘 ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 prefix 𝐿 ) ‘ 𝑘 ) ) ) ) ) ) |
| 104 |
5 35 98 103
|
mpbir3and |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 prefix 𝐿 ) ( Walks ‘ 𝐺 ) ( 𝑃 prefix ( 𝐿 + 1 ) ) ) |