Step | Hyp | Ref
| Expression |
1 | | upgrop 28354 |
. . . 4
⊢ (𝐺 ∈ UPGraph →
⟨(Vtx‘𝐺),
(iEdg‘𝐺)⟩ ∈
UPGraph) |
2 | | fvex 6905 |
. . . . . 6
⊢
(iEdg‘𝐺)
∈ V |
3 | | fvex 6905 |
. . . . . . 7
⊢
(iEdg‘⟨𝑘,
𝑒⟩) ∈
V |
4 | 3 | resex 6030 |
. . . . . 6
⊢
((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ V |
5 | | eleq1 2822 |
. . . . . . . 8
⊢ (𝑒 = (iEdg‘𝐺) → (𝑒 ∈ Fin ↔ (iEdg‘𝐺) ∈ Fin)) |
6 | 5 | adantl 483 |
. . . . . . 7
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (𝑒 ∈ Fin ↔ (iEdg‘𝐺) ∈ Fin)) |
7 | | simpl 484 |
. . . . . . . . 9
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → 𝑘 = (Vtx‘𝐺)) |
8 | | oveq12 7418 |
. . . . . . . . . . 11
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (𝑘VtxDeg𝑒) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))) |
9 | 8 | fveq1d 6894 |
. . . . . . . . . 10
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → ((𝑘VtxDeg𝑒)‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣)) |
10 | 9 | adantr 482 |
. . . . . . . . 9
⊢ (((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) ∧ 𝑣 ∈ 𝑘) → ((𝑘VtxDeg𝑒)‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣)) |
11 | 7, 10 | sumeq12dv 15652 |
. . . . . . . 8
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣)) |
12 | | fveq2 6892 |
. . . . . . . . . 10
⊢ (𝑒 = (iEdg‘𝐺) → (♯‘𝑒) = (♯‘(iEdg‘𝐺))) |
13 | 12 | oveq2d 7425 |
. . . . . . . . 9
⊢ (𝑒 = (iEdg‘𝐺) → (2 · (♯‘𝑒)) = (2 ·
(♯‘(iEdg‘𝐺)))) |
14 | 13 | adantl 483 |
. . . . . . . 8
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (2 · (♯‘𝑒)) = (2 ·
(♯‘(iEdg‘𝐺)))) |
15 | 11, 14 | eqeq12d 2749 |
. . . . . . 7
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)) ↔ Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 ·
(♯‘(iEdg‘𝐺))))) |
16 | 6, 15 | imbi12d 345 |
. . . . . 6
⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → ((𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))) ↔ ((iEdg‘𝐺) ∈ Fin → Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 ·
(♯‘(iEdg‘𝐺)))))) |
17 | | eleq1 2822 |
. . . . . . . 8
⊢ (𝑒 = 𝑓 → (𝑒 ∈ Fin ↔ 𝑓 ∈ Fin)) |
18 | 17 | adantl 483 |
. . . . . . 7
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑒 ∈ Fin ↔ 𝑓 ∈ Fin)) |
19 | | simpl 484 |
. . . . . . . . 9
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → 𝑘 = 𝑤) |
20 | | oveq12 7418 |
. . . . . . . . . . . 12
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑘VtxDeg𝑒) = (𝑤VtxDeg𝑓)) |
21 | | df-ov 7412 |
. . . . . . . . . . . 12
⊢ (𝑤VtxDeg𝑓) = (VtxDeg‘⟨𝑤, 𝑓⟩) |
22 | 20, 21 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑘VtxDeg𝑒) = (VtxDeg‘⟨𝑤, 𝑓⟩)) |
23 | 22 | fveq1d 6894 |
. . . . . . . . . 10
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣)) |
24 | 23 | adantr 482 |
. . . . . . . . 9
⊢ (((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) ∧ 𝑣 ∈ 𝑘) → ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣)) |
25 | 19, 24 | sumeq12dv 15652 |
. . . . . . . 8
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣)) |
26 | | fveq2 6892 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑓 → (♯‘𝑒) = (♯‘𝑓)) |
27 | 26 | oveq2d 7425 |
. . . . . . . . 9
⊢ (𝑒 = 𝑓 → (2 · (♯‘𝑒)) = (2 ·
(♯‘𝑓))) |
28 | 27 | adantl 483 |
. . . . . . . 8
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (2 · (♯‘𝑒)) = (2 ·
(♯‘𝑓))) |
29 | 25, 28 | eqeq12d 2749 |
. . . . . . 7
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)) ↔ Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = (2 · (♯‘𝑓)))) |
30 | 18, 29 | imbi12d 345 |
. . . . . 6
⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → ((𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))) ↔ (𝑓 ∈ Fin → Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = (2 · (♯‘𝑓))))) |
31 | | vex 3479 |
. . . . . . . . 9
⊢ 𝑘 ∈ V |
32 | | vex 3479 |
. . . . . . . . 9
⊢ 𝑒 ∈ V |
33 | 31, 32 | opvtxfvi 28269 |
. . . . . . . 8
⊢
(Vtx‘⟨𝑘,
𝑒⟩) = 𝑘 |
34 | 33 | eqcomi 2742 |
. . . . . . 7
⊢ 𝑘 = (Vtx‘⟨𝑘, 𝑒⟩) |
35 | | eqid 2733 |
. . . . . . 7
⊢
(iEdg‘⟨𝑘,
𝑒⟩) =
(iEdg‘⟨𝑘, 𝑒⟩) |
36 | | eqid 2733 |
. . . . . . 7
⊢ {𝑖 ∈ dom
(iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉
((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} = {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} |
37 | | eqid 2733 |
. . . . . . 7
⊢
⟨(𝑘 ∖
{𝑛}),
((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom
(iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉
((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩ = ⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩ |
38 | 34, 35, 36, 37 | upgrres 28563 |
. . . . . 6
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
𝑛 ∈ 𝑘) → ⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩ ∈ UPGraph) |
39 | | eleq1 2822 |
. . . . . . . 8
⊢ (𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) → (𝑓 ∈ Fin ↔ ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin)) |
40 | 39 | adantl 483 |
. . . . . . 7
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → (𝑓 ∈ Fin ↔ ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin)) |
41 | | simpl 484 |
. . . . . . . . 9
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → 𝑤 = (𝑘 ∖ {𝑛})) |
42 | | opeq12 4876 |
. . . . . . . . . . . 12
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → ⟨𝑤, 𝑓⟩ = ⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩) |
43 | 42 | fveq2d 6896 |
. . . . . . . . . . 11
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → (VtxDeg‘⟨𝑤, 𝑓⟩) = (VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)) |
44 | 43 | fveq1d 6894 |
. . . . . . . . . 10
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = ((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣)) |
45 | 44 | adantr 482 |
. . . . . . . . 9
⊢ (((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) ∧ 𝑣 ∈ 𝑤) → ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = ((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣)) |
46 | 41, 45 | sumeq12dv 15652 |
. . . . . . . 8
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣)) |
47 | | fveq2 6892 |
. . . . . . . . . 10
⊢ (𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) → (♯‘𝑓) = (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}))) |
48 | 47 | oveq2d 7425 |
. . . . . . . . 9
⊢ (𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) → (2 · (♯‘𝑓)) = (2 ·
(♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) |
49 | 48 | adantl 483 |
. . . . . . . 8
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → (2 · (♯‘𝑓)) = (2 ·
(♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) |
50 | 46, 49 | eqeq12d 2749 |
. . . . . . 7
⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → (Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = (2 · (♯‘𝑓)) ↔ Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 ·
(♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}))))) |
51 | 40, 50 | imbi12d 345 |
. . . . . 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 14323 |
. . . . . . . . 9
⊢ (𝑘 ∈ V →
((♯‘𝑘) = 0
↔ 𝑘 =
∅)) |
53 | 52 | elv 3481 |
. . . . . . . 8
⊢
((♯‘𝑘) =
0 ↔ 𝑘 =
∅) |
54 | | 2t0e0 12381 |
. . . . . . . . . 10
⊢ (2
· 0) = 0 |
55 | 54 | a1i 11 |
. . . . . . . . 9
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
𝑘 = ∅) → (2
· 0) = 0) |
56 | 31, 32 | opiedgfvi 28270 |
. . . . . . . . . . . . 13
⊢
(iEdg‘⟨𝑘,
𝑒⟩) = 𝑒 |
57 | 56 | eqcomi 2742 |
. . . . . . . . . . . 12
⊢ 𝑒 = (iEdg‘⟨𝑘, 𝑒⟩) |
58 | | upgruhgr 28362 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑘, 𝑒⟩ ∈ UPGraph →
⟨𝑘, 𝑒⟩ ∈ UHGraph) |
59 | 58 | adantr 482 |
. . . . . . . . . . . . 13
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
𝑘 = ∅) →
⟨𝑘, 𝑒⟩ ∈ UHGraph) |
60 | 34 | eqeq1i 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = ∅ ↔
(Vtx‘⟨𝑘, 𝑒⟩) =
∅) |
61 | | uhgr0vb 28332 |
. . . . . . . . . . . . . 14
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
(Vtx‘⟨𝑘, 𝑒⟩) = ∅) →
(⟨𝑘, 𝑒⟩ ∈ UHGraph ↔
(iEdg‘⟨𝑘, 𝑒⟩) =
∅)) |
62 | 60, 61 | sylan2b 595 |
. . . . . . . . . . . . 13
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
𝑘 = ∅) →
(⟨𝑘, 𝑒⟩ ∈ UHGraph ↔
(iEdg‘⟨𝑘, 𝑒⟩) =
∅)) |
63 | 59, 62 | mpbid 231 |
. . . . . . . . . . . 12
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
𝑘 = ∅) →
(iEdg‘⟨𝑘, 𝑒⟩) =
∅) |
64 | 57, 63 | eqtrid 2785 |
. . . . . . . . . . 11
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
𝑘 = ∅) → 𝑒 = ∅) |
65 | | hasheq0 14323 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ V →
((♯‘𝑒) = 0
↔ 𝑒 =
∅)) |
66 | 65 | elv 3481 |
. . . . . . . . . . 11
⊢
((♯‘𝑒) =
0 ↔ 𝑒 =
∅) |
67 | 64, 66 | sylibr 233 |
. . . . . . . . . 10
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
𝑘 = ∅) →
(♯‘𝑒) =
0) |
68 | 67 | oveq2d 7425 |
. . . . . . . . 9
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
𝑘 = ∅) → (2
· (♯‘𝑒))
= (2 · 0)) |
69 | | sumeq1 15635 |
. . . . . . . . . . 11
⊢ (𝑘 = ∅ → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ ∅ ((𝑘VtxDeg𝑒)‘𝑣)) |
70 | | sum0 15667 |
. . . . . . . . . . 11
⊢
Σ𝑣 ∈
∅ ((𝑘VtxDeg𝑒)‘𝑣) = 0 |
71 | 69, 70 | eqtrdi 2789 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = 0) |
72 | 71 | adantl 483 |
. . . . . . . . 9
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
𝑘 = ∅) →
Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = 0) |
73 | 55, 68, 72 | 3eqtr4rd 2784 |
. . . . . . . 8
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
𝑘 = ∅) →
Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))) |
74 | 53, 73 | sylan2b 595 |
. . . . . . 7
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
(♯‘𝑘) = 0)
→ Σ𝑣 ∈
𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))) |
75 | 74 | a1d 25 |
. . . . . 6
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
(♯‘𝑘) = 0)
→ (𝑒 ∈ Fin →
Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))) |
76 | | eleq1 2822 |
. . . . . . . . . . 11
⊢ ((𝑦 + 1) = (♯‘𝑘) → ((𝑦 + 1) ∈ ℕ0 ↔
(♯‘𝑘) ∈
ℕ0)) |
77 | 76 | eqcoms 2741 |
. . . . . . . . . 10
⊢
((♯‘𝑘) =
(𝑦 + 1) → ((𝑦 + 1) ∈ ℕ0
↔ (♯‘𝑘)
∈ ℕ0)) |
78 | 77 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢
((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
(♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘) → ((𝑦 + 1) ∈ ℕ0 ↔
(♯‘𝑘) ∈
ℕ0)) |
79 | | hashclb 14318 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ V → (𝑘 ∈ Fin ↔
(♯‘𝑘) ∈
ℕ0)) |
80 | 79 | biimprd 247 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ V →
((♯‘𝑘) ∈
ℕ0 → 𝑘 ∈ Fin)) |
81 | 80 | elv 3481 |
. . . . . . . . . 10
⊢
((♯‘𝑘)
∈ ℕ0 → 𝑘 ∈ Fin) |
82 | | eqid 2733 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∖ {𝑛}) = (𝑘 ∖ {𝑛}) |
83 | | eqid 2733 |
. . . . . . . . . . . . . . 15
⊢ {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)} |
84 | 56 | dmeqi 5905 |
. . . . . . . . . . . . . . . . . 18
⊢ dom
(iEdg‘⟨𝑘, 𝑒⟩) = dom 𝑒 |
85 | 84 | rabeqi 3446 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑖 ∈ dom
(iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉
((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} |
86 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ dom 𝑒 → 𝑛 = 𝑛) |
87 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ dom 𝑒 → (iEdg‘⟨𝑘, 𝑒⟩) = 𝑒) |
88 | 87 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ dom 𝑒 → ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖) = (𝑒‘𝑖)) |
89 | 86, 88 | neleq12d 3052 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ dom 𝑒 → (𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖) ↔ 𝑛 ∉ (𝑒‘𝑖))) |
90 | 89 | rabbiia 3437 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)} |
91 | 85, 90 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
⊢ {𝑖 ∈ dom
(iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉
((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)} |
92 | 56, 91 | reseq12i 5980 |
. . . . . . . . . . . . . . 15
⊢
((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) = (𝑒 ↾ {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)}) |
93 | 34, 57, 82, 83, 92, 37 | finsumvtxdg2sstep 28806 |
. . . . . . . . . . . . . 14
⊢
(((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
𝑛 ∈ 𝑘) ∧ (𝑘 ∈ Fin ∧ 𝑒 ∈ Fin)) →
((((iEdg‘⟨𝑘,
𝑒⟩) ↾ {𝑖 ∈ dom
(iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉
((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 ·
(♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) → Σ𝑣 ∈ 𝑘 ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣) = (2 · (♯‘𝑒)))) |
94 | | df-ov 7412 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘VtxDeg𝑒) = (VtxDeg‘⟨𝑘, 𝑒⟩) |
95 | 94 | fveq1i 6893 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣) |
96 | 95 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ 𝑘 → ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣)) |
97 | 96 | sumeq2i 15645 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑣 ∈
𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ 𝑘 ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣) |
98 | 97 | eqeq1i 2738 |
. . . . . . . . . . . . . 14
⊢
(Σ𝑣 ∈
𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)) ↔ Σ𝑣 ∈ 𝑘 ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣) = (2 · (♯‘𝑒))) |
99 | 93, 98 | imbitrrdi 251 |
. . . . . . . . . . . . 13
⊢
(((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧
𝑛 ∈ 𝑘) ∧ (𝑘 ∈ Fin ∧ 𝑒 ∈ Fin)) →
((((iEdg‘⟨𝑘,
𝑒⟩) ↾ {𝑖 ∈ dom
(iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉
((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 ·
(♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))) |
100 | 99 | exp32 422 |
. . . . . . . . . . . 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 239 |
. . . . . . . 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 409 |
. . . . . . 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 408 |
. . . . . 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 14463 |
. . . . 5
⊢
((⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ UPGraph ∧
(Vtx‘𝐺) ∈ Fin)
→ ((iEdg‘𝐺)
∈ Fin → Σ𝑣
∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 ·
(♯‘(iEdg‘𝐺))))) |
108 | 107 | ex 414 |
. . . 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 2825 |
. . . 4
⊢ (𝑉 ∈ Fin ↔
(Vtx‘𝐺) ∈
Fin) |
112 | 111 | a1i 11 |
. . 3
⊢ (𝐺 ∈ UPGraph → (𝑉 ∈ Fin ↔
(Vtx‘𝐺) ∈
Fin)) |
113 | | sumvtxdg2size.i |
. . . . . 6
⊢ 𝐼 = (iEdg‘𝐺) |
114 | 113 | eleq1i 2825 |
. . . . 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 28727 |
. . . . . . . . 9
⊢ (𝐺 ∈ UPGraph →
(VtxDeg‘𝐺) =
((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))) |
119 | 117, 118 | eqtrid 2785 |
. . . . . . . 8
⊢ (𝐺 ∈ UPGraph → 𝐷 = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))) |
120 | 119 | fveq1d 6894 |
. . . . . . 7
⊢ (𝐺 ∈ UPGraph → (𝐷‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣)) |
121 | 120 | adantr 482 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧ 𝑣 ∈ 𝑉) → (𝐷‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣)) |
122 | 116, 121 | sumeq12dv 15652 |
. . . . 5
⊢ (𝐺 ∈ UPGraph →
Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣)) |
123 | 113 | fveq2i 6895 |
. . . . . . 7
⊢
(♯‘𝐼) =
(♯‘(iEdg‘𝐺)) |
124 | 123 | oveq2i 7420 |
. . . . . 6
⊢ (2
· (♯‘𝐼))
= (2 · (♯‘(iEdg‘𝐺))) |
125 | 124 | a1i 11 |
. . . . 5
⊢ (𝐺 ∈ UPGraph → (2
· (♯‘𝐼))
= (2 · (♯‘(iEdg‘𝐺)))) |
126 | 122, 125 | eqeq12d 2749 |
. . . 4
⊢ (𝐺 ∈ UPGraph →
(Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)) ↔ Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 ·
(♯‘(iEdg‘𝐺))))) |
127 | 115, 126 | imbi12d 345 |
. . 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 1112 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼))) |