Proof of Theorem eupthp1
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 |
. . . 4
⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) |
9 | | eupthis1wlk 41380 |
. . . 4
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) |
11 | | eupthp1.n |
. . 3
⊢ 𝑁 = (#‘𝐹) |
12 | | eupthp1.e |
. . 3
⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) |
13 | | eupthp1.x |
. . 3
⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) |
14 | | eupthp1.u |
. . . 4
⊢
(iEdg‘𝑆) =
(𝐼 ∪ {〈𝐵, 𝐸〉}) |
15 | 14 | a1i 11 |
. . 3
⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) |
16 | | eupthp1.h |
. . 3
⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) |
17 | | eupthp1.q |
. . 3
⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) |
18 | | eupthp1.s |
. . . 4
⊢
(Vtx‘𝑆) =
𝑉 |
19 | 18 | a1i 11 |
. . 3
⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) |
20 | | eupthp1.l |
. . 3
⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶}) |
21 | 1, 2, 3, 4, 5, 6, 7, 10, 11, 12, 13, 15, 16, 17, 19, 20 | 1wlkp1 40890 |
. 2
⊢ (𝜑 → 𝐻(1Walks‘𝑆)𝑄) |
22 | 2 | eupthi 41371 |
. . . . 5
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → (𝐹(1Walks‘𝐺)𝑃 ∧ 𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼)) |
23 | 11 | eqcomi 2619 |
. . . . . . . . 9
⊢
(#‘𝐹) = 𝑁 |
24 | 23 | oveq2i 6560 |
. . . . . . . 8
⊢
(0..^(#‘𝐹)) =
(0..^𝑁) |
25 | | f1oeq2 6041 |
. . . . . . . 8
⊢
((0..^(#‘𝐹)) =
(0..^𝑁) → (𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼 ↔ 𝐹:(0..^𝑁)–1-1-onto→dom
𝐼)) |
26 | 24, 25 | ax-mp 5 |
. . . . . . 7
⊢ (𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼 ↔ 𝐹:(0..^𝑁)–1-1-onto→dom
𝐼) |
27 | 26 | biimpi 205 |
. . . . . 6
⊢ (𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼 → 𝐹:(0..^𝑁)–1-1-onto→dom
𝐼) |
28 | 27 | adantl 481 |
. . . . 5
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ 𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼) → 𝐹:(0..^𝑁)–1-1-onto→dom
𝐼) |
29 | 8, 22, 28 | 3syl 18 |
. . . 4
⊢ (𝜑 → 𝐹:(0..^𝑁)–1-1-onto→dom
𝐼) |
30 | | fvex 6113 |
. . . . . . 7
⊢
(#‘𝐹) ∈
V |
31 | 11, 30 | eqeltri 2684 |
. . . . . 6
⊢ 𝑁 ∈ V |
32 | | f1osng 6089 |
. . . . . 6
⊢ ((𝑁 ∈ V ∧ 𝐵 ∈ V) → {〈𝑁, 𝐵〉}:{𝑁}–1-1-onto→{𝐵}) |
33 | 31, 5, 32 | sylancr 694 |
. . . . 5
⊢ (𝜑 → {〈𝑁, 𝐵〉}:{𝑁}–1-1-onto→{𝐵}) |
34 | | dmsnopg 5524 |
. . . . . . 7
⊢ (𝐸 ∈ (Edg‘𝐺) → dom {〈𝐵, 𝐸〉} = {𝐵}) |
35 | 12, 34 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom {〈𝐵, 𝐸〉} = {𝐵}) |
36 | 35 | f1oeq3d 6047 |
. . . . 5
⊢ (𝜑 → ({〈𝑁, 𝐵〉}:{𝑁}–1-1-onto→dom
{〈𝐵, 𝐸〉} ↔ {〈𝑁, 𝐵〉}:{𝑁}–1-1-onto→{𝐵})) |
37 | 33, 36 | mpbird 246 |
. . . 4
⊢ (𝜑 → {〈𝑁, 𝐵〉}:{𝑁}–1-1-onto→dom
{〈𝐵, 𝐸〉}) |
38 | | fzodisjsn 12374 |
. . . . 5
⊢
((0..^𝑁) ∩
{𝑁}) =
∅ |
39 | 38 | a1i 11 |
. . . 4
⊢ (𝜑 → ((0..^𝑁) ∩ {𝑁}) = ∅) |
40 | 35 | ineq2d 3776 |
. . . . 5
⊢ (𝜑 → (dom 𝐼 ∩ dom {〈𝐵, 𝐸〉}) = (dom 𝐼 ∩ {𝐵})) |
41 | | disjsn 4192 |
. . . . . 6
⊢ ((dom
𝐼 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ dom 𝐼) |
42 | 7, 41 | sylibr 223 |
. . . . 5
⊢ (𝜑 → (dom 𝐼 ∩ {𝐵}) = ∅) |
43 | 40, 42 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (dom 𝐼 ∩ dom {〈𝐵, 𝐸〉}) = ∅) |
44 | | f1oun 6069 |
. . . 4
⊢ (((𝐹:(0..^𝑁)–1-1-onto→dom
𝐼 ∧ {〈𝑁, 𝐵〉}:{𝑁}–1-1-onto→dom
{〈𝐵, 𝐸〉}) ∧ (((0..^𝑁) ∩ {𝑁}) = ∅ ∧ (dom 𝐼 ∩ dom {〈𝐵, 𝐸〉}) = ∅)) → (𝐹 ∪ {〈𝑁, 𝐵〉}):((0..^𝑁) ∪ {𝑁})–1-1-onto→(dom
𝐼 ∪ dom {〈𝐵, 𝐸〉})) |
45 | 29, 37, 39, 43, 44 | syl22anc 1319 |
. . 3
⊢ (𝜑 → (𝐹 ∪ {〈𝑁, 𝐵〉}):((0..^𝑁) ∪ {𝑁})–1-1-onto→(dom
𝐼 ∪ dom {〈𝐵, 𝐸〉})) |
46 | 16 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉})) |
47 | 1, 2, 3, 4, 5, 6, 7, 10, 11, 12, 13, 15, 16 | 1wlkp1lem2 40883 |
. . . . . 6
⊢ (𝜑 → (#‘𝐻) = (𝑁 + 1)) |
48 | 47 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (0..^(#‘𝐻)) = (0..^(𝑁 + 1))) |
49 | | 1wlkcl 40820 |
. . . . . . . 8
⊢ (𝐹(1Walks‘𝐺)𝑃 → (#‘𝐹) ∈
ℕ0) |
50 | 11 | eleq1i 2679 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
↔ (#‘𝐹) ∈
ℕ0) |
51 | | elnn0uz 11601 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
52 | 50, 51 | sylbb1 226 |
. . . . . . . 8
⊢
((#‘𝐹) ∈
ℕ0 → 𝑁 ∈
(ℤ≥‘0)) |
53 | 49, 52 | syl 17 |
. . . . . . 7
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑁 ∈
(ℤ≥‘0)) |
54 | 8, 9, 53 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
55 | | fzosplitsn 12442 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
56 | 54, 55 | syl 17 |
. . . . 5
⊢ (𝜑 → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
57 | 48, 56 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (0..^(#‘𝐻)) = ((0..^𝑁) ∪ {𝑁})) |
58 | | dmun 5253 |
. . . . 5
⊢ dom
(𝐼 ∪ {〈𝐵, 𝐸〉}) = (dom 𝐼 ∪ dom {〈𝐵, 𝐸〉}) |
59 | 58 | a1i 11 |
. . . 4
⊢ (𝜑 → dom (𝐼 ∪ {〈𝐵, 𝐸〉}) = (dom 𝐼 ∪ dom {〈𝐵, 𝐸〉})) |
60 | 46, 57, 59 | f1oeq123d 6046 |
. . 3
⊢ (𝜑 → (𝐻:(0..^(#‘𝐻))–1-1-onto→dom
(𝐼 ∪ {〈𝐵, 𝐸〉}) ↔ (𝐹 ∪ {〈𝑁, 𝐵〉}):((0..^𝑁) ∪ {𝑁})–1-1-onto→(dom
𝐼 ∪ dom {〈𝐵, 𝐸〉}))) |
61 | 45, 60 | mpbird 246 |
. 2
⊢ (𝜑 → 𝐻:(0..^(#‘𝐻))–1-1-onto→dom
(𝐼 ∪ {〈𝐵, 𝐸〉})) |
62 | 1, 2, 3, 4, 5, 6, 7, 10, 11, 12, 13, 15, 16, 17, 19 | 1wlkp1lem4 40885 |
. . 3
⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) |
63 | 14 | eqcomi 2619 |
. . . 4
⊢ (𝐼 ∪ {〈𝐵, 𝐸〉}) = (iEdg‘𝑆) |
64 | 63 | iseupthf1o 41369 |
. . 3
⊢ ((𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(EulerPaths‘𝑆)𝑄 ↔ (𝐻(1Walks‘𝑆)𝑄 ∧ 𝐻:(0..^(#‘𝐻))–1-1-onto→dom
(𝐼 ∪ {〈𝐵, 𝐸〉})))) |
65 | 62, 64 | syl 17 |
. 2
⊢ (𝜑 → (𝐻(EulerPaths‘𝑆)𝑄 ↔ (𝐻(1Walks‘𝑆)𝑄 ∧ 𝐻:(0..^(#‘𝐻))–1-1-onto→dom
(𝐼 ∪ {〈𝐵, 𝐸〉})))) |
66 | 21, 61, 65 | mpbir2and 959 |
1
⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄) |