Metamath Proof Explorer


Theorem vdegp1ci

Description: The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of U in the edge set E is P , then adding { X , U } to the edge set, where X =/= U , yields degree P + 1 . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 28-Feb-2016) (Revised by AV, 3-Mar-2021)

Ref Expression
Hypotheses vdegp1ai.vg V = Vtx G
vdegp1ai.u U V
vdegp1ai.i I = iEdg G
vdegp1ai.w I Word x 𝒫 V | x 2
vdegp1ai.d VtxDeg G U = P
vdegp1ai.vf Vtx F = V
vdegp1bi.x X V
vdegp1bi.xu X U
vdegp1ci.f iEdg F = I ++ ⟨“ X U ”⟩
Assertion vdegp1ci VtxDeg F U = P + 1

Proof

Step Hyp Ref Expression
1 vdegp1ai.vg V = Vtx G
2 vdegp1ai.u U V
3 vdegp1ai.i I = iEdg G
4 vdegp1ai.w I Word x 𝒫 V | x 2
5 vdegp1ai.d VtxDeg G U = P
6 vdegp1ai.vf Vtx F = V
7 vdegp1bi.x X V
8 vdegp1bi.xu X U
9 vdegp1ci.f iEdg F = I ++ ⟨“ X U ”⟩
10 prcom X U = U X
11 s1eq X U = U X ⟨“ X U ”⟩ = ⟨“ U X ”⟩
12 10 11 ax-mp ⟨“ X U ”⟩ = ⟨“ U X ”⟩
13 12 oveq2i I ++ ⟨“ X U ”⟩ = I ++ ⟨“ U X ”⟩
14 9 13 eqtri iEdg F = I ++ ⟨“ U X ”⟩
15 1 2 3 4 5 6 7 8 14 vdegp1bi VtxDeg F U = P + 1