Description: The sum of the degrees of all vertices of a finite pseudograph of finite size is twice the size of the pseudograph. See equation (1) in section I.1 in Bollobas p. 4. Here, the "proof" is simply the statement "Since each edge has two endvertices, the sum of the degrees is exactly twice the number of edges". The formal proof of this theorem (for pseudographs) is much more complicated, taking also the used auxiliary theorems into account. The proof for a (finite) simple graph (see fusgr1th ) would be shorter, but nevertheless still laborious. Although this theorem would hold also for infinite pseudographs and pseudographs of infinite size, the proof of this most general version (see theorem "sumvtxdg2size" below) would require many more auxiliary theorems (e.g., the extension of the sum sum_ over an arbitrary set).
I dedicate this theorem and its proof to Norman Megill, who deceased too early on December 9, 2021. This proof is an example for the rigor which was the main motivation for Norman Megill to invent and develop Metamath, see section 1.1.6 "Rigor" on page 19 of the Metamath book: "... it is usually assumed in mathematical literature that the person reading the proof is a mathematician familiar with the specialty being described, and that the missing steps are obvious to such a reader or at least the reader is capable of filling them in." I filled in the missing steps of Bollobas' proof as Norm would have liked it... (Contributed by Alexander van der Vekens, 19-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | sumvtxdg2size.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| sumvtxdg2size.i | ⊢ 𝐼 = ( iEdg ‘ 𝐺 ) | ||
| sumvtxdg2size.d | ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 ) | ||
| Assertion | finsumvtxdg2size | ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐼 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sumvtxdg2size.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| 2 | sumvtxdg2size.i | ⊢ 𝐼 = ( iEdg ‘ 𝐺 ) | |
| 3 | sumvtxdg2size.d | ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 ) | |
| 4 | upgrop | ⊢ ( 𝐺 ∈ UPGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph ) | |
| 5 | fvex | ⊢ ( iEdg ‘ 𝐺 ) ∈ V | |
| 6 | fvex | ⊢ ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∈ V | |
| 7 | 6 | resex | ⊢ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ V |
| 8 | eleq1 | ⊢ ( 𝑒 = ( iEdg ‘ 𝐺 ) → ( 𝑒 ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) ) | |
| 9 | 8 | adantl | ⊢ ( ( 𝑘 = ( Vtx ‘ 𝐺 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → ( 𝑒 ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) ) |
| 10 | simpl | ⊢ ( ( 𝑘 = ( Vtx ‘ 𝐺 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → 𝑘 = ( Vtx ‘ 𝐺 ) ) | |
| 11 | oveq12 | ⊢ ( ( 𝑘 = ( Vtx ‘ 𝐺 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → ( 𝑘 VtxDeg 𝑒 ) = ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ) | |
| 12 | 11 | fveq1d | ⊢ ( ( 𝑘 = ( Vtx ‘ 𝐺 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) ) |
| 13 | 12 | adantr | ⊢ ( ( ( 𝑘 = ( Vtx ‘ 𝐺 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) ∧ 𝑣 ∈ 𝑘 ) → ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) ) |
| 14 | 10 13 | sumeq12dv | ⊢ ( ( 𝑘 = ( Vtx ‘ 𝐺 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = Σ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) ) |
| 15 | fveq2 | ⊢ ( 𝑒 = ( iEdg ‘ 𝐺 ) → ( ♯ ‘ 𝑒 ) = ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) ) | |
| 16 | 15 | oveq2d | ⊢ ( 𝑒 = ( iEdg ‘ 𝐺 ) → ( 2 · ( ♯ ‘ 𝑒 ) ) = ( 2 · ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) ) ) |
| 17 | 16 | adantl | ⊢ ( ( 𝑘 = ( Vtx ‘ 𝐺 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → ( 2 · ( ♯ ‘ 𝑒 ) ) = ( 2 · ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) ) ) |
| 18 | 14 17 | eqeq12d | ⊢ ( ( 𝑘 = ( Vtx ‘ 𝐺 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → ( Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ↔ Σ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) ) ) ) |
| 19 | 9 18 | imbi12d | ⊢ ( ( 𝑘 = ( Vtx ‘ 𝐺 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → ( ( 𝑒 ∈ Fin → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) ↔ ( ( iEdg ‘ 𝐺 ) ∈ Fin → Σ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) ) ) ) ) |
| 20 | eleq1 | ⊢ ( 𝑒 = 𝑓 → ( 𝑒 ∈ Fin ↔ 𝑓 ∈ Fin ) ) | |
| 21 | 20 | adantl | ⊢ ( ( 𝑘 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝑒 ∈ Fin ↔ 𝑓 ∈ Fin ) ) |
| 22 | simpl | ⊢ ( ( 𝑘 = 𝑤 ∧ 𝑒 = 𝑓 ) → 𝑘 = 𝑤 ) | |
| 23 | oveq12 | ⊢ ( ( 𝑘 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝑘 VtxDeg 𝑒 ) = ( 𝑤 VtxDeg 𝑓 ) ) | |
| 24 | df-ov | ⊢ ( 𝑤 VtxDeg 𝑓 ) = ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) | |
| 25 | 23 24 | eqtrdi | ⊢ ( ( 𝑘 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝑘 VtxDeg 𝑒 ) = ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) ) |
| 26 | 25 | fveq1d | ⊢ ( ( 𝑘 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) ‘ 𝑣 ) ) |
| 27 | 26 | adantr | ⊢ ( ( ( 𝑘 = 𝑤 ∧ 𝑒 = 𝑓 ) ∧ 𝑣 ∈ 𝑘 ) → ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) ‘ 𝑣 ) ) |
| 28 | 22 27 | sumeq12dv | ⊢ ( ( 𝑘 = 𝑤 ∧ 𝑒 = 𝑓 ) → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = Σ 𝑣 ∈ 𝑤 ( ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) ‘ 𝑣 ) ) |
| 29 | fveq2 | ⊢ ( 𝑒 = 𝑓 → ( ♯ ‘ 𝑒 ) = ( ♯ ‘ 𝑓 ) ) | |
| 30 | 29 | oveq2d | ⊢ ( 𝑒 = 𝑓 → ( 2 · ( ♯ ‘ 𝑒 ) ) = ( 2 · ( ♯ ‘ 𝑓 ) ) ) |
| 31 | 30 | adantl | ⊢ ( ( 𝑘 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 2 · ( ♯ ‘ 𝑒 ) ) = ( 2 · ( ♯ ‘ 𝑓 ) ) ) |
| 32 | 28 31 | eqeq12d | ⊢ ( ( 𝑘 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ↔ Σ 𝑣 ∈ 𝑤 ( ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑓 ) ) ) ) |
| 33 | 21 32 | imbi12d | ⊢ ( ( 𝑘 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( ( 𝑒 ∈ Fin → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) ↔ ( 𝑓 ∈ Fin → Σ 𝑣 ∈ 𝑤 ( ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑓 ) ) ) ) ) |
| 34 | vex | ⊢ 𝑘 ∈ V | |
| 35 | vex | ⊢ 𝑒 ∈ V | |
| 36 | 34 35 | opvtxfvi | ⊢ ( Vtx ‘ ⟨ 𝑘 , 𝑒 ⟩ ) = 𝑘 |
| 37 | 36 | eqcomi | ⊢ 𝑘 = ( Vtx ‘ ⟨ 𝑘 , 𝑒 ⟩ ) |
| 38 | eqid | ⊢ ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) = ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) | |
| 39 | eqid | ⊢ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } = { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } | |
| 40 | eqid | ⊢ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ = ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ | |
| 41 | 37 38 39 40 | upgrres | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘 ) → ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ∈ UPGraph ) |
| 42 | eleq1 | ⊢ ( 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) → ( 𝑓 ∈ Fin ↔ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ Fin ) ) | |
| 43 | 42 | adantl | ⊢ ( ( 𝑤 = ( 𝑘 ∖ { 𝑛 } ) ∧ 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) → ( 𝑓 ∈ Fin ↔ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ Fin ) ) |
| 44 | simpl | ⊢ ( ( 𝑤 = ( 𝑘 ∖ { 𝑛 } ) ∧ 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) → 𝑤 = ( 𝑘 ∖ { 𝑛 } ) ) | |
| 45 | opeq12 | ⊢ ( ( 𝑤 = ( 𝑘 ∖ { 𝑛 } ) ∧ 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) → ⟨ 𝑤 , 𝑓 ⟩ = ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) | |
| 46 | 45 | fveq2d | ⊢ ( ( 𝑤 = ( 𝑘 ∖ { 𝑛 } ) ∧ 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) → ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) = ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ) |
| 47 | 46 | fveq1d | ⊢ ( ( 𝑤 = ( 𝑘 ∖ { 𝑛 } ) ∧ 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) → ( ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) ‘ 𝑣 ) = ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) ) |
| 48 | 47 | adantr | ⊢ ( ( ( 𝑤 = ( 𝑘 ∖ { 𝑛 } ) ∧ 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ∧ 𝑣 ∈ 𝑤 ) → ( ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) ‘ 𝑣 ) = ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) ) |
| 49 | 44 48 | sumeq12dv | ⊢ ( ( 𝑤 = ( 𝑘 ∖ { 𝑛 } ) ∧ 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) → Σ 𝑣 ∈ 𝑤 ( ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) ‘ 𝑣 ) = Σ 𝑣 ∈ ( 𝑘 ∖ { 𝑛 } ) ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) ) |
| 50 | fveq2 | ⊢ ( 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) | |
| 51 | 50 | oveq2d | ⊢ ( 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) → ( 2 · ( ♯ ‘ 𝑓 ) ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) |
| 52 | 51 | adantl | ⊢ ( ( 𝑤 = ( 𝑘 ∖ { 𝑛 } ) ∧ 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) → ( 2 · ( ♯ ‘ 𝑓 ) ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) |
| 53 | 49 52 | eqeq12d | ⊢ ( ( 𝑤 = ( 𝑘 ∖ { 𝑛 } ) ∧ 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) → ( Σ 𝑣 ∈ 𝑤 ( ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑓 ) ) ↔ Σ 𝑣 ∈ ( 𝑘 ∖ { 𝑛 } ) ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) ) |
| 54 | 43 53 | imbi12d | ⊢ ( ( 𝑤 = ( 𝑘 ∖ { 𝑛 } ) ∧ 𝑓 = ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) → ( ( 𝑓 ∈ Fin → Σ 𝑣 ∈ 𝑤 ( ( VtxDeg ‘ ⟨ 𝑤 , 𝑓 ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑓 ) ) ) ↔ ( ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ Fin → Σ 𝑣 ∈ ( 𝑘 ∖ { 𝑛 } ) ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) ) ) |
| 55 | hasheq0 | ⊢ ( 𝑘 ∈ V → ( ( ♯ ‘ 𝑘 ) = 0 ↔ 𝑘 = ∅ ) ) | |
| 56 | 55 | elv | ⊢ ( ( ♯ ‘ 𝑘 ) = 0 ↔ 𝑘 = ∅ ) |
| 57 | 2t0e0 | ⊢ ( 2 · 0 ) = 0 | |
| 58 | 57 | a1i | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑘 = ∅ ) → ( 2 · 0 ) = 0 ) |
| 59 | 34 35 | opiedgfvi | ⊢ ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) = 𝑒 |
| 60 | 59 | eqcomi | ⊢ 𝑒 = ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) |
| 61 | upgruhgr | ⊢ ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph → ⟨ 𝑘 , 𝑒 ⟩ ∈ UHGraph ) | |
| 62 | 61 | adantr | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑘 = ∅ ) → ⟨ 𝑘 , 𝑒 ⟩ ∈ UHGraph ) |
| 63 | 37 | eqeq1i | ⊢ ( 𝑘 = ∅ ↔ ( Vtx ‘ ⟨ 𝑘 , 𝑒 ⟩ ) = ∅ ) |
| 64 | uhgr0vb | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ ( Vtx ‘ ⟨ 𝑘 , 𝑒 ⟩ ) = ∅ ) → ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UHGraph ↔ ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) = ∅ ) ) | |
| 65 | 63 64 | sylan2b | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑘 = ∅ ) → ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UHGraph ↔ ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) = ∅ ) ) |
| 66 | 62 65 | mpbid | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑘 = ∅ ) → ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) = ∅ ) |
| 67 | 60 66 | eqtrid | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑘 = ∅ ) → 𝑒 = ∅ ) |
| 68 | hasheq0 | ⊢ ( 𝑒 ∈ V → ( ( ♯ ‘ 𝑒 ) = 0 ↔ 𝑒 = ∅ ) ) | |
| 69 | 68 | elv | ⊢ ( ( ♯ ‘ 𝑒 ) = 0 ↔ 𝑒 = ∅ ) |
| 70 | 67 69 | sylibr | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑘 = ∅ ) → ( ♯ ‘ 𝑒 ) = 0 ) |
| 71 | 70 | oveq2d | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑘 = ∅ ) → ( 2 · ( ♯ ‘ 𝑒 ) ) = ( 2 · 0 ) ) |
| 72 | sumeq1 | ⊢ ( 𝑘 = ∅ → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = Σ 𝑣 ∈ ∅ ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) ) | |
| 73 | sum0 | ⊢ Σ 𝑣 ∈ ∅ ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = 0 | |
| 74 | 72 73 | eqtrdi | ⊢ ( 𝑘 = ∅ → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = 0 ) |
| 75 | 74 | adantl | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑘 = ∅ ) → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = 0 ) |
| 76 | 58 71 75 | 3eqtr4rd | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑘 = ∅ ) → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) |
| 77 | 56 76 | sylan2b | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ ( ♯ ‘ 𝑘 ) = 0 ) → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) |
| 78 | 77 | a1d | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ ( ♯ ‘ 𝑘 ) = 0 ) → ( 𝑒 ∈ Fin → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) ) |
| 79 | eleq1 | ⊢ ( ( 𝑦 + 1 ) = ( ♯ ‘ 𝑘 ) → ( ( 𝑦 + 1 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑘 ) ∈ ℕ0 ) ) | |
| 80 | 79 | eqcoms | ⊢ ( ( ♯ ‘ 𝑘 ) = ( 𝑦 + 1 ) → ( ( 𝑦 + 1 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑘 ) ∈ ℕ0 ) ) |
| 81 | 80 | 3ad2ant2 | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ ( ♯ ‘ 𝑘 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑘 ) → ( ( 𝑦 + 1 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑘 ) ∈ ℕ0 ) ) |
| 82 | hashclb | ⊢ ( 𝑘 ∈ V → ( 𝑘 ∈ Fin ↔ ( ♯ ‘ 𝑘 ) ∈ ℕ0 ) ) | |
| 83 | 82 | biimprd | ⊢ ( 𝑘 ∈ V → ( ( ♯ ‘ 𝑘 ) ∈ ℕ0 → 𝑘 ∈ Fin ) ) |
| 84 | 83 | elv | ⊢ ( ( ♯ ‘ 𝑘 ) ∈ ℕ0 → 𝑘 ∈ Fin ) |
| 85 | eqid | ⊢ ( 𝑘 ∖ { 𝑛 } ) = ( 𝑘 ∖ { 𝑛 } ) | |
| 86 | eqid | ⊢ { 𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ( 𝑒 ‘ 𝑖 ) } = { 𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ( 𝑒 ‘ 𝑖 ) } | |
| 87 | 59 | dmeqi | ⊢ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) = dom 𝑒 |
| 88 | 87 | rabeqi | ⊢ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } = { 𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } |
| 89 | eqidd | ⊢ ( 𝑖 ∈ dom 𝑒 → 𝑛 = 𝑛 ) | |
| 90 | 59 | a1i | ⊢ ( 𝑖 ∈ dom 𝑒 → ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) = 𝑒 ) |
| 91 | 90 | fveq1d | ⊢ ( 𝑖 ∈ dom 𝑒 → ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) = ( 𝑒 ‘ 𝑖 ) ) |
| 92 | 89 91 | neleq12d | ⊢ ( 𝑖 ∈ dom 𝑒 → ( 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) ↔ 𝑛 ∉ ( 𝑒 ‘ 𝑖 ) ) ) |
| 93 | 92 | rabbiia | ⊢ { 𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } = { 𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ( 𝑒 ‘ 𝑖 ) } |
| 94 | 88 93 | eqtri | ⊢ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } = { 𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ( 𝑒 ‘ 𝑖 ) } |
| 95 | 59 94 | reseq12i | ⊢ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) = ( 𝑒 ↾ { 𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ( 𝑒 ‘ 𝑖 ) } ) |
| 96 | 37 60 85 86 95 40 | finsumvtxdg2sstep | ⊢ ( ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘 ) ∧ ( 𝑘 ∈ Fin ∧ 𝑒 ∈ Fin ) ) → ( ( ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ Fin → Σ 𝑣 ∈ ( 𝑘 ∖ { 𝑛 } ) ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) → Σ 𝑣 ∈ 𝑘 ( ( VtxDeg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) ) |
| 97 | df-ov | ⊢ ( 𝑘 VtxDeg 𝑒 ) = ( VtxDeg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) | |
| 98 | 97 | fveq1i | ⊢ ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( ( VtxDeg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑣 ) |
| 99 | 98 | a1i | ⊢ ( 𝑣 ∈ 𝑘 → ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( ( VtxDeg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑣 ) ) |
| 100 | 99 | sumeq2i | ⊢ Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = Σ 𝑣 ∈ 𝑘 ( ( VtxDeg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑣 ) |
| 101 | 100 | eqeq1i | ⊢ ( Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ↔ Σ 𝑣 ∈ 𝑘 ( ( VtxDeg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) |
| 102 | 96 101 | syl6ibr | ⊢ ( ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘 ) ∧ ( 𝑘 ∈ Fin ∧ 𝑒 ∈ Fin ) ) → ( ( ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ Fin → Σ 𝑣 ∈ ( 𝑘 ∖ { 𝑛 } ) ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) ) |
| 103 | 102 | exp32 | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘 ) → ( 𝑘 ∈ Fin → ( 𝑒 ∈ Fin → ( ( ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ Fin → Σ 𝑣 ∈ ( 𝑘 ∖ { 𝑛 } ) ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) ) ) ) |
| 104 | 103 | com34 | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘 ) → ( 𝑘 ∈ Fin → ( ( ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ Fin → Σ 𝑣 ∈ ( 𝑘 ∖ { 𝑛 } ) ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) → ( 𝑒 ∈ Fin → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) ) ) ) |
| 105 | 104 | 3adant2 | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ ( ♯ ‘ 𝑘 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑘 ) → ( 𝑘 ∈ Fin → ( ( ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ Fin → Σ 𝑣 ∈ ( 𝑘 ∖ { 𝑛 } ) ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) → ( 𝑒 ∈ Fin → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) ) ) ) |
| 106 | 84 105 | syl5 | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ ( ♯ ‘ 𝑘 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑘 ) → ( ( ♯ ‘ 𝑘 ) ∈ ℕ0 → ( ( ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ Fin → Σ 𝑣 ∈ ( 𝑘 ∖ { 𝑛 } ) ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) → ( 𝑒 ∈ Fin → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) ) ) ) |
| 107 | 81 106 | sylbid | ⊢ ( ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ ( ♯ ‘ 𝑘 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑘 ) → ( ( 𝑦 + 1 ) ∈ ℕ0 → ( ( ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ Fin → Σ 𝑣 ∈ ( 𝑘 ∖ { 𝑛 } ) ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) → ( 𝑒 ∈ Fin → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) ) ) ) |
| 108 | 107 | impcom | ⊢ ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ ( ♯ ‘ 𝑘 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑘 ) ) → ( ( ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ Fin → Σ 𝑣 ∈ ( 𝑘 ∖ { 𝑛 } ) ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) → ( 𝑒 ∈ Fin → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) ) ) |
| 109 | 108 | imp | ⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑘 , 𝑒 ⟩ ∈ UPGraph ∧ ( ♯ ‘ 𝑘 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑘 ) ) ∧ ( ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ∈ Fin → Σ 𝑣 ∈ ( 𝑘 ∖ { 𝑛 } ) ( ( VtxDeg ‘ ⟨ ( 𝑘 ∖ { 𝑛 } ) , ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ⟩ ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ↾ { 𝑖 ∈ dom ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ∣ 𝑛 ∉ ( ( iEdg ‘ ⟨ 𝑘 , 𝑒 ⟩ ) ‘ 𝑖 ) } ) ) ) ) ) → ( 𝑒 ∈ Fin → Σ 𝑣 ∈ 𝑘 ( ( 𝑘 VtxDeg 𝑒 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑒 ) ) ) ) |
| 110 | 5 7 19 33 41 54 78 109 | opfi1ind | ⊢ ( ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) → ( ( iEdg ‘ 𝐺 ) ∈ Fin → Σ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) ) ) ) |
| 111 | 110 | ex | ⊢ ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph → ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( ( iEdg ‘ 𝐺 ) ∈ Fin → Σ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) ) ) ) ) |
| 112 | 4 111 | syl | ⊢ ( 𝐺 ∈ UPGraph → ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( ( iEdg ‘ 𝐺 ) ∈ Fin → Σ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) ) ) ) ) |
| 113 | 1 | eleq1i | ⊢ ( 𝑉 ∈ Fin ↔ ( Vtx ‘ 𝐺 ) ∈ Fin ) |
| 114 | 113 | a1i | ⊢ ( 𝐺 ∈ UPGraph → ( 𝑉 ∈ Fin ↔ ( Vtx ‘ 𝐺 ) ∈ Fin ) ) |
| 115 | 2 | eleq1i | ⊢ ( 𝐼 ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) |
| 116 | 115 | a1i | ⊢ ( 𝐺 ∈ UPGraph → ( 𝐼 ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) ) |
| 117 | 1 | a1i | ⊢ ( 𝐺 ∈ UPGraph → 𝑉 = ( Vtx ‘ 𝐺 ) ) |
| 118 | vtxdgop | ⊢ ( 𝐺 ∈ UPGraph → ( VtxDeg ‘ 𝐺 ) = ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ) | |
| 119 | 3 118 | eqtrid | ⊢ ( 𝐺 ∈ UPGraph → 𝐷 = ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ) |
| 120 | 119 | fveq1d | ⊢ ( 𝐺 ∈ UPGraph → ( 𝐷 ‘ 𝑣 ) = ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) ) |
| 121 | 120 | adantr | ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑣 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑣 ) = ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) ) |
| 122 | 117 121 | sumeq12dv | ⊢ ( 𝐺 ∈ UPGraph → Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = Σ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) ) |
| 123 | 2 | fveq2i | ⊢ ( ♯ ‘ 𝐼 ) = ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) |
| 124 | 123 | oveq2i | ⊢ ( 2 · ( ♯ ‘ 𝐼 ) ) = ( 2 · ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) ) |
| 125 | 124 | a1i | ⊢ ( 𝐺 ∈ UPGraph → ( 2 · ( ♯ ‘ 𝐼 ) ) = ( 2 · ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) ) ) |
| 126 | 122 125 | eqeq12d | ⊢ ( 𝐺 ∈ UPGraph → ( Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐼 ) ) ↔ Σ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) ) ) ) |
| 127 | 116 126 | imbi12d | ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐼 ∈ Fin → Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐼 ) ) ) ↔ ( ( iEdg ‘ 𝐺 ) ∈ Fin → Σ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) ) ) ) ) |
| 128 | 112 114 127 | 3imtr4d | ⊢ ( 𝐺 ∈ UPGraph → ( 𝑉 ∈ Fin → ( 𝐼 ∈ Fin → Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐼 ) ) ) ) ) |
| 129 | 128 | 3imp | ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐼 ) ) ) |