Step | Hyp | Ref
| Expression |
1 | | eupthp1.v |
. . 3
β’ π = (VtxβπΊ) |
2 | | eupthp1.i |
. . 3
β’ πΌ = (iEdgβπΊ) |
3 | | eupthp1.f |
. . 3
β’ (π β Fun πΌ) |
4 | | eupthp1.a |
. . 3
β’ (π β πΌ β Fin) |
5 | | eupthp1.b |
. . 3
β’ (π β π΅ β π) |
6 | | eupthp1.c |
. . 3
β’ (π β πΆ β π) |
7 | | eupthp1.d |
. . 3
β’ (π β Β¬ π΅ β dom πΌ) |
8 | | eupthp1.p |
. . 3
β’ (π β πΉ(EulerPathsβπΊ)π) |
9 | | eupthp1.n |
. . 3
β’ π = (β―βπΉ) |
10 | | eupthp1.e |
. . 3
β’ (π β πΈ β (EdgβπΊ)) |
11 | | eupthp1.x |
. . 3
β’ (π β {(πβπ), πΆ} β πΈ) |
12 | | eupthp1.u |
. . 3
β’
(iEdgβπ) =
(πΌ βͺ {β¨π΅, πΈβ©}) |
13 | | eupthp1.h |
. . 3
β’ π» = (πΉ βͺ {β¨π, π΅β©}) |
14 | | eupthp1.q |
. . 3
β’ π = (π βͺ {β¨(π + 1), πΆβ©}) |
15 | | eupthp1.s |
. . 3
β’
(Vtxβπ) =
π |
16 | | eupthp1.l |
. . 3
β’ ((π β§ πΆ = (πβπ)) β πΈ = {πΆ}) |
17 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16 | eupthp1 29163 |
. 2
β’ (π β π»(EulerPathsβπ)π) |
18 | | simpr 486 |
. . 3
β’ ((π β§ π»(EulerPathsβπ)π) β π»(EulerPathsβπ)π) |
19 | | eupthistrl 29158 |
. . . . 5
β’ (π»(EulerPathsβπ)π β π»(Trailsβπ)π) |
20 | 19 | adantl 483 |
. . . 4
β’ ((π β§ π»(EulerPathsβπ)π) β π»(Trailsβπ)π) |
21 | | fveq2 6843 |
. . . . . . . 8
β’ (π = 0 β (πβπ) = (πβ0)) |
22 | | fveq2 6843 |
. . . . . . . 8
β’ (π = 0 β (πβπ) = (πβ0)) |
23 | 21, 22 | eqeq12d 2753 |
. . . . . . 7
β’ (π = 0 β ((πβπ) = (πβπ) β (πβ0) = (πβ0))) |
24 | | eupthiswlk 29159 |
. . . . . . . . 9
β’ (πΉ(EulerPathsβπΊ)π β πΉ(WalksβπΊ)π) |
25 | 8, 24 | syl 17 |
. . . . . . . 8
β’ (π β πΉ(WalksβπΊ)π) |
26 | 12 | a1i 11 |
. . . . . . . 8
β’ (π β (iEdgβπ) = (πΌ βͺ {β¨π΅, πΈβ©})) |
27 | 15 | a1i 11 |
. . . . . . . 8
β’ (π β (Vtxβπ) = π) |
28 | 1, 2, 3, 4, 5, 6, 7, 25, 9, 10, 11, 26, 13, 14, 27 | wlkp1lem5 28628 |
. . . . . . 7
β’ (π β βπ β (0...π)(πβπ) = (πβπ)) |
29 | 2 | wlkf 28565 |
. . . . . . . . 9
β’ (πΉ(WalksβπΊ)π β πΉ β Word dom πΌ) |
30 | 24, 29 | syl 17 |
. . . . . . . 8
β’ (πΉ(EulerPathsβπΊ)π β πΉ β Word dom πΌ) |
31 | | lencl 14422 |
. . . . . . . . 9
β’ (πΉ β Word dom πΌ β (β―βπΉ) β
β0) |
32 | 9 | eleq1i 2829 |
. . . . . . . . . 10
β’ (π β β0
β (β―βπΉ)
β β0) |
33 | | 0elfz 13539 |
. . . . . . . . . 10
β’ (π β β0
β 0 β (0...π)) |
34 | 32, 33 | sylbir 234 |
. . . . . . . . 9
β’
((β―βπΉ)
β β0 β 0 β (0...π)) |
35 | 31, 34 | syl 17 |
. . . . . . . 8
β’ (πΉ β Word dom πΌ β 0 β (0...π)) |
36 | 8, 30, 35 | 3syl 18 |
. . . . . . 7
β’ (π β 0 β (0...π)) |
37 | 23, 28, 36 | rspcdva 3583 |
. . . . . 6
β’ (π β (πβ0) = (πβ0)) |
38 | 37 | adantr 482 |
. . . . 5
β’ ((π β§ π»(EulerPathsβπ)π) β (πβ0) = (πβ0)) |
39 | | eupth2eucrct.c |
. . . . . . 7
β’ (π β πΆ = (πβ0)) |
40 | 39 | eqcomd 2743 |
. . . . . 6
β’ (π β (πβ0) = πΆ) |
41 | 40 | adantr 482 |
. . . . 5
β’ ((π β§ π»(EulerPathsβπ)π) β (πβ0) = πΆ) |
42 | 14 | a1i 11 |
. . . . . . 7
β’ ((π β§ π»(EulerPathsβπ)π) β π = (π βͺ {β¨(π + 1), πΆβ©})) |
43 | 13 | fveq2i 6846 |
. . . . . . . . 9
β’
(β―βπ») =
(β―β(πΉ βͺ
{β¨π, π΅β©})) |
44 | 43 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π»(EulerPathsβπ)π) β (β―βπ») = (β―β(πΉ βͺ {β¨π, π΅β©}))) |
45 | | wrdfin 14421 |
. . . . . . . . . . . 12
β’ (πΉ β Word dom πΌ β πΉ β Fin) |
46 | 29, 45 | syl 17 |
. . . . . . . . . . 11
β’ (πΉ(WalksβπΊ)π β πΉ β Fin) |
47 | 8, 24, 46 | 3syl 18 |
. . . . . . . . . 10
β’ (π β πΉ β Fin) |
48 | 47 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π»(EulerPathsβπ)π) β πΉ β Fin) |
49 | | snfi 8989 |
. . . . . . . . . 10
β’
{β¨π, π΅β©} β
Fin |
50 | 49 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π»(EulerPathsβπ)π) β {β¨π, π΅β©} β Fin) |
51 | | wrddm 14410 |
. . . . . . . . . . . . 13
β’ (πΉ β Word dom πΌ β dom πΉ = (0..^(β―βπΉ))) |
52 | 8, 30, 51 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β dom πΉ = (0..^(β―βπΉ))) |
53 | | fzonel 13587 |
. . . . . . . . . . . . . . . 16
β’ Β¬
(β―βπΉ) β
(0..^(β―βπΉ)) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β Β¬ (β―βπΉ) β
(0..^(β―βπΉ))) |
55 | 9 | eleq1i 2829 |
. . . . . . . . . . . . . . 15
β’ (π β
(0..^(β―βπΉ))
β (β―βπΉ)
β (0..^(β―βπΉ))) |
56 | 54, 55 | sylnibr 329 |
. . . . . . . . . . . . . 14
β’ (π β Β¬ π β (0..^(β―βπΉ))) |
57 | | eleq2 2827 |
. . . . . . . . . . . . . . 15
β’ (dom
πΉ =
(0..^(β―βπΉ))
β (π β dom πΉ β π β (0..^(β―βπΉ)))) |
58 | 57 | notbid 318 |
. . . . . . . . . . . . . 14
β’ (dom
πΉ =
(0..^(β―βπΉ))
β (Β¬ π β dom
πΉ β Β¬ π β
(0..^(β―βπΉ)))) |
59 | 56, 58 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
β’ (π β (dom πΉ = (0..^(β―βπΉ)) β Β¬ π β dom πΉ)) |
60 | 9 | fvexi 6857 |
. . . . . . . . . . . . . . 15
β’ π β V |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β π β V) |
62 | 61, 5 | opeldmd 5863 |
. . . . . . . . . . . . 13
β’ (π β (β¨π, π΅β© β πΉ β π β dom πΉ)) |
63 | 59, 62 | nsyld 156 |
. . . . . . . . . . . 12
β’ (π β (dom πΉ = (0..^(β―βπΉ)) β Β¬ β¨π, π΅β© β πΉ)) |
64 | 52, 63 | mpd 15 |
. . . . . . . . . . 11
β’ (π β Β¬ β¨π, π΅β© β πΉ) |
65 | 64 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π»(EulerPathsβπ)π) β Β¬ β¨π, π΅β© β πΉ) |
66 | | disjsn 4673 |
. . . . . . . . . 10
β’ ((πΉ β© {β¨π, π΅β©}) = β
β Β¬ β¨π, π΅β© β πΉ) |
67 | 65, 66 | sylibr 233 |
. . . . . . . . 9
β’ ((π β§ π»(EulerPathsβπ)π) β (πΉ β© {β¨π, π΅β©}) = β
) |
68 | | hashun 14283 |
. . . . . . . . 9
β’ ((πΉ β Fin β§ {β¨π, π΅β©} β Fin β§ (πΉ β© {β¨π, π΅β©}) = β
) β
(β―β(πΉ βͺ
{β¨π, π΅β©})) = ((β―βπΉ) + (β―β{β¨π, π΅β©}))) |
69 | 48, 50, 67, 68 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π»(EulerPathsβπ)π) β (β―β(πΉ βͺ {β¨π, π΅β©})) = ((β―βπΉ) + (β―β{β¨π, π΅β©}))) |
70 | 9 | eqcomi 2746 |
. . . . . . . . . 10
β’
(β―βπΉ) =
π |
71 | | opex 5422 |
. . . . . . . . . . 11
β’
β¨π, π΅β© β V |
72 | | hashsng 14270 |
. . . . . . . . . . 11
β’
(β¨π, π΅β© β V β
(β―β{β¨π,
π΅β©}) =
1) |
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . 10
β’
(β―β{β¨π, π΅β©}) = 1 |
74 | 70, 73 | oveq12i 7370 |
. . . . . . . . 9
β’
((β―βπΉ) +
(β―β{β¨π,
π΅β©})) = (π + 1) |
75 | 74 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π»(EulerPathsβπ)π) β ((β―βπΉ) + (β―β{β¨π, π΅β©})) = (π + 1)) |
76 | 44, 69, 75 | 3eqtrd 2781 |
. . . . . . 7
β’ ((π β§ π»(EulerPathsβπ)π) β (β―βπ») = (π + 1)) |
77 | 42, 76 | fveq12d 6850 |
. . . . . 6
β’ ((π β§ π»(EulerPathsβπ)π) β (πβ(β―βπ»)) = ((π βͺ {β¨(π + 1), πΆβ©})β(π + 1))) |
78 | | ovexd 7393 |
. . . . . . . . 9
β’ (π β (π + 1) β V) |
79 | 1, 2, 3, 4, 5, 6, 7, 25, 9 | wlkp1lem1 28624 |
. . . . . . . . 9
β’ (π β Β¬ (π + 1) β dom π) |
80 | 78, 6, 79 | 3jca 1129 |
. . . . . . . 8
β’ (π β ((π + 1) β V β§ πΆ β π β§ Β¬ (π + 1) β dom π)) |
81 | 80 | adantr 482 |
. . . . . . 7
β’ ((π β§ π»(EulerPathsβπ)π) β ((π + 1) β V β§ πΆ β π β§ Β¬ (π + 1) β dom π)) |
82 | | fsnunfv 7134 |
. . . . . . 7
β’ (((π + 1) β V β§ πΆ β π β§ Β¬ (π + 1) β dom π) β ((π βͺ {β¨(π + 1), πΆβ©})β(π + 1)) = πΆ) |
83 | 81, 82 | syl 17 |
. . . . . 6
β’ ((π β§ π»(EulerPathsβπ)π) β ((π βͺ {β¨(π + 1), πΆβ©})β(π + 1)) = πΆ) |
84 | 77, 83 | eqtr2d 2778 |
. . . . 5
β’ ((π β§ π»(EulerPathsβπ)π) β πΆ = (πβ(β―βπ»))) |
85 | 38, 41, 84 | 3eqtrd 2781 |
. . . 4
β’ ((π β§ π»(EulerPathsβπ)π) β (πβ0) = (πβ(β―βπ»))) |
86 | | iscrct 28741 |
. . . 4
β’ (π»(Circuitsβπ)π β (π»(Trailsβπ)π β§ (πβ0) = (πβ(β―βπ»)))) |
87 | 20, 85, 86 | sylanbrc 584 |
. . 3
β’ ((π β§ π»(EulerPathsβπ)π) β π»(Circuitsβπ)π) |
88 | 18, 87 | jca 513 |
. 2
β’ ((π β§ π»(EulerPathsβπ)π) β (π»(EulerPathsβπ)π β§ π»(Circuitsβπ)π)) |
89 | 17, 88 | mpdan 686 |
1
β’ (π β (π»(EulerPathsβπ)π β§ π»(Circuitsβπ)π)) |