Step |
Hyp |
Ref |
Expression |
1 |
|
2wlkd.p |
⊢ 𝑃 = 〈“ 𝐴 𝐵 𝐶 ”〉 |
2 |
|
2wlkd.f |
⊢ 𝐹 = 〈“ 𝐽 𝐾 ”〉 |
3 |
|
2wlkd.s |
⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) |
4 |
|
2wlkd.n |
⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ) |
5 |
|
2wlkd.e |
⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) ) |
6 |
|
2wlkd.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
7 |
|
2wlkd.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
8 |
1 2 3 4 5 6 7
|
2wlkd |
⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) |
9 |
3
|
simp1d |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
10 |
1
|
fveq1i |
⊢ ( 𝑃 ‘ 0 ) = ( 〈“ 𝐴 𝐵 𝐶 ”〉 ‘ 0 ) |
11 |
|
s3fv0 |
⊢ ( 𝐴 ∈ 𝑉 → ( 〈“ 𝐴 𝐵 𝐶 ”〉 ‘ 0 ) = 𝐴 ) |
12 |
10 11
|
syl5eq |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝑃 ‘ 0 ) = 𝐴 ) |
13 |
9 12
|
syl |
⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = 𝐴 ) |
14 |
2
|
fveq2i |
⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 〈“ 𝐽 𝐾 ”〉 ) |
15 |
|
s2len |
⊢ ( ♯ ‘ 〈“ 𝐽 𝐾 ”〉 ) = 2 |
16 |
14 15
|
eqtri |
⊢ ( ♯ ‘ 𝐹 ) = 2 |
17 |
1 16
|
fveq12i |
⊢ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 〈“ 𝐴 𝐵 𝐶 ”〉 ‘ 2 ) |
18 |
3
|
simp3d |
⊢ ( 𝜑 → 𝐶 ∈ 𝑉 ) |
19 |
|
s3fv2 |
⊢ ( 𝐶 ∈ 𝑉 → ( 〈“ 𝐴 𝐵 𝐶 ”〉 ‘ 2 ) = 𝐶 ) |
20 |
18 19
|
syl |
⊢ ( 𝜑 → ( 〈“ 𝐴 𝐵 𝐶 ”〉 ‘ 2 ) = 𝐶 ) |
21 |
17 20
|
syl5eq |
⊢ ( 𝜑 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) |
22 |
|
3simpb |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) |
23 |
3 22
|
syl |
⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) |
24 |
|
s2cli |
⊢ 〈“ 𝐽 𝐾 ”〉 ∈ Word V |
25 |
2 24
|
eqeltri |
⊢ 𝐹 ∈ Word V |
26 |
|
s3cli |
⊢ 〈“ 𝐴 𝐵 𝐶 ”〉 ∈ Word V |
27 |
1 26
|
eqeltri |
⊢ 𝑃 ∈ Word V |
28 |
25 27
|
pm3.2i |
⊢ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) |
29 |
6
|
iswlkon |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) ) |
30 |
23 28 29
|
sylancl |
⊢ ( 𝜑 → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) ) |
31 |
8 13 21 30
|
mpbir3and |
⊢ ( 𝜑 → 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 ) |