| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eupth2lem3 | Structured version Visualization version GIF version | ||
| Description: Lemma for eupth2 30661. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
| Ref | Expression |
|---|---|
| eupth2.v | ⊢ 𝑉 = (Vtx‘𝐺) |
| eupth2.i | ⊢ 𝐼 = (iEdg‘𝐺) |
| eupth2.g | ⊢ (𝜑 → 𝐺 ∈ UPGraph) |
| eupth2.f | ⊢ (𝜑 → Fun 𝐼) |
| eupth2.p | ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) |
| eupth2.h | ⊢ 𝐻 = 〈𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑁)))〉 |
| eupth2.x | ⊢ 𝑋 = 〈𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))〉 |
| eupth2.n | ⊢ (𝜑 → 𝑁 ∈ ℕ0) |
| eupth2.l | ⊢ (𝜑 → (𝑁 + 1) ≤ (♯‘𝐹)) |
| eupth2.u | ⊢ (𝜑 → 𝑈 ∈ 𝑉) |
| eupth2.o | ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐻)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) |
| Ref | Expression |
|---|---|
| eupth2lem3 | ⊢ (𝜑 → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |
| 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 30634 | . . . 4 ⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) | |
| 7 | wlkcl 30023 | . . . 4 ⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ ℕ0) | |
| 8 | 5, 6, 7 | 3syl 19 | . . 3 ⊢ (𝜑 → (♯‘𝐹) ∈ ℕ0) |
| 9 | eupth2.l | . . 3 ⊢ (𝜑 → (𝑁 + 1) ≤ (♯‘𝐹)) | |
| 10 | nn0p1elfzo 13748 | . . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ0 ∧ (𝑁 + 1) ≤ (♯‘𝐹)) → 𝑁 ∈ (0..^(♯‘𝐹))) | |
| 11 | 4, 8, 9, 10 | syl3anc 1398 | . 2 ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) |
| 12 | eupth2.u | . 2 ⊢ (𝜑 → 𝑈 ∈ 𝑉) | |
| 13 | eupthistrl 30633 | . . 3 ⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹(Trails‘𝐺)𝑃) | |
| 14 | 5, 13 | syl 18 | . 2 ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) |
| 15 | eupth2.h | . . . . 5 ⊢ 𝐻 = 〈𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑁)))〉 | |
| 16 | 15 | fveq2i 6888 | . . . 4 ⊢ (Vtx‘𝐻) = (Vtx‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑁)))〉) |
| 17 | 1 | fvexi 6899 | . . . . 5 ⊢ 𝑉 ∈ V |
| 18 | 2 | fvexi 6899 | . . . . . 6 ⊢ 𝐼 ∈ V |
| 19 | 18 | resex 6030 | . . . . 5 ⊢ (𝐼 ↾ (𝐹 “ (0..^𝑁))) ∈ V |
| 20 | 17, 19 | opvtxfvi 29414 | . . . 4 ⊢ (Vtx‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑁)))〉) = 𝑉 |
| 21 | 16, 20 | eqtri 2788 | . . 3 ⊢ (Vtx‘𝐻) = 𝑉 |
| 22 | 21 | a1i 11 | . 2 ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) |
| 23 | snex 5412 | . . . 4 ⊢ {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉} ∈ V | |
| 24 | 17, 23 | opvtxfvi 29414 | . . 3 ⊢ (Vtx‘〈𝑉, {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}〉) = 𝑉 |
| 25 | 24 | a1i 11 | . 2 ⊢ (𝜑 → (Vtx‘〈𝑉, {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}〉) = 𝑉) |
| 26 | eupth2.x | . . . . 5 ⊢ 𝑋 = 〈𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))〉 | |
| 27 | 26 | fveq2i 6888 | . . . 4 ⊢ (Vtx‘𝑋) = (Vtx‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))〉) |
| 28 | 18 | resex 6030 | . . . . 5 ⊢ (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1)))) ∈ V |
| 29 | 17, 28 | opvtxfvi 29414 | . . . 4 ⊢ (Vtx‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))〉) = 𝑉 |
| 30 | 27, 29 | eqtri 2788 | . . 3 ⊢ (Vtx‘𝑋) = 𝑉 |
| 31 | 30 | a1i 11 | . 2 ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) |
| 32 | 15 | fveq2i 6888 | . . . 4 ⊢ (iEdg‘𝐻) = (iEdg‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑁)))〉) |
| 33 | 17, 19 | opiedgfvi 29415 | . . . 4 ⊢ (iEdg‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑁)))〉) = (𝐼 ↾ (𝐹 “ (0..^𝑁))) |
| 34 | 32, 33 | eqtri 2788 | . . 3 ⊢ (iEdg‘𝐻) = (𝐼 ↾ (𝐹 “ (0..^𝑁))) |
| 35 | 34 | a1i 11 | . 2 ⊢ (𝜑 → (iEdg‘𝐻) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) |
| 36 | 17, 23 | opiedgfvi 29415 | . . 3 ⊢ (iEdg‘〈𝑉, {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}〉) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉} |
| 37 | 36 | a1i 11 | . 2 ⊢ (𝜑 → (iEdg‘〈𝑉, {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}〉) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) |
| 38 | 26 | fveq2i 6888 | . . . 4 ⊢ (iEdg‘𝑋) = (iEdg‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))〉) |
| 39 | 17, 28 | opiedgfvi 29415 | . . . 4 ⊢ (iEdg‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))〉) = (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1)))) |
| 40 | 38, 39 | eqtri 2788 | . . 3 ⊢ (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1)))) |
| 41 | 4 | nn0zd 12631 | . . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 42 | fzval3 13780 | . . . . . . 7 ⊢ (𝑁 ∈ ℤ → (0...𝑁) = (0..^(𝑁 + 1))) | |
| 43 | 42 | eqcomd 2771 | . . . . . 6 ⊢ (𝑁 ∈ ℤ → (0..^(𝑁 + 1)) = (0...𝑁)) |
| 44 | 41, 43 | syl 18 | . . . . 5 ⊢ (𝜑 → (0..^(𝑁 + 1)) = (0...𝑁)) |
| 45 | 44 | imaeq2d 6064 | . . . 4 ⊢ (𝜑 → (𝐹 “ (0..^(𝑁 + 1))) = (𝐹 “ (0...𝑁))) |
| 46 | 45 | reseq2d 5980 | . . 3 ⊢ (𝜑 → (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1)))) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) |
| 47 | 40, 46 | eqtrid 2812 | . 2 ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) |
| 48 | eupth2.o | . 2 ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐻)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) | |
| 49 | 2fveq3 6890 | . . . 4 ⊢ (𝑘 = 𝑁 → (𝐼‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘𝑁))) | |
| 50 | fveq2 6885 | . . . . 5 ⊢ (𝑘 = 𝑁 → (𝑃‘𝑘) = (𝑃‘𝑁)) | |
| 51 | fvoveq1 7442 | . . . . 5 ⊢ (𝑘 = 𝑁 → (𝑃‘(𝑘 + 1)) = (𝑃‘(𝑁 + 1))) | |
| 52 | 50, 51 | preq12d 4709 | . . . 4 ⊢ (𝑘 = 𝑁 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}) |
| 53 | 49, 52 | eqeq12d 2781 | . . 3 ⊢ (𝑘 = 𝑁 → ((𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))})) |
| 54 | eupth2.g | . . . 4 ⊢ (𝜑 → 𝐺 ∈ UPGraph) | |
| 55 | 5, 6 | syl 18 | . . . 4 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) |
| 56 | 2 | upgrwlkedg 30049 | . . . 4 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
| 57 | 54, 55, 56 | syl2anc 596 | . . 3 ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
| 58 | 53, 57, 11 | rspcdva 3584 | . 2 ⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}) |
| 59 | 1, 2, 3, 11, 12, 14, 22, 25, 31, 35, 37, 47, 48, 58 | eupth2lem3lem7 30656 | 1 ⊢ (𝜑 → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 = wceq 1570 ∈ wcel 2146 ∀wral 3081 {crab 3418 ∅c0 4286 ifcif 4489 {csn 4591 {cpr 4593 〈cop 4597 class class class wbr 5111 ↾ cres 5665 “ cima 5666 Fun wfun 6534 ‘cfv 6540 (class class class)co 7419 0cc0 11115 1c1 11116 + caddc 11118 ≤ cle 11259 2c2 12310 ℕ0cn0 12519 ℤcz 12606 ...cfz 13551 ..^cfzo 13699 ♯chash 14384 ∥ cdvds 16332 Vtxcvtx 29401 iEdgciedg 29402 UPGraphcupgr 29485 VtxDegcvtxdg 29873 Walkscwlks 30004 Trailsctrls 30100 EulerPathsceupth 30619 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11171 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191 ax-pre-mulgt0 11192 ax-pre-sup 11193 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-ifp 1079 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-oadd 8463 df-er 8700 df-map 8832 df-pm 8833 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-sup 9409 df-inf 9410 df-dju 9903 df-card 9941 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-le 11264 df-sub 11458 df-neg 11459 df-div 11887 df-nn 12249 df-2 12318 df-3 12319 df-n0 12520 df-xnn0 12593 df-z 12607 df-uz 12879 df-rp 13033 df-xadd 13154 df-fz 13552 df-fzo 13700 df-seq 14056 df-exp 14116 df-hash 14385 df-word 14569 df-cj 15174 df-re 15175 df-im 15176 df-sqrt 15310 df-abs 15311 df-dvds 16333 df-vtx 29403 df-iedg 29404 df-edg 29453 df-uhgr 29463 df-ushgr 29464 df-upgr 29487 df-uspgr 29558 df-vtxdg 29874 df-wlks 30007 df-trls 30102 df-eupth 30620 |
| This theorem is used by: eupth2lems 30660 |
| Copyright terms: Public domain | W3C validator |