Step | Hyp | Ref
| Expression |
1 | | wlkv 40815 |
. . . 4
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
2 | | usgrupgr 40412 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph
) |
3 | | 3simpc 1053 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
4 | 2, 3 | anim12i 588 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧ (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐺 ∈ UPGraph ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
5 | | 3anass 1035 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ↔ (𝐺 ∈ UPGraph ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
6 | 4, 5 | sylibr 223 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧ (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
7 | | eqid 2610 |
. . . . . . . . 9
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
8 | | eqid 2610 |
. . . . . . . . 9
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
9 | 7, 8 | upgriswlk 40849 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
10 | 6, 9 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
11 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V |
12 | | 1ex 9914 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
V |
13 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 0 → (𝐹‘𝑘) = (𝐹‘0)) |
14 | 13 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 0 → ((iEdg‘𝐺)‘(𝐹‘𝑘)) = ((iEdg‘𝐺)‘(𝐹‘0))) |
15 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
16 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1)) |
17 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 + 1) =
1 |
18 | 16, 17 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 0 → (𝑘 + 1) = 1) |
19 | 18 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
20 | 15, 19 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
21 | 14, 20 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 0 → (((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)})) |
22 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1)) |
23 | 22 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 1 → ((iEdg‘𝐺)‘(𝐹‘𝑘)) = ((iEdg‘𝐺)‘(𝐹‘1))) |
24 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1)) |
25 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
26 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 + 1) =
2 |
27 | 25, 26 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 1 → (𝑘 + 1) = 2) |
28 | 27 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2)) |
29 | 24, 28 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)}) |
30 | 23, 29 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 1 → (((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
31 | 11, 12, 21, 30 | ralpr 4185 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
{0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
32 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → 𝐺 ∈ USGraph ) |
33 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃‘0) ∈
V |
34 | 8 | usgrnloopv 40427 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ USGraph ∧ (𝑃‘0) ∈ V) →
(((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → (𝑃‘0) ≠ (𝑃‘1))) |
35 | 32, 33, 34 | sylancl 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → (𝑃‘0) ≠ (𝑃‘1))) |
36 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃‘1) ∈
V |
37 | 8 | usgrnloopv 40427 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ USGraph ∧ (𝑃‘1) ∈ V) →
(((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘1) ≠ (𝑃‘2))) |
38 | 32, 36, 37 | sylancl 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → (((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘1) ≠ (𝑃‘2))) |
39 | 35, 38 | anim12d 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)))) |
40 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐹‘0) = (𝐹‘1) → ((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1))) |
41 | 40 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹‘0) = (𝐹‘1) → (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ↔ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)})) |
42 | | eqtr2 2630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → {(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)}) |
43 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ {(𝑃‘1), (𝑃‘2)} = {(𝑃‘2), (𝑃‘1)} |
44 | 43 | eqeq2i 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ({(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)} ↔ {(𝑃‘0), (𝑃‘1)} = {(𝑃‘2), (𝑃‘1)}) |
45 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑃‘2) ∈
V |
46 | 33, 45 | preqr1 4319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ({(𝑃‘0), (𝑃‘1)} = {(𝑃‘2), (𝑃‘1)} → (𝑃‘0) = (𝑃‘2)) |
47 | 44, 46 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ({(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)} → (𝑃‘0) = (𝑃‘2)) |
48 | 42, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) = (𝑃‘2)) |
49 | 48 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)} → (((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘0) = (𝑃‘2))) |
50 | 41, 49 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐹‘0) = (𝐹‘1) → (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → (((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘0) = (𝑃‘2)))) |
51 | 50 | impd 446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹‘0) = (𝐹‘1) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) = (𝑃‘2))) |
52 | 51 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((𝐹‘0) = (𝐹‘1) → (𝑃‘0) = (𝑃‘2))) |
53 | 52 | necon3d 2803 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((𝑃‘0) ≠ (𝑃‘2) → (𝐹‘0) ≠ (𝐹‘1))) |
54 | 53 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑃‘0) ≠ (𝑃‘2) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐹‘0) ≠ (𝐹‘1))) |
55 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐹‘0) ≠ (𝐹‘1))) |
56 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)) → (𝑃‘0) ≠ (𝑃‘1)) |
57 | 56 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) → (𝑃‘0) ≠ (𝑃‘1)) |
58 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) → (𝑃‘0) ≠ (𝑃‘2)) |
59 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) → (𝑃‘1) ≠ (𝑃‘2)) |
60 | 57, 58, 59 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2))) |
61 | 55, 60 | jctild 564 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
62 | 61 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘0) ≠ (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
63 | 62 | com23 84 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘0) ≠ (𝑃‘2) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
64 | 63 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
66 | 39, 65 | mpdd 42 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
67 | 31, 66 | syl5bi 231 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
68 | 67 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) → (𝑃:(0...2)⟶(Vtx‘𝐺) → (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
69 | 68 | com23 84 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) → (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
70 | 69 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
((𝑃‘0) ≠ (𝑃‘2) → (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
71 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 2
→ (𝑃‘(#‘𝐹)) = (𝑃‘2)) |
72 | 71 | neeq2d 2842 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 2
→ ((𝑃‘0) ≠
(𝑃‘(#‘𝐹)) ↔ (𝑃‘0) ≠ (𝑃‘2))) |
73 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
(0..^2)) |
74 | | fzo0to2pr 12420 |
. . . . . . . . . . . . . . . . 17
⊢ (0..^2) =
{0, 1} |
75 | 73, 74 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
{0, 1}) |
76 | 75 | raleqdv 3121 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 2
→ (∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
77 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 2
→ (0...(#‘𝐹)) =
(0...2)) |
78 | 77 | feq2d 5944 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 2
→ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ↔ 𝑃:(0...2)⟶(Vtx‘𝐺))) |
79 | 78 | imbi1d 330 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 2
→ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))) ↔ (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
80 | 76, 79 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 2
→ ((∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))) ↔ (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
81 | 72, 80 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 2
→ (((𝑃‘0) ≠
(𝑃‘(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) ↔ ((𝑃‘0) ≠ (𝑃‘2) → (∀𝑘 ∈ {0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))))) |
82 | 70, 81 | syl5ibrcom 236 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
((#‘𝐹) = 2 →
((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))))) |
83 | 82 | impd 446 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
(((#‘𝐹) = 2 ∧
(𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
84 | 83 | com24 93 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
(𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
85 | 84 | ex 449 |
. . . . . . . . 9
⊢ (𝐺 ∈ USGraph → (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))))) |
86 | 85 | 3impd 1273 |
. . . . . . . 8
⊢ (𝐺 ∈ USGraph → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
87 | 86 | adantr 480 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
88 | 10, 87 | sylbid 229 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(1Walks‘𝐺)𝑃 → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
89 | 88 | ex 449 |
. . . . 5
⊢ (𝐺 ∈ USGraph → ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(1Walks‘𝐺)𝑃 → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
90 | 89 | com13 86 |
. . . 4
⊢ (𝐹(1Walks‘𝐺)𝑃 → ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐺 ∈ USGraph → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
91 | 1, 90 | mpd 15 |
. . 3
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ USGraph → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
92 | 91 | impcom 445 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
93 | 92 | imp 444 |
1
⊢ (((𝐺 ∈ USGraph ∧ 𝐹(1Walks‘𝐺)𝑃) ∧ ((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))) |