| Step | Hyp | Ref
| Expression |
| 1 | | upgrop 29111 |
. . . 4
⊢ (𝐺 ∈ UPGraph →
〈(Vtx‘𝐺),
(iEdg‘𝐺)〉 ∈
UPGraph) |
| 2 | | fvex 6919 |
. . . . . 6
⊢
(iEdg‘𝐺)
∈ V |
| 3 | | fvex 6919 |
. . . . . . 7
⊢
(iEdg‘〈𝑘,
𝑒〉) ∈
V |
| 4 | 3 | resex 6047 |
. . . . . 6
⊢
((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ V |
| 5 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑒 = (iEdg‘𝐺) → (𝑒 ∈ Fin ↔ (iEdg‘𝐺) ∈ Fin)) |
| 6 | 5 | adantl 481 |
. . . . . . 7
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (𝑒 ∈ Fin ↔ (iEdg‘𝐺) ∈ Fin)) |
| 7 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → 𝑘 = (Vtx‘𝐺)) |
| 8 | | oveq12 7440 |
. . . . . . . . . . 11
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (𝑘VtxDeg𝑒) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))) |
| 9 | 8 | fveq1d 6908 |
. . . . . . . . . 10
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → ((𝑘VtxDeg𝑒)‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣)) |
| 10 | 9 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) ∧ 𝑣 ∈ 𝑘) → ((𝑘VtxDeg𝑒)‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣)) |
| 11 | 7, 10 | sumeq12dv 15742 |
. . . . . . . 8
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣)) |
| 12 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑒 = (iEdg‘𝐺) → (♯‘𝑒) = (♯‘(iEdg‘𝐺))) |
| 13 | 12 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑒 = (iEdg‘𝐺) → (2 · (♯‘𝑒)) = (2 ·
(♯‘(iEdg‘𝐺)))) |
| 14 | 13 | adantl 481 |
. . . . . . . 8
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (2 · (♯‘𝑒)) = (2 ·
(♯‘(iEdg‘𝐺)))) |
| 15 | 11, 14 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)) ↔ Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 ·
(♯‘(iEdg‘𝐺))))) |
| 16 | 6, 15 | imbi12d 344 |
. . . . . 6
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → ((𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))) ↔ ((iEdg‘𝐺) ∈ Fin → Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 ·
(♯‘(iEdg‘𝐺)))))) |
| 17 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑒 = 𝑓 → (𝑒 ∈ Fin ↔ 𝑓 ∈ Fin)) |
| 18 | 17 | adantl 481 |
. . . . . . 7
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑒 ∈ Fin ↔ 𝑓 ∈ Fin)) |
| 19 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → 𝑘 = 𝑤) |
| 20 | | oveq12 7440 |
. . . . . . . . . . . 12
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑘VtxDeg𝑒) = (𝑤VtxDeg𝑓)) |
| 21 | | df-ov 7434 |
. . . . . . . . . . . 12
⊢ (𝑤VtxDeg𝑓) = (VtxDeg‘〈𝑤, 𝑓〉) |
| 22 | 20, 21 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑘VtxDeg𝑒) = (VtxDeg‘〈𝑤, 𝑓〉)) |
| 23 | 22 | fveq1d 6908 |
. . . . . . . . . 10
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘〈𝑤, 𝑓〉)‘𝑣)) |
| 24 | 23 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) ∧ 𝑣 ∈ 𝑘) → ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘〈𝑤, 𝑓〉)‘𝑣)) |
| 25 | 19, 24 | sumeq12dv 15742 |
. . . . . . . 8
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ 𝑤 ((VtxDeg‘〈𝑤, 𝑓〉)‘𝑣)) |
| 26 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑓 → (♯‘𝑒) = (♯‘𝑓)) |
| 27 | 26 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑒 = 𝑓 → (2 · (♯‘𝑒)) = (2 ·
(♯‘𝑓))) |
| 28 | 27 | adantl 481 |
. . . . . . . 8
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (2 · (♯‘𝑒)) = (2 ·
(♯‘𝑓))) |
| 29 | 25, 28 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)) ↔ Σ𝑣 ∈ 𝑤 ((VtxDeg‘〈𝑤, 𝑓〉)‘𝑣) = (2 · (♯‘𝑓)))) |
| 30 | 18, 29 | imbi12d 344 |
. . . . . 6
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → ((𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))) ↔ (𝑓 ∈ Fin → Σ𝑣 ∈ 𝑤 ((VtxDeg‘〈𝑤, 𝑓〉)‘𝑣) = (2 · (♯‘𝑓))))) |
| 31 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑘 ∈ V |
| 32 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑒 ∈ V |
| 33 | 31, 32 | opvtxfvi 29026 |
. . . . . . . 8
⊢
(Vtx‘〈𝑘,
𝑒〉) = 𝑘 |
| 34 | 33 | eqcomi 2746 |
. . . . . . 7
⊢ 𝑘 = (Vtx‘〈𝑘, 𝑒〉) |
| 35 | | eqid 2737 |
. . . . . . 7
⊢
(iEdg‘〈𝑘,
𝑒〉) =
(iEdg‘〈𝑘, 𝑒〉) |
| 36 | | eqid 2737 |
. . . . . . 7
⊢ {𝑖 ∈ dom
(iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉
((iEdg‘〈𝑘, 𝑒〉)‘𝑖)} = {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)} |
| 37 | | eqid 2737 |
. . . . . . 7
⊢
〈(𝑘 ∖
{𝑛}),
((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom
(iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉
((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉 = 〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉 |
| 38 | 34, 35, 36, 37 | upgrres 29323 |
. . . . . 6
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑛 ∈ 𝑘) → 〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉 ∈ UPGraph) |
| 39 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) → (𝑓 ∈ Fin ↔ ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ Fin)) |
| 40 | 39 | adantl 481 |
. . . . . . 7
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})) → (𝑓 ∈ Fin ↔ ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ Fin)) |
| 41 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})) → 𝑤 = (𝑘 ∖ {𝑛})) |
| 42 | | opeq12 4875 |
. . . . . . . . . . . 12
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})) → 〈𝑤, 𝑓〉 = 〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉) |
| 43 | 42 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})) → (VtxDeg‘〈𝑤, 𝑓〉) = (VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)) |
| 44 | 43 | fveq1d 6908 |
. . . . . . . . . 10
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})) → ((VtxDeg‘〈𝑤, 𝑓〉)‘𝑣) = ((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣)) |
| 45 | 44 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})) ∧ 𝑣 ∈ 𝑤) → ((VtxDeg‘〈𝑤, 𝑓〉)‘𝑣) = ((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣)) |
| 46 | 41, 45 | sumeq12dv 15742 |
. . . . . . . 8
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})) → Σ𝑣 ∈ 𝑤 ((VtxDeg‘〈𝑤, 𝑓〉)‘𝑣) = Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣)) |
| 47 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) → (♯‘𝑓) = (♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}))) |
| 48 | 47 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) → (2 · (♯‘𝑓)) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})))) |
| 49 | 48 | adantl 481 |
. . . . . . . 8
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})) → (2 · (♯‘𝑓)) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})))) |
| 50 | 46, 49 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})) → (Σ𝑣 ∈ 𝑤 ((VtxDeg‘〈𝑤, 𝑓〉)‘𝑣) = (2 · (♯‘𝑓)) ↔ Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}))))) |
| 51 | 40, 50 | imbi12d 344 |
. . . . . 6
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})) → ((𝑓 ∈ Fin → Σ𝑣 ∈ 𝑤 ((VtxDeg‘〈𝑤, 𝑓〉)‘𝑣) = (2 · (♯‘𝑓))) ↔
(((iEdg‘〈𝑘,
𝑒〉) ↾ {𝑖 ∈ dom
(iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉
((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})))))) |
| 52 | | hasheq0 14402 |
. . . . . . . . 9
⊢ (𝑘 ∈ V →
((♯‘𝑘) = 0
↔ 𝑘 =
∅)) |
| 53 | 52 | elv 3485 |
. . . . . . . 8
⊢
((♯‘𝑘) =
0 ↔ 𝑘 =
∅) |
| 54 | | 2t0e0 12435 |
. . . . . . . . . 10
⊢ (2
· 0) = 0 |
| 55 | 54 | a1i 11 |
. . . . . . . . 9
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑘 = ∅) → (2
· 0) = 0) |
| 56 | 31, 32 | opiedgfvi 29027 |
. . . . . . . . . . . . 13
⊢
(iEdg‘〈𝑘,
𝑒〉) = 𝑒 |
| 57 | 56 | eqcomi 2746 |
. . . . . . . . . . . 12
⊢ 𝑒 = (iEdg‘〈𝑘, 𝑒〉) |
| 58 | | upgruhgr 29119 |
. . . . . . . . . . . . . 14
⊢
(〈𝑘, 𝑒〉 ∈ UPGraph →
〈𝑘, 𝑒〉 ∈ UHGraph) |
| 59 | 58 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑘 = ∅) →
〈𝑘, 𝑒〉 ∈ UHGraph) |
| 60 | 34 | eqeq1i 2742 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = ∅ ↔
(Vtx‘〈𝑘, 𝑒〉) =
∅) |
| 61 | | uhgr0vb 29089 |
. . . . . . . . . . . . . 14
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
(Vtx‘〈𝑘, 𝑒〉) = ∅) →
(〈𝑘, 𝑒〉 ∈ UHGraph ↔
(iEdg‘〈𝑘, 𝑒〉) =
∅)) |
| 62 | 60, 61 | sylan2b 594 |
. . . . . . . . . . . . 13
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑘 = ∅) →
(〈𝑘, 𝑒〉 ∈ UHGraph ↔
(iEdg‘〈𝑘, 𝑒〉) =
∅)) |
| 63 | 59, 62 | mpbid 232 |
. . . . . . . . . . . 12
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑘 = ∅) →
(iEdg‘〈𝑘, 𝑒〉) =
∅) |
| 64 | 57, 63 | eqtrid 2789 |
. . . . . . . . . . 11
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑘 = ∅) → 𝑒 = ∅) |
| 65 | | hasheq0 14402 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ V →
((♯‘𝑒) = 0
↔ 𝑒 =
∅)) |
| 66 | 65 | elv 3485 |
. . . . . . . . . . 11
⊢
((♯‘𝑒) =
0 ↔ 𝑒 =
∅) |
| 67 | 64, 66 | sylibr 234 |
. . . . . . . . . 10
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑘 = ∅) →
(♯‘𝑒) =
0) |
| 68 | 67 | oveq2d 7447 |
. . . . . . . . 9
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑘 = ∅) → (2
· (♯‘𝑒))
= (2 · 0)) |
| 69 | | sumeq1 15725 |
. . . . . . . . . . 11
⊢ (𝑘 = ∅ → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ ∅ ((𝑘VtxDeg𝑒)‘𝑣)) |
| 70 | | sum0 15757 |
. . . . . . . . . . 11
⊢
Σ𝑣 ∈
∅ ((𝑘VtxDeg𝑒)‘𝑣) = 0 |
| 71 | 69, 70 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = 0) |
| 72 | 71 | adantl 481 |
. . . . . . . . 9
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑘 = ∅) →
Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = 0) |
| 73 | 55, 68, 72 | 3eqtr4rd 2788 |
. . . . . . . 8
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑘 = ∅) →
Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))) |
| 74 | 53, 73 | sylan2b 594 |
. . . . . . 7
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
(♯‘𝑘) = 0)
→ Σ𝑣 ∈
𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))) |
| 75 | 74 | a1d 25 |
. . . . . 6
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
(♯‘𝑘) = 0)
→ (𝑒 ∈ Fin →
Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))) |
| 76 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ ((𝑦 + 1) = (♯‘𝑘) → ((𝑦 + 1) ∈ ℕ0 ↔
(♯‘𝑘) ∈
ℕ0)) |
| 77 | 76 | eqcoms 2745 |
. . . . . . . . . 10
⊢
((♯‘𝑘) =
(𝑦 + 1) → ((𝑦 + 1) ∈ ℕ0
↔ (♯‘𝑘)
∈ ℕ0)) |
| 78 | 77 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
(♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘) → ((𝑦 + 1) ∈ ℕ0 ↔
(♯‘𝑘) ∈
ℕ0)) |
| 79 | | hashclb 14397 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ V → (𝑘 ∈ Fin ↔
(♯‘𝑘) ∈
ℕ0)) |
| 80 | 79 | biimprd 248 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ V →
((♯‘𝑘) ∈
ℕ0 → 𝑘 ∈ Fin)) |
| 81 | 80 | elv 3485 |
. . . . . . . . . 10
⊢
((♯‘𝑘)
∈ ℕ0 → 𝑘 ∈ Fin) |
| 82 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∖ {𝑛}) = (𝑘 ∖ {𝑛}) |
| 83 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)} |
| 84 | 56 | dmeqi 5915 |
. . . . . . . . . . . . . . . . . 18
⊢ dom
(iEdg‘〈𝑘, 𝑒〉) = dom 𝑒 |
| 85 | 84 | rabeqi 3450 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑖 ∈ dom
(iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉
((iEdg‘〈𝑘, 𝑒〉)‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)} |
| 86 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ dom 𝑒 → 𝑛 = 𝑛) |
| 87 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ dom 𝑒 → (iEdg‘〈𝑘, 𝑒〉) = 𝑒) |
| 88 | 87 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ dom 𝑒 → ((iEdg‘〈𝑘, 𝑒〉)‘𝑖) = (𝑒‘𝑖)) |
| 89 | 86, 88 | neleq12d 3051 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ dom 𝑒 → (𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖) ↔ 𝑛 ∉ (𝑒‘𝑖))) |
| 90 | 89 | rabbiia 3440 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)} |
| 91 | 85, 90 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢ {𝑖 ∈ dom
(iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉
((iEdg‘〈𝑘, 𝑒〉)‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)} |
| 92 | 56, 91 | reseq12i 5995 |
. . . . . . . . . . . . . . 15
⊢
((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) = (𝑒 ↾ {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)}) |
| 93 | 34, 57, 82, 83, 92, 37 | finsumvtxdg2sstep 29567 |
. . . . . . . . . . . . . 14
⊢
(((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑛 ∈ 𝑘) ∧ (𝑘 ∈ Fin ∧ 𝑒 ∈ Fin)) →
((((iEdg‘〈𝑘,
𝑒〉) ↾ {𝑖 ∈ dom
(iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉
((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})))) → Σ𝑣 ∈ 𝑘 ((VtxDeg‘〈𝑘, 𝑒〉)‘𝑣) = (2 · (♯‘𝑒)))) |
| 94 | | df-ov 7434 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘VtxDeg𝑒) = (VtxDeg‘〈𝑘, 𝑒〉) |
| 95 | 94 | fveq1i 6907 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘〈𝑘, 𝑒〉)‘𝑣) |
| 96 | 95 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ 𝑘 → ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘〈𝑘, 𝑒〉)‘𝑣)) |
| 97 | 96 | sumeq2i 15734 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑣 ∈
𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ 𝑘 ((VtxDeg‘〈𝑘, 𝑒〉)‘𝑣) |
| 98 | 97 | eqeq1i 2742 |
. . . . . . . . . . . . . 14
⊢
(Σ𝑣 ∈
𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)) ↔ Σ𝑣 ∈ 𝑘 ((VtxDeg‘〈𝑘, 𝑒〉)‘𝑣) = (2 · (♯‘𝑒))) |
| 99 | 93, 98 | imbitrrdi 252 |
. . . . . . . . . . . . 13
⊢
(((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑛 ∈ 𝑘) ∧ (𝑘 ∈ Fin ∧ 𝑒 ∈ Fin)) →
((((iEdg‘〈𝑘,
𝑒〉) ↾ {𝑖 ∈ dom
(iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉
((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})))) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))) |
| 100 | 99 | exp32 420 |
. . . . . . . . . . . 12
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑛 ∈ 𝑘) → (𝑘 ∈ Fin → (𝑒 ∈ Fin → ((((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})))) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))))) |
| 101 | 100 | com34 91 |
. . . . . . . . . . 11
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
𝑛 ∈ 𝑘) → (𝑘 ∈ Fin → ((((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})))) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))))) |
| 102 | 101 | 3adant2 1132 |
. . . . . . . . . 10
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
(♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘) → (𝑘 ∈ Fin → ((((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})))) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))))) |
| 103 | 81, 102 | syl5 34 |
. . . . . . . . 9
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
(♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘) → ((♯‘𝑘) ∈ ℕ0 →
((((iEdg‘〈𝑘,
𝑒〉) ↾ {𝑖 ∈ dom
(iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉
((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})))) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))))) |
| 104 | 78, 103 | sylbid 240 |
. . . . . . . 8
⊢
((〈𝑘, 𝑒〉 ∈ UPGraph ∧
(♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘) → ((𝑦 + 1) ∈ ℕ0 →
((((iEdg‘〈𝑘,
𝑒〉) ↾ {𝑖 ∈ dom
(iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉
((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})))) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))))) |
| 105 | 104 | impcom 407 |
. . . . . . 7
⊢ (((𝑦 + 1) ∈ ℕ0
∧ (〈𝑘, 𝑒〉 ∈ UPGraph ∧
(♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘)) → ((((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})))) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))))) |
| 106 | 105 | imp 406 |
. . . . . 6
⊢ ((((𝑦 + 1) ∈ ℕ0
∧ (〈𝑘, 𝑒〉 ∈ UPGraph ∧
(♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘)) ∧ (((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘〈(𝑘 ∖ {𝑛}), ((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)})〉)‘𝑣) = (2 ·
(♯‘((iEdg‘〈𝑘, 𝑒〉) ↾ {𝑖 ∈ dom (iEdg‘〈𝑘, 𝑒〉) ∣ 𝑛 ∉ ((iEdg‘〈𝑘, 𝑒〉)‘𝑖)}))))) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))) |
| 107 | 2, 4, 16, 30, 38, 51, 75, 106 | opfi1ind 14551 |
. . . . 5
⊢
((〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ∈ UPGraph ∧
(Vtx‘𝐺) ∈ Fin)
→ ((iEdg‘𝐺)
∈ Fin → Σ𝑣
∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 ·
(♯‘(iEdg‘𝐺))))) |
| 108 | 107 | ex 412 |
. . . 4
⊢
(〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ∈ UPGraph →
((Vtx‘𝐺) ∈ Fin
→ ((iEdg‘𝐺)
∈ Fin → Σ𝑣
∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 ·
(♯‘(iEdg‘𝐺)))))) |
| 109 | 1, 108 | syl 17 |
. . 3
⊢ (𝐺 ∈ UPGraph →
((Vtx‘𝐺) ∈ Fin
→ ((iEdg‘𝐺)
∈ Fin → Σ𝑣
∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 ·
(♯‘(iEdg‘𝐺)))))) |
| 110 | | sumvtxdg2size.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
| 111 | 110 | eleq1i 2832 |
. . . 4
⊢ (𝑉 ∈ Fin ↔
(Vtx‘𝐺) ∈
Fin) |
| 112 | 111 | a1i 11 |
. . 3
⊢ (𝐺 ∈ UPGraph → (𝑉 ∈ Fin ↔
(Vtx‘𝐺) ∈
Fin)) |
| 113 | | sumvtxdg2size.i |
. . . . . 6
⊢ 𝐼 = (iEdg‘𝐺) |
| 114 | 113 | eleq1i 2832 |
. . . . 5
⊢ (𝐼 ∈ Fin ↔
(iEdg‘𝐺) ∈
Fin) |
| 115 | 114 | a1i 11 |
. . . 4
⊢ (𝐺 ∈ UPGraph → (𝐼 ∈ Fin ↔
(iEdg‘𝐺) ∈
Fin)) |
| 116 | 110 | a1i 11 |
. . . . . 6
⊢ (𝐺 ∈ UPGraph → 𝑉 = (Vtx‘𝐺)) |
| 117 | | sumvtxdg2size.d |
. . . . . . . . 9
⊢ 𝐷 = (VtxDeg‘𝐺) |
| 118 | | vtxdgop 29488 |
. . . . . . . . 9
⊢ (𝐺 ∈ UPGraph →
(VtxDeg‘𝐺) =
((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))) |
| 119 | 117, 118 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝐺 ∈ UPGraph → 𝐷 = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))) |
| 120 | 119 | fveq1d 6908 |
. . . . . . 7
⊢ (𝐺 ∈ UPGraph → (𝐷‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣)) |
| 121 | 120 | adantr 480 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧ 𝑣 ∈ 𝑉) → (𝐷‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣)) |
| 122 | 116, 121 | sumeq12dv 15742 |
. . . . 5
⊢ (𝐺 ∈ UPGraph →
Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣)) |
| 123 | 113 | fveq2i 6909 |
. . . . . . 7
⊢
(♯‘𝐼) =
(♯‘(iEdg‘𝐺)) |
| 124 | 123 | oveq2i 7442 |
. . . . . 6
⊢ (2
· (♯‘𝐼))
= (2 · (♯‘(iEdg‘𝐺))) |
| 125 | 124 | a1i 11 |
. . . . 5
⊢ (𝐺 ∈ UPGraph → (2
· (♯‘𝐼))
= (2 · (♯‘(iEdg‘𝐺)))) |
| 126 | 122, 125 | eqeq12d 2753 |
. . . 4
⊢ (𝐺 ∈ UPGraph →
(Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)) ↔ Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 ·
(♯‘(iEdg‘𝐺))))) |
| 127 | 115, 126 | imbi12d 344 |
. . 3
⊢ (𝐺 ∈ UPGraph → ((𝐼 ∈ Fin → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼))) ↔ ((iEdg‘𝐺) ∈ Fin → Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 ·
(♯‘(iEdg‘𝐺)))))) |
| 128 | 109, 112,
127 | 3imtr4d 294 |
. 2
⊢ (𝐺 ∈ UPGraph → (𝑉 ∈ Fin → (𝐼 ∈ Fin → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼))))) |
| 129 | 128 | 3imp 1111 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼))) |