Metamath Proof Explorer


Theorem p1evtxdeqlem

Description: Lemma for p1evtxdeq and p1evtxdp1 . (Contributed by AV, 3-Mar-2021)

Ref Expression
Hypotheses p1evtxdeq.v V=VtxG
p1evtxdeq.i I=iEdgG
p1evtxdeq.f φFunI
p1evtxdeq.fv φVtxF=V
p1evtxdeq.fi φiEdgF=IKE
p1evtxdeq.k φKX
p1evtxdeq.d φKdomI
p1evtxdeq.u φUV
p1evtxdeq.e φEY
Assertion p1evtxdeqlem φVtxDegFU=VtxDegGU+𝑒VtxDegVKEU

Proof

Step Hyp Ref Expression
1 p1evtxdeq.v V=VtxG
2 p1evtxdeq.i I=iEdgG
3 p1evtxdeq.f φFunI
4 p1evtxdeq.fv φVtxF=V
5 p1evtxdeq.fi φiEdgF=IKE
6 p1evtxdeq.k φKX
7 p1evtxdeq.d φKdomI
8 p1evtxdeq.u φUV
9 p1evtxdeq.e φEY
10 1 fvexi VV
11 snex KEV
12 10 11 pm3.2i VVKEV
13 opiedgfv VVKEViEdgVKE=KE
14 13 eqcomd VVKEVKE=iEdgVKE
15 12 14 ax-mp KE=iEdgVKE
16 opvtxfv VVKEVVtxVKE=V
17 12 16 mp1i φVtxVKE=V
18 dmsnopg EYdomKE=K
19 9 18 syl φdomKE=K
20 19 ineq2d φdomIdomKE=domIK
21 df-nel KdomI¬KdomI
22 7 21 sylib φ¬KdomI
23 disjsn domIK=¬KdomI
24 22 23 sylibr φdomIK=
25 20 24 eqtrd φdomIdomKE=
26 funsng KXEYFunKE
27 6 9 26 syl2anc φFunKE
28 2 15 1 17 4 25 3 27 8 5 vtxdun φVtxDegFU=VtxDegGU+𝑒VtxDegVKEU