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 | | eupthiswlk 29159 |
. . . 4
β’ (πΉ(EulerPathsβπΊ)π β πΉ(WalksβπΊ)π) |
7 | | wlkcl 28566 |
. . . 4
β’ (πΉ(WalksβπΊ)π β (β―βπΉ) β
β0) |
8 | 5, 6, 7 | 3syl 18 |
. . 3
β’ (π β (β―βπΉ) β
β0) |
9 | | eupth2.l |
. . 3
β’ (π β (π + 1) β€ (β―βπΉ)) |
10 | | nn0p1elfzo 13616 |
. . 3
β’ ((π β β0
β§ (β―βπΉ)
β β0 β§ (π + 1) β€ (β―βπΉ)) β π β (0..^(β―βπΉ))) |
11 | 4, 8, 9, 10 | syl3anc 1372 |
. 2
β’ (π β π β (0..^(β―βπΉ))) |
12 | | eupth2.u |
. 2
β’ (π β π β π) |
13 | | eupthistrl 29158 |
. . 3
β’ (πΉ(EulerPathsβπΊ)π β πΉ(TrailsβπΊ)π) |
14 | 5, 13 | syl 17 |
. 2
β’ (π β πΉ(TrailsβπΊ)π) |
15 | | eupth2.h |
. . . . 5
β’ π» = β¨π, (πΌ βΎ (πΉ β (0..^π)))β© |
16 | 15 | fveq2i 6846 |
. . . 4
β’
(Vtxβπ») =
(Vtxββ¨π, (πΌ βΎ (πΉ β (0..^π)))β©) |
17 | 1 | fvexi 6857 |
. . . . 5
β’ π β V |
18 | 2 | fvexi 6857 |
. . . . . 6
β’ πΌ β V |
19 | 18 | resex 5986 |
. . . . 5
β’ (πΌ βΎ (πΉ β (0..^π))) β V |
20 | 17, 19 | opvtxfvi 27963 |
. . . 4
β’
(Vtxββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©) = π |
21 | 16, 20 | eqtri 2765 |
. . 3
β’
(Vtxβπ») =
π |
22 | 21 | a1i 11 |
. 2
β’ (π β (Vtxβπ») = π) |
23 | | snex 5389 |
. . . 4
β’
{β¨(πΉβπ), (πΌβ(πΉβπ))β©} β V |
24 | 17, 23 | opvtxfvi 27963 |
. . 3
β’
(Vtxββ¨π,
{β¨(πΉβπ), (πΌβ(πΉβπ))β©}β©) = π |
25 | 24 | a1i 11 |
. 2
β’ (π β (Vtxββ¨π, {β¨(πΉβπ), (πΌβ(πΉβπ))β©}β©) = π) |
26 | | eupth2.x |
. . . . 5
β’ π = β¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β© |
27 | 26 | fveq2i 6846 |
. . . 4
β’
(Vtxβπ) =
(Vtxββ¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β©) |
28 | 18 | resex 5986 |
. . . . 5
β’ (πΌ βΎ (πΉ β (0..^(π + 1)))) β V |
29 | 17, 28 | opvtxfvi 27963 |
. . . 4
β’
(Vtxββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©) = π |
30 | 27, 29 | eqtri 2765 |
. . 3
β’
(Vtxβπ) =
π |
31 | 30 | a1i 11 |
. 2
β’ (π β (Vtxβπ) = π) |
32 | 15 | fveq2i 6846 |
. . . 4
β’
(iEdgβπ») =
(iEdgββ¨π, (πΌ βΎ (πΉ β (0..^π)))β©) |
33 | 17, 19 | opiedgfvi 27964 |
. . . 4
β’
(iEdgββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©) = (πΌ βΎ (πΉ β (0..^π))) |
34 | 32, 33 | eqtri 2765 |
. . 3
β’
(iEdgβπ») =
(πΌ βΎ (πΉ β (0..^π))) |
35 | 34 | a1i 11 |
. 2
β’ (π β (iEdgβπ») = (πΌ βΎ (πΉ β (0..^π)))) |
36 | 17, 23 | opiedgfvi 27964 |
. . 3
β’
(iEdgββ¨π,
{β¨(πΉβπ), (πΌβ(πΉβπ))β©}β©) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©} |
37 | 36 | a1i 11 |
. 2
β’ (π β (iEdgββ¨π, {β¨(πΉβπ), (πΌβ(πΉβπ))β©}β©) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) |
38 | 26 | fveq2i 6846 |
. . . 4
β’
(iEdgβπ) =
(iEdgββ¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β©) |
39 | 17, 28 | opiedgfvi 27964 |
. . . 4
β’
(iEdgββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©) = (πΌ βΎ (πΉ β (0..^(π + 1)))) |
40 | 38, 39 | eqtri 2765 |
. . 3
β’
(iEdgβπ) =
(πΌ βΎ (πΉ β (0..^(π + 1)))) |
41 | 4 | nn0zd 12526 |
. . . . . 6
β’ (π β π β β€) |
42 | | fzval3 13642 |
. . . . . . 7
β’ (π β β€ β
(0...π) = (0..^(π + 1))) |
43 | 42 | eqcomd 2743 |
. . . . . 6
β’ (π β β€ β
(0..^(π + 1)) = (0...π)) |
44 | 41, 43 | syl 17 |
. . . . 5
β’ (π β (0..^(π + 1)) = (0...π)) |
45 | 44 | imaeq2d 6014 |
. . . 4
β’ (π β (πΉ β (0..^(π + 1))) = (πΉ β (0...π))) |
46 | 45 | reseq2d 5938 |
. . 3
β’ (π β (πΌ βΎ (πΉ β (0..^(π + 1)))) = (πΌ βΎ (πΉ β (0...π)))) |
47 | 40, 46 | eqtrid 2789 |
. 2
β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) |
48 | | eupth2.o |
. 2
β’ (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ»)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) |
49 | | 2fveq3 6848 |
. . . 4
β’ (π = π β (πΌβ(πΉβπ)) = (πΌβ(πΉβπ))) |
50 | | fveq2 6843 |
. . . . 5
β’ (π = π β (πβπ) = (πβπ)) |
51 | | fvoveq1 7381 |
. . . . 5
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
52 | 50, 51 | preq12d 4703 |
. . . 4
β’ (π = π β {(πβπ), (πβ(π + 1))} = {(πβπ), (πβ(π + 1))}) |
53 | 49, 52 | eqeq12d 2753 |
. . 3
β’ (π = π β ((πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
54 | | eupth2.g |
. . . 4
β’ (π β πΊ β UPGraph) |
55 | 5, 6 | syl 17 |
. . . 4
β’ (π β πΉ(WalksβπΊ)π) |
56 | 2 | upgrwlkedg 28593 |
. . . 4
β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π) β βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
57 | 54, 55, 56 | syl2anc 585 |
. . 3
β’ (π β βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
58 | 53, 57, 11 | rspcdva 3583 |
. 2
β’ (π β (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
59 | 1, 2, 3, 11, 12, 14, 22, 25, 31, 35, 37, 47, 48, 58 | eupth2lem3lem7 29181 |
1
β’ (π β (Β¬ 2 β₯
((VtxDegβπ)βπ) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |