Metamath Proof Explorer

Theorem finsumvtxdg2ssteplem2

Description: Lemma for finsumvtxdg2sstep . (Contributed by AV, 12-Dec-2021)

Ref Expression
Hypotheses finsumvtxdg2sstep.v ⊢V=Vtx⁡G
finsumvtxdg2sstep.e ⊢E=iEdg⁡G
finsumvtxdg2sstep.k ⊢K=V∖N
finsumvtxdg2sstep.i ⊢I=i∈dom⁡E|N∉E⁡i
finsumvtxdg2sstep.p ⊢P=E↾I
finsumvtxdg2sstep.s ⊢S=KP
finsumvtxdg2ssteplem.j ⊢J=i∈dom⁡E|N∈E⁡i
Assertion finsumvtxdg2ssteplem2 ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→VtxDeg⁡G⁡N=J+i∈dom⁡E|E⁡i=N

Proof

Step Hyp Ref Expression
1 finsumvtxdg2sstep.v ⊢V=Vtx⁡G
2 finsumvtxdg2sstep.e ⊢E=iEdg⁡G
3 finsumvtxdg2sstep.k ⊢K=V∖N
4 finsumvtxdg2sstep.i ⊢I=i∈dom⁡E|N∉E⁡i
5 finsumvtxdg2sstep.p ⊢P=E↾I
6 finsumvtxdg2sstep.s ⊢S=KP
7 finsumvtxdg2ssteplem.j ⊢J=i∈dom⁡E|N∈E⁡i
8 dmfi ⊢E∈Fin→dom⁡E∈Fin
9 8 adantl ⊢V∈Fin∧E∈Fin→dom⁡E∈Fin
10 simpr ⊢G∈UPGraph∧N∈V→N∈V
11 eqid ⊢dom⁡E=dom⁡E
12 1 2 11 vtxdgfival ⊢dom⁡E∈Fin∧N∈V→VtxDeg⁡G⁡N=i∈dom⁡E|N∈E⁡i+i∈dom⁡E|E⁡i=N
13 9 10 12 syl2anr ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→VtxDeg⁡G⁡N=i∈dom⁡E|N∈E⁡i+i∈dom⁡E|E⁡i=N
14 7 eqcomi ⊢i∈dom⁡E|N∈E⁡i=J
15 14 fveq2i ⊢i∈dom⁡E|N∈E⁡i=J
16 15 a1i ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→i∈dom⁡E|N∈E⁡i=J
17 16 oveq1d ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→i∈dom⁡E|N∈E⁡i+i∈dom⁡E|E⁡i=N=J+i∈dom⁡E|E⁡i=N
18 13 17 eqtrd ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→VtxDeg⁡G⁡N=J+i∈dom⁡E|E⁡i=N