Step | Hyp | Ref
| Expression |
1 | | eupth2.v |
. 2
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | eupth2.i |
. 2
⊢ 𝐼 = (iEdg‘𝐺) |
3 | | eupth2.f |
. 2
⊢ (𝜑 → Fun 𝐼) |
4 | | eupth2.n |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
5 | | eupth2.p |
. . . 4
⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) |
6 | | eupthis1wlk 41380 |
. . . 4
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
7 | | 1wlkcl 40820 |
. . . 4
⊢ (𝐹(1Walks‘𝐺)𝑃 → (#‘𝐹) ∈
ℕ0) |
8 | 5, 6, 7 | 3syl 18 |
. . 3
⊢ (𝜑 → (#‘𝐹) ∈
ℕ0) |
9 | | eupth2.l |
. . 3
⊢ (𝜑 → (𝑁 + 1) ≤ (#‘𝐹)) |
10 | | nn0p1elfzo 12378 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ0 ∧ (𝑁 + 1) ≤ (#‘𝐹)) → 𝑁 ∈ (0..^(#‘𝐹))) |
11 | 4, 8, 9, 10 | syl3anc 1318 |
. 2
⊢ (𝜑 → 𝑁 ∈ (0..^(#‘𝐹))) |
12 | | eupth2.u |
. 2
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
13 | | eupthistrl 41379 |
. . 3
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹(TrailS‘𝐺)𝑃) |
14 | 5, 13 | syl 17 |
. 2
⊢ (𝜑 → 𝐹(TrailS‘𝐺)𝑃) |
15 | | eupth2.h |
. . . . 5
⊢ 𝐻 = 〈𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑁)))〉 |
16 | 15 | fveq2i 6106 |
. . . 4
⊢
(Vtx‘𝐻) =
(Vtx‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑁)))〉) |
17 | | fvex 6113 |
. . . . . 6
⊢
(Vtx‘𝐺) ∈
V |
18 | 1, 17 | eqeltri 2684 |
. . . . 5
⊢ 𝑉 ∈ V |
19 | | fvex 6113 |
. . . . . . 7
⊢
(iEdg‘𝐺)
∈ V |
20 | 2, 19 | eqeltri 2684 |
. . . . . 6
⊢ 𝐼 ∈ V |
21 | 20 | resex 5363 |
. . . . 5
⊢ (𝐼 ↾ (𝐹 “ (0..^𝑁))) ∈ V |
22 | 18, 21 | opvtxfvi 25686 |
. . . 4
⊢
(Vtx‘〈𝑉,
(𝐼 ↾ (𝐹 “ (0..^𝑁)))〉) = 𝑉 |
23 | 16, 22 | eqtri 2632 |
. . 3
⊢
(Vtx‘𝐻) =
𝑉 |
24 | 23 | a1i 11 |
. 2
⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) |
25 | | snex 4835 |
. . . 4
⊢
{〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉} ∈ V |
26 | 18, 25 | opvtxfvi 25686 |
. . 3
⊢
(Vtx‘〈𝑉,
{〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}〉) = 𝑉 |
27 | 26 | a1i 11 |
. 2
⊢ (𝜑 → (Vtx‘〈𝑉, {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}〉) = 𝑉) |
28 | | eupth2.x |
. . . . 5
⊢ 𝑋 = 〈𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))〉 |
29 | 28 | fveq2i 6106 |
. . . 4
⊢
(Vtx‘𝑋) =
(Vtx‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))〉) |
30 | 20 | resex 5363 |
. . . . 5
⊢ (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1)))) ∈ V |
31 | 18, 30 | opvtxfvi 25686 |
. . . 4
⊢
(Vtx‘〈𝑉,
(𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))〉) = 𝑉 |
32 | 29, 31 | eqtri 2632 |
. . 3
⊢
(Vtx‘𝑋) =
𝑉 |
33 | 32 | a1i 11 |
. 2
⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) |
34 | 15 | fveq2i 6106 |
. . . 4
⊢
(iEdg‘𝐻) =
(iEdg‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑁)))〉) |
35 | 18, 21 | opiedgfvi 25687 |
. . . 4
⊢
(iEdg‘〈𝑉,
(𝐼 ↾ (𝐹 “ (0..^𝑁)))〉) = (𝐼 ↾ (𝐹 “ (0..^𝑁))) |
36 | 34, 35 | eqtri 2632 |
. . 3
⊢
(iEdg‘𝐻) =
(𝐼 ↾ (𝐹 “ (0..^𝑁))) |
37 | 36 | a1i 11 |
. 2
⊢ (𝜑 → (iEdg‘𝐻) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) |
38 | 18, 25 | opiedgfvi 25687 |
. . 3
⊢
(iEdg‘〈𝑉,
{〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}〉) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉} |
39 | 38 | a1i 11 |
. 2
⊢ (𝜑 → (iEdg‘〈𝑉, {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}〉) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) |
40 | 28 | fveq2i 6106 |
. . . 4
⊢
(iEdg‘𝑋) =
(iEdg‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))〉) |
41 | 18, 30 | opiedgfvi 25687 |
. . . 4
⊢
(iEdg‘〈𝑉,
(𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))〉) = (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1)))) |
42 | 40, 41 | eqtri 2632 |
. . 3
⊢
(iEdg‘𝑋) =
(𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1)))) |
43 | 4 | nn0zd 11356 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
44 | | fzval3 12404 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ →
(0...𝑁) = (0..^(𝑁 + 1))) |
45 | 44 | eqcomd 2616 |
. . . . . 6
⊢ (𝑁 ∈ ℤ →
(0..^(𝑁 + 1)) = (0...𝑁)) |
46 | 43, 45 | syl 17 |
. . . . 5
⊢ (𝜑 → (0..^(𝑁 + 1)) = (0...𝑁)) |
47 | 46 | imaeq2d 5385 |
. . . 4
⊢ (𝜑 → (𝐹 “ (0..^(𝑁 + 1))) = (𝐹 “ (0...𝑁))) |
48 | 47 | reseq2d 5317 |
. . 3
⊢ (𝜑 → (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1)))) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) |
49 | 42, 48 | syl5eq 2656 |
. 2
⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) |
50 | | eupth2.o |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝐻)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) |
51 | | eupth2.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ UPGraph ) |
52 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) |
53 | 2 | upgrwlkedg 40850 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
54 | 51, 52, 53 | syl2anc 691 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
55 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (𝐹‘𝑘) = (𝐹‘𝑁)) |
56 | 55 | fveq2d 6107 |
. . . . 5
⊢ (𝑘 = 𝑁 → (𝐼‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘𝑁))) |
57 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (𝑃‘𝑘) = (𝑃‘𝑁)) |
58 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (𝑘 + 1) = (𝑁 + 1)) |
59 | 58 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (𝑃‘(𝑘 + 1)) = (𝑃‘(𝑁 + 1))) |
60 | 57, 59 | preq12d 4220 |
. . . . 5
⊢ (𝑘 = 𝑁 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}) |
61 | 56, 60 | eqeq12d 2625 |
. . . 4
⊢ (𝑘 = 𝑁 → ((𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))})) |
62 | 61 | rspcv 3278 |
. . 3
⊢ (𝑁 ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))})) |
63 | 11, 54, 62 | sylc 63 |
. 2
⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}) |
64 | 1, 2, 3, 11, 12, 14, 24, 27, 33, 37, 39, 49, 50, 63 | eupth2lem3lem7 41402 |
1
⊢ (𝜑 → (¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |