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
⊢ (𝜑 → 𝐵 ∈ V) |
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 41384 |
. 2
⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄) |
18 | | simpr 476 |
. . 3
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → 𝐻(EulerPaths‘𝑆)𝑄) |
19 | | eupthistrl 41379 |
. . . . 5
⊢ (𝐻(EulerPaths‘𝑆)𝑄 → 𝐻(TrailS‘𝑆)𝑄) |
20 | 19 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → 𝐻(TrailS‘𝑆)𝑄) |
21 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 0 → (𝑄‘𝑘) = (𝑄‘0)) |
22 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
23 | 21, 22 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑘 = 0 → ((𝑄‘𝑘) = (𝑃‘𝑘) ↔ (𝑄‘0) = (𝑃‘0))) |
24 | | eupthis1wlk 41380 |
. . . . . . . . 9
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
25 | 8, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) |
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 | 1wlkp1lem5 40886 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)(𝑄‘𝑘) = (𝑃‘𝑘)) |
29 | 2 | 1wlkf 40819 |
. . . . . . . . 9
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
30 | 24, 29 | syl 17 |
. . . . . . . 8
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
31 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝐹 ∈ Word dom 𝐼 → (#‘𝐹) ∈
ℕ0) |
32 | 9 | eleq1i 2679 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
↔ (#‘𝐹) ∈
ℕ0) |
33 | | 0elfz 12305 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0...𝑁)) |
34 | 32, 33 | sylbir 224 |
. . . . . . . . 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 3288 |
. . . . . 6
⊢ (𝜑 → (𝑄‘0) = (𝑃‘0)) |
38 | 37 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → (𝑄‘0) = (𝑃‘0)) |
39 | | eupth2eucrct.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 = (𝑃‘0)) |
40 | 39 | eqcomd 2616 |
. . . . . 6
⊢ (𝜑 → (𝑃‘0) = 𝐶) |
41 | 40 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → (𝑃‘0) = 𝐶) |
42 | 14 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉})) |
43 | 13 | fveq2i 6106 |
. . . . . . . . 9
⊢
(#‘𝐻) =
(#‘(𝐹 ∪
{〈𝑁, 𝐵〉})) |
44 | 43 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → (#‘𝐻) = (#‘(𝐹 ∪ {〈𝑁, 𝐵〉}))) |
45 | | wrdfin 13178 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹 ∈ Fin) |
46 | 29, 45 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝐹 ∈ Fin) |
47 | 8, 24, 46 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ Fin) |
48 | 47 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → 𝐹 ∈ Fin) |
49 | | snfi 7923 |
. . . . . . . . . 10
⊢
{〈𝑁, 𝐵〉} ∈
Fin |
50 | 49 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → {〈𝑁, 𝐵〉} ∈ Fin) |
51 | | wrddm 13167 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ Word dom 𝐼 → dom 𝐹 = (0..^(#‘𝐹))) |
52 | 8, 30, 51 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐹 = (0..^(#‘𝐹))) |
53 | | fzonel 12352 |
. . . . . . . . . . . . . . . 16
⊢ ¬
(#‘𝐹) ∈
(0..^(#‘𝐹)) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ (#‘𝐹) ∈ (0..^(#‘𝐹))) |
55 | 9 | eleq1i 2679 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ (0..^(#‘𝐹)) ↔ (#‘𝐹) ∈ (0..^(#‘𝐹))) |
56 | 54, 55 | sylnibr 318 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝑁 ∈ (0..^(#‘𝐹))) |
57 | | eleq2 2677 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝐹 = (0..^(#‘𝐹)) → (𝑁 ∈ dom 𝐹 ↔ 𝑁 ∈ (0..^(#‘𝐹)))) |
58 | 57 | notbid 307 |
. . . . . . . . . . . . . 14
⊢ (dom
𝐹 = (0..^(#‘𝐹)) → (¬ 𝑁 ∈ dom 𝐹 ↔ ¬ 𝑁 ∈ (0..^(#‘𝐹)))) |
59 | 56, 58 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (dom 𝐹 = (0..^(#‘𝐹)) → ¬ 𝑁 ∈ dom 𝐹)) |
60 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(#‘𝐹) ∈
V |
61 | 9, 60 | eqeltri 2684 |
. . . . . . . . . . . . . . 15
⊢ 𝑁 ∈ V |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ V) |
63 | 62, 5 | opeldmd 5249 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (〈𝑁, 𝐵〉 ∈ 𝐹 → 𝑁 ∈ dom 𝐹)) |
64 | 59, 63 | nsyld 153 |
. . . . . . . . . . . 12
⊢ (𝜑 → (dom 𝐹 = (0..^(#‘𝐹)) → ¬ 〈𝑁, 𝐵〉 ∈ 𝐹)) |
65 | 52, 64 | mpd 15 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 〈𝑁, 𝐵〉 ∈ 𝐹) |
66 | 65 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → ¬ 〈𝑁, 𝐵〉 ∈ 𝐹) |
67 | | disjsn 4192 |
. . . . . . . . . 10
⊢ ((𝐹 ∩ {〈𝑁, 𝐵〉}) = ∅ ↔ ¬ 〈𝑁, 𝐵〉 ∈ 𝐹) |
68 | 66, 67 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → (𝐹 ∩ {〈𝑁, 𝐵〉}) = ∅) |
69 | | hashun 13032 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Fin ∧ {〈𝑁, 𝐵〉} ∈ Fin ∧ (𝐹 ∩ {〈𝑁, 𝐵〉}) = ∅) → (#‘(𝐹 ∪ {〈𝑁, 𝐵〉})) = ((#‘𝐹) + (#‘{〈𝑁, 𝐵〉}))) |
70 | 48, 50, 68, 69 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → (#‘(𝐹 ∪ {〈𝑁, 𝐵〉})) = ((#‘𝐹) + (#‘{〈𝑁, 𝐵〉}))) |
71 | 9 | eqcomi 2619 |
. . . . . . . . . 10
⊢
(#‘𝐹) = 𝑁 |
72 | | opex 4859 |
. . . . . . . . . . 11
⊢
〈𝑁, 𝐵〉 ∈ V |
73 | | hashsng 13020 |
. . . . . . . . . . 11
⊢
(〈𝑁, 𝐵〉 ∈ V →
(#‘{〈𝑁, 𝐵〉}) = 1) |
74 | 72, 73 | ax-mp 5 |
. . . . . . . . . 10
⊢
(#‘{〈𝑁,
𝐵〉}) =
1 |
75 | 71, 74 | oveq12i 6561 |
. . . . . . . . 9
⊢
((#‘𝐹) +
(#‘{〈𝑁, 𝐵〉})) = (𝑁 + 1) |
76 | 75 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → ((#‘𝐹) + (#‘{〈𝑁, 𝐵〉})) = (𝑁 + 1)) |
77 | 44, 70, 76 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → (#‘𝐻) = (𝑁 + 1)) |
78 | 42, 77 | fveq12d 6109 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → (𝑄‘(#‘𝐻)) = ((𝑃 ∪ {〈(𝑁 + 1), 𝐶〉})‘(𝑁 + 1))) |
79 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑁 + 1) ∈ V |
80 | 79 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 + 1) ∈ V) |
81 | 1, 2, 3, 4, 5, 6, 7, 25, 9 | 1wlkp1lem1 40882 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (𝑁 + 1) ∈ dom 𝑃) |
82 | 80, 6, 81 | 3jca 1235 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 + 1) ∈ V ∧ 𝐶 ∈ 𝑉 ∧ ¬ (𝑁 + 1) ∈ dom 𝑃)) |
83 | 82 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → ((𝑁 + 1) ∈ V ∧ 𝐶 ∈ 𝑉 ∧ ¬ (𝑁 + 1) ∈ dom 𝑃)) |
84 | | fsnunfv 6358 |
. . . . . . 7
⊢ (((𝑁 + 1) ∈ V ∧ 𝐶 ∈ 𝑉 ∧ ¬ (𝑁 + 1) ∈ dom 𝑃) → ((𝑃 ∪ {〈(𝑁 + 1), 𝐶〉})‘(𝑁 + 1)) = 𝐶) |
85 | 83, 84 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → ((𝑃 ∪ {〈(𝑁 + 1), 𝐶〉})‘(𝑁 + 1)) = 𝐶) |
86 | 78, 85 | eqtr2d 2645 |
. . . . 5
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → 𝐶 = (𝑄‘(#‘𝐻))) |
87 | 38, 41, 86 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → (𝑄‘0) = (𝑄‘(#‘𝐻))) |
88 | | eupthis1wlk 41380 |
. . . . . 6
⊢ (𝐻(EulerPaths‘𝑆)𝑄 → 𝐻(1Walks‘𝑆)𝑄) |
89 | | wlkv 40815 |
. . . . . 6
⊢ (𝐻(1Walks‘𝑆)𝑄 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) |
90 | | isCrct 40996 |
. . . . . 6
⊢ ((𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(CircuitS‘𝑆)𝑄 ↔ (𝐻(TrailS‘𝑆)𝑄 ∧ (𝑄‘0) = (𝑄‘(#‘𝐻))))) |
91 | 88, 89, 90 | 3syl 18 |
. . . . 5
⊢ (𝐻(EulerPaths‘𝑆)𝑄 → (𝐻(CircuitS‘𝑆)𝑄 ↔ (𝐻(TrailS‘𝑆)𝑄 ∧ (𝑄‘0) = (𝑄‘(#‘𝐻))))) |
92 | 91 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → (𝐻(CircuitS‘𝑆)𝑄 ↔ (𝐻(TrailS‘𝑆)𝑄 ∧ (𝑄‘0) = (𝑄‘(#‘𝐻))))) |
93 | 20, 87, 92 | mpbir2and 959 |
. . 3
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → 𝐻(CircuitS‘𝑆)𝑄) |
94 | 18, 93 | jca 553 |
. 2
⊢ ((𝜑 ∧ 𝐻(EulerPaths‘𝑆)𝑄) → (𝐻(EulerPaths‘𝑆)𝑄 ∧ 𝐻(CircuitS‘𝑆)𝑄)) |
95 | 17, 94 | mpdan 699 |
1
⊢ (𝜑 → (𝐻(EulerPaths‘𝑆)𝑄 ∧ 𝐻(CircuitS‘𝑆)𝑄)) |