Proof of Theorem eupth2lem3lem3
Step | Hyp | Ref
| Expression |
1 | | trlsegvdeg.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
2 | | fveq2 6272 |
. . . . . . . 8
⊢ (𝑥 = 𝑈 → ((VtxDeg‘𝑋)‘𝑥) = ((VtxDeg‘𝑋)‘𝑈)) |
3 | 2 | breq2d 4740 |
. . . . . . 7
⊢ (𝑥 = 𝑈 → (2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝑋)‘𝑈))) |
4 | 3 | notbid 307 |
. . . . . 6
⊢ (𝑥 = 𝑈 → (¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈))) |
5 | 4 | elrab3 3438 |
. . . . 5
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈))) |
6 | 1, 5 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈))) |
7 | | eupth2lem3.o |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) |
8 | 7 | eleq2d 2757 |
. . . 4
⊢ (𝜑 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥)} ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) |
9 | 6, 8 | bitr3d 270 |
. . 3
⊢ (𝜑 → (¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) |
10 | 9 | adantr 472 |
. 2
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) |
11 | | 2z 11490 |
. . . . . 6
⊢ 2 ∈
ℤ |
12 | 11 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → 2 ∈
ℤ) |
13 | | trlsegvdeg.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
14 | | trlsegvdeg.i |
. . . . . . . 8
⊢ 𝐼 = (iEdg‘𝐺) |
15 | | trlsegvdeg.f |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐼) |
16 | | trlsegvdeg.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) |
17 | | trlsegvdeg.w |
. . . . . . . 8
⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) |
18 | | trlsegvdeg.vx |
. . . . . . . 8
⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) |
19 | | trlsegvdeg.vy |
. . . . . . . 8
⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) |
20 | | trlsegvdeg.vz |
. . . . . . . 8
⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) |
21 | | trlsegvdeg.ix |
. . . . . . . 8
⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) |
22 | | trlsegvdeg.iy |
. . . . . . . 8
⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) |
23 | | trlsegvdeg.iz |
. . . . . . . 8
⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) |
24 | 13, 14, 15, 16, 1, 17, 18, 19, 20, 21, 22, 23 | eupth2lem3lem1 27269 |
. . . . . . 7
⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈
ℕ0) |
25 | 24 | nn0zd 11561 |
. . . . . 6
⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℤ) |
26 | 25 | adantr 472 |
. . . . 5
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → ((VtxDeg‘𝑋)‘𝑈) ∈ ℤ) |
27 | 13, 14, 15, 16, 1, 17, 18, 19, 20, 21, 22, 23 | eupth2lem3lem2 27270 |
. . . . . . 7
⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈
ℕ0) |
28 | 27 | nn0zd 11561 |
. . . . . 6
⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℤ) |
29 | 28 | adantr 472 |
. . . . 5
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → ((VtxDeg‘𝑌)‘𝑈) ∈ ℤ) |
30 | | iddvds 15086 |
. . . . . . . 8
⊢ (2 ∈
ℤ → 2 ∥ 2) |
31 | 11, 30 | ax-mp 5 |
. . . . . . 7
⊢ 2 ∥
2 |
32 | 19 | ad2antrr 764 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (Vtx‘𝑌) = 𝑉) |
33 | | fvexd 6284 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (𝐹‘𝑁) ∈ V) |
34 | 1 | ad2antrr 764 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → 𝑈 ∈ 𝑉) |
35 | 22 | ad2antrr 764 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) |
36 | | eupth2lem3lem3.e |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) |
37 | 36 | adantr 472 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) |
38 | | ifptru 1061 |
. . . . . . . . . . . . . 14
⊢ ((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) ↔ (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)})) |
39 | 38 | adantl 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) ↔ (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)})) |
40 | 37, 39 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}) |
41 | | sneq 4263 |
. . . . . . . . . . . . 13
⊢ ((𝑃‘𝑁) = 𝑈 → {(𝑃‘𝑁)} = {𝑈}) |
42 | 41 | eqcoms 2700 |
. . . . . . . . . . . 12
⊢ (𝑈 = (𝑃‘𝑁) → {(𝑃‘𝑁)} = {𝑈}) |
43 | 40, 42 | sylan9eq 2746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (𝐼‘(𝐹‘𝑁)) = {𝑈}) |
44 | 43 | opeq2d 4484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → 〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉 = 〈(𝐹‘𝑁), {𝑈}〉) |
45 | 44 | sneqd 4265 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉} = {〈(𝐹‘𝑁), {𝑈}〉}) |
46 | 35, 45 | eqtrd 2726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (iEdg‘𝑌) = {〈(𝐹‘𝑁), {𝑈}〉}) |
47 | 32, 33, 34, 46 | 1loopgrvd2 26498 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → ((VtxDeg‘𝑌)‘𝑈) = 2) |
48 | 31, 47 | syl5breqr 4766 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → 2 ∥ ((VtxDeg‘𝑌)‘𝑈)) |
49 | | dvds0 15088 |
. . . . . . . 8
⊢ (2 ∈
ℤ → 2 ∥ 0) |
50 | 11, 49 | ax-mp 5 |
. . . . . . 7
⊢ 2 ∥
0 |
51 | 19 | ad2antrr 764 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → (Vtx‘𝑌) = 𝑉) |
52 | | fvexd 6284 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → (𝐹‘𝑁) ∈ V) |
53 | 13, 14, 15, 16, 1, 17 | trlsegvdeglem1 27261 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃‘𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉)) |
54 | 53 | simpld 477 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃‘𝑁) ∈ 𝑉) |
55 | 54 | ad2antrr 764 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → (𝑃‘𝑁) ∈ 𝑉) |
56 | 22 | adantr 472 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) |
57 | 40 | opeq2d 4484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → 〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉 = 〈(𝐹‘𝑁), {(𝑃‘𝑁)}〉) |
58 | 57 | sneqd 4265 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉} = {〈(𝐹‘𝑁), {(𝑃‘𝑁)}〉}) |
59 | 56, 58 | eqtrd 2726 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (iEdg‘𝑌) = {〈(𝐹‘𝑁), {(𝑃‘𝑁)}〉}) |
60 | 59 | adantr 472 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → (iEdg‘𝑌) = {〈(𝐹‘𝑁), {(𝑃‘𝑁)}〉}) |
61 | 1 | adantr 472 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → 𝑈 ∈ 𝑉) |
62 | 61 | anim1i 593 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → (𝑈 ∈ 𝑉 ∧ 𝑈 ≠ (𝑃‘𝑁))) |
63 | | eldifsn 4393 |
. . . . . . . . 9
⊢ (𝑈 ∈ (𝑉 ∖ {(𝑃‘𝑁)}) ↔ (𝑈 ∈ 𝑉 ∧ 𝑈 ≠ (𝑃‘𝑁))) |
64 | 62, 63 | sylibr 224 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → 𝑈 ∈ (𝑉 ∖ {(𝑃‘𝑁)})) |
65 | 51, 52, 55, 60, 64 | 1loopgrvd0 26499 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → ((VtxDeg‘𝑌)‘𝑈) = 0) |
66 | 50, 65 | syl5breqr 4766 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → 2 ∥ ((VtxDeg‘𝑌)‘𝑈)) |
67 | 48, 66 | pm2.61dane 2951 |
. . . . 5
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → 2 ∥
((VtxDeg‘𝑌)‘𝑈)) |
68 | | dvdsadd2b 15119 |
. . . . 5
⊢ ((2
∈ ℤ ∧ ((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ (((VtxDeg‘𝑌)‘𝑈) ∈ ℤ ∧ 2 ∥
((VtxDeg‘𝑌)‘𝑈))) → (2 ∥ ((VtxDeg‘𝑋)‘𝑈) ↔ 2 ∥ (((VtxDeg‘𝑌)‘𝑈) + ((VtxDeg‘𝑋)‘𝑈)))) |
69 | 12, 26, 29, 67, 68 | syl112anc 1411 |
. . . 4
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥
((VtxDeg‘𝑋)‘𝑈) ↔ 2 ∥ (((VtxDeg‘𝑌)‘𝑈) + ((VtxDeg‘𝑋)‘𝑈)))) |
70 | 27 | nn0cnd 11434 |
. . . . . . 7
⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℂ) |
71 | 24 | nn0cnd 11434 |
. . . . . . 7
⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℂ) |
72 | 70, 71 | addcomd 10319 |
. . . . . 6
⊢ (𝜑 → (((VtxDeg‘𝑌)‘𝑈) + ((VtxDeg‘𝑋)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈))) |
73 | 72 | breq2d 4740 |
. . . . 5
⊢ (𝜑 → (2 ∥
(((VtxDeg‘𝑌)‘𝑈) + ((VtxDeg‘𝑋)‘𝑈)) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)))) |
74 | 73 | adantr 472 |
. . . 4
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥
(((VtxDeg‘𝑌)‘𝑈) + ((VtxDeg‘𝑋)‘𝑈)) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)))) |
75 | 69, 74 | bitrd 268 |
. . 3
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥
((VtxDeg‘𝑋)‘𝑈) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)))) |
76 | 75 | notbid 307 |
. 2
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈) ↔ ¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)))) |
77 | | simpr 479 |
. . . . 5
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) |
78 | 77 | eqeq2d 2702 |
. . . 4
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → ((𝑃‘0) = (𝑃‘𝑁) ↔ (𝑃‘0) = (𝑃‘(𝑁 + 1)))) |
79 | 77 | preq2d 4350 |
. . . 4
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → {(𝑃‘0), (𝑃‘𝑁)} = {(𝑃‘0), (𝑃‘(𝑁 + 1))}) |
80 | 78, 79 | ifbieq2d 4187 |
. . 3
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) = if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})) |
81 | 80 | eleq2d 2757 |
. 2
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |
82 | 10, 76, 81 | 3bitr3d 298 |
1
⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |