This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem p1evtxdp1

Description: If an edge E (not being a loop) which contains vertex U is added to a graph G (yielding a graph F ), the degree of U is increased by 1. (Contributed by AV, 3-Mar-2021)

Ref Expression
Hypotheses p1evtxdeq.v ⊢ V = Vtx ⁡ G
p1evtxdeq.i ⊢ I = iEdg ⁡ G
p1evtxdeq.f ⊢ φ → Fun ⁡ I
p1evtxdeq.fv ⊢ φ → Vtx ⁡ F = V
p1evtxdeq.fi ⊢ φ → iEdg ⁡ F = I ∪ K E
p1evtxdeq.k ⊢ φ → K ∈ X
p1evtxdeq.d ⊢ φ → K ∉ dom ⁡ I
p1evtxdeq.u ⊢ φ → U ∈ V
p1evtxdp1.e ⊢ φ → E ∈ 𝒫 V
p1evtxdp1.n ⊢ φ → U ∈ E
p1evtxdp1.l ⊢ φ → 2 ≤ E
Assertion p1evtxdp1 ⊢ φ → VtxDeg ⁡ F ⁡ U = VtxDeg ⁡ G ⁡ U + 𝑒 1

Proof

Step Hyp Ref Expression
1 p1evtxdeq.v ⊢ V = Vtx ⁡ G
2 p1evtxdeq.i ⊢ I = iEdg ⁡ G
3 p1evtxdeq.f ⊢ φ → Fun ⁡ I
4 p1evtxdeq.fv ⊢ φ → Vtx ⁡ F = V
5 p1evtxdeq.fi ⊢ φ → iEdg ⁡ F = I ∪ K E
6 p1evtxdeq.k ⊢ φ → K ∈ X
7 p1evtxdeq.d ⊢ φ → K ∉ dom ⁡ I
8 p1evtxdeq.u ⊢ φ → U ∈ V
9 p1evtxdp1.e ⊢ φ → E ∈ 𝒫 V
10 p1evtxdp1.n ⊢ φ → U ∈ E
11 p1evtxdp1.l ⊢ φ → 2 ≤ E
12 1 2 3 4 5 6 7 8 9 p1evtxdeqlem ⊢ φ → VtxDeg ⁡ F ⁡ U = VtxDeg ⁡ G ⁡ U + 𝑒 VtxDeg ⁡ V K E ⁡ U
13 1 fvexi ⊢ V ∈ V
14 snex ⊢ K E ∈ V
15 13 14 pm3.2i ⊢ V ∈ V ∧ K E ∈ V
16 opiedgfv ⊢ V ∈ V ∧ K E ∈ V → iEdg ⁡ V K E = K E
17 15 16 mp1i ⊢ φ → iEdg ⁡ V K E = K E
18 opvtxfv ⊢ V ∈ V ∧ K E ∈ V → Vtx ⁡ V K E = V
19 15 18 mp1i ⊢ φ → Vtx ⁡ V K E = V
20 17 19 6 8 9 10 11 1hevtxdg1 ⊢ φ → VtxDeg ⁡ V K E ⁡ U = 1
21 20 oveq2d ⊢ φ → VtxDeg ⁡ G ⁡ U + 𝑒 VtxDeg ⁡ V K E ⁡ U = VtxDeg ⁡ G ⁡ U + 𝑒 1
22 12 21 eqtrd ⊢ φ → VtxDeg ⁡ F ⁡ U = VtxDeg ⁡ G ⁡ U + 𝑒 1