Step | Hyp | Ref
| Expression |
1 | | 1wlk2v2e.g |
. . . . 5
⊢ 𝐺 = 〈{𝑋, 𝑌}, 𝐼〉 |
2 | | 1wlk2v2e.i |
. . . . . 6
⊢ 𝐼 = 〈“{𝑋, 𝑌}”〉 |
3 | 2 | opeq2i 4344 |
. . . . 5
⊢
〈{𝑋, 𝑌}, 𝐼〉 = 〈{𝑋, 𝑌}, 〈“{𝑋, 𝑌}”〉〉 |
4 | 1, 3 | eqtri 2632 |
. . . 4
⊢ 𝐺 = 〈{𝑋, 𝑌}, 〈“{𝑋, 𝑌}”〉〉 |
5 | | 1wlk2v2e.x |
. . . . 5
⊢ 𝑋 ∈ V |
6 | | 1wlk2v2e.y |
. . . . 5
⊢ 𝑌 ∈ V |
7 | | uspgr2v1e2w 40477 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → 〈{𝑋, 𝑌}, 〈“{𝑋, 𝑌}”〉〉 ∈ USPGraph
) |
8 | 5, 6, 7 | mp2an 704 |
. . . 4
⊢
〈{𝑋, 𝑌}, 〈“{𝑋, 𝑌}”〉〉 ∈
USPGraph |
9 | 4, 8 | eqeltri 2684 |
. . 3
⊢ 𝐺 ∈
USPGraph |
10 | | uspgrupgr 40406 |
. . 3
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph
) |
11 | 9, 10 | ax-mp 5 |
. 2
⊢ 𝐺 ∈ UPGraph |
12 | | 1wlk2v2e.f |
. . 3
⊢ 𝐹 =
〈“00”〉 |
13 | | s2cli 13475 |
. . 3
⊢
〈“00”〉 ∈ Word V |
14 | 12, 13 | eqeltri 2684 |
. 2
⊢ 𝐹 ∈ Word V |
15 | | 1wlk2v2e.p |
. . 3
⊢ 𝑃 = 〈“𝑋𝑌𝑋”〉 |
16 | | s3cli 13476 |
. . 3
⊢
〈“𝑋𝑌𝑋”〉 ∈ Word V |
17 | 15, 16 | eqeltri 2684 |
. 2
⊢ 𝑃 ∈ Word V |
18 | 2, 12 | 1wlk2v2elem1 41322 |
. . . 4
⊢ 𝐹 ∈ Word dom 𝐼 |
19 | 5 | elexi 3186 |
. . . . . . . . . 10
⊢ 𝑋 ∈ V |
20 | 19 | prid1 4241 |
. . . . . . . . 9
⊢ 𝑋 ∈ {𝑋, 𝑌} |
21 | 6 | elexi 3186 |
. . . . . . . . . 10
⊢ 𝑌 ∈ V |
22 | 21 | prid2 4242 |
. . . . . . . . 9
⊢ 𝑌 ∈ {𝑋, 𝑌} |
23 | | s3cl 13474 |
. . . . . . . . 9
⊢ ((𝑋 ∈ {𝑋, 𝑌} ∧ 𝑌 ∈ {𝑋, 𝑌} ∧ 𝑋 ∈ {𝑋, 𝑌}) → 〈“𝑋𝑌𝑋”〉 ∈ Word {𝑋, 𝑌}) |
24 | 20, 22, 20, 23 | mp3an 1416 |
. . . . . . . 8
⊢
〈“𝑋𝑌𝑋”〉 ∈ Word {𝑋, 𝑌} |
25 | 15, 24 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑃 ∈ Word {𝑋, 𝑌} |
26 | | wrdf 13165 |
. . . . . . 7
⊢ (𝑃 ∈ Word {𝑋, 𝑌} → 𝑃:(0..^(#‘𝑃))⟶{𝑋, 𝑌}) |
27 | 25, 26 | ax-mp 5 |
. . . . . 6
⊢ 𝑃:(0..^(#‘𝑃))⟶{𝑋, 𝑌} |
28 | 15 | fveq2i 6106 |
. . . . . . . . 9
⊢
(#‘𝑃) =
(#‘〈“𝑋𝑌𝑋”〉) |
29 | | s3len 13489 |
. . . . . . . . 9
⊢
(#‘〈“𝑋𝑌𝑋”〉) = 3 |
30 | 28, 29 | eqtr2i 2633 |
. . . . . . . 8
⊢ 3 =
(#‘𝑃) |
31 | 30 | oveq2i 6560 |
. . . . . . 7
⊢ (0..^3) =
(0..^(#‘𝑃)) |
32 | 31 | feq2i 5950 |
. . . . . 6
⊢ (𝑃:(0..^3)⟶{𝑋, 𝑌} ↔ 𝑃:(0..^(#‘𝑃))⟶{𝑋, 𝑌}) |
33 | 27, 32 | mpbir 220 |
. . . . 5
⊢ 𝑃:(0..^3)⟶{𝑋, 𝑌} |
34 | 12 | fveq2i 6106 |
. . . . . . . . 9
⊢
(#‘𝐹) =
(#‘〈“00”〉) |
35 | | s2len 13484 |
. . . . . . . . 9
⊢
(#‘〈“00”〉) = 2 |
36 | 34, 35 | eqtri 2632 |
. . . . . . . 8
⊢
(#‘𝐹) =
2 |
37 | 36 | oveq2i 6560 |
. . . . . . 7
⊢
(0...(#‘𝐹)) =
(0...2) |
38 | | 3z 11287 |
. . . . . . . . 9
⊢ 3 ∈
ℤ |
39 | | fzoval 12340 |
. . . . . . . . 9
⊢ (3 ∈
ℤ → (0..^3) = (0...(3 − 1))) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . 8
⊢ (0..^3) =
(0...(3 − 1)) |
41 | | 3m1e2 11014 |
. . . . . . . . 9
⊢ (3
− 1) = 2 |
42 | 41 | oveq2i 6560 |
. . . . . . . 8
⊢ (0...(3
− 1)) = (0...2) |
43 | 40, 42 | eqtr2i 2633 |
. . . . . . 7
⊢ (0...2) =
(0..^3) |
44 | 37, 43 | eqtri 2632 |
. . . . . 6
⊢
(0...(#‘𝐹)) =
(0..^3) |
45 | 44 | feq2i 5950 |
. . . . 5
⊢ (𝑃:(0...(#‘𝐹))⟶{𝑋, 𝑌} ↔ 𝑃:(0..^3)⟶{𝑋, 𝑌}) |
46 | 33, 45 | mpbir 220 |
. . . 4
⊢ 𝑃:(0...(#‘𝐹))⟶{𝑋, 𝑌} |
47 | 2, 12, 5, 6, 15 | 1wlk2v2elem2 41323 |
. . . 4
⊢
∀𝑘 ∈
(0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} |
48 | 18, 46, 47 | 3pm3.2i 1232 |
. . 3
⊢ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶{𝑋, 𝑌} ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
49 | 1 | fveq2i 6106 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘〈{𝑋, 𝑌}, 𝐼〉) |
50 | | prex 4836 |
. . . . . 6
⊢ {𝑋, 𝑌} ∈ V |
51 | | s1cli 13237 |
. . . . . . 7
⊢
〈“{𝑋,
𝑌}”〉 ∈ Word
V |
52 | 2, 51 | eqeltri 2684 |
. . . . . 6
⊢ 𝐼 ∈ Word V |
53 | | opvtxfv 25681 |
. . . . . 6
⊢ (({𝑋, 𝑌} ∈ V ∧ 𝐼 ∈ Word V) →
(Vtx‘〈{𝑋, 𝑌}, 𝐼〉) = {𝑋, 𝑌}) |
54 | 50, 52, 53 | mp2an 704 |
. . . . 5
⊢
(Vtx‘〈{𝑋,
𝑌}, 𝐼〉) = {𝑋, 𝑌} |
55 | 49, 54 | eqtr2i 2633 |
. . . 4
⊢ {𝑋, 𝑌} = (Vtx‘𝐺) |
56 | 1 | fveq2i 6106 |
. . . . 5
⊢
(iEdg‘𝐺) =
(iEdg‘〈{𝑋, 𝑌}, 𝐼〉) |
57 | | opiedgfv 25684 |
. . . . . 6
⊢ (({𝑋, 𝑌} ∈ V ∧ 𝐼 ∈ Word V) →
(iEdg‘〈{𝑋, 𝑌}, 𝐼〉) = 𝐼) |
58 | 50, 52, 57 | mp2an 704 |
. . . . 5
⊢
(iEdg‘〈{𝑋, 𝑌}, 𝐼〉) = 𝐼 |
59 | 56, 58 | eqtr2i 2633 |
. . . 4
⊢ 𝐼 = (iEdg‘𝐺) |
60 | 55, 59 | upgriswlk 40849 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V) → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶{𝑋, 𝑌} ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
61 | 48, 60 | mpbiri 247 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V) → 𝐹(1Walks‘𝐺)𝑃) |
62 | 11, 14, 17, 61 | mp3an 1416 |
1
⊢ 𝐹(1Walks‘𝐺)𝑃 |