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 = K P
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 = K P
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