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=\mathrm{Vtx}\left(G\right)$$
	p1evtxdeq.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	p1evtxdeq.f	$$⊢\phi \to \mathrm{Fun}I$$
	p1evtxdeq.fv	$$⊢\phi \to \mathrm{Vtx}\left(F\right)=V$$
	p1evtxdeq.fi	$$⊢\phi \to \mathrm{iEdg}\left(F\right)=I\cup \left\{⟨K,E⟩\right\}$$
	p1evtxdeq.k	$$⊢\phi \to K\in X$$
	p1evtxdeq.d	$$⊢\phi \to K\notin \mathrm{dom}I$$
	p1evtxdeq.u	$$⊢\phi \to U\in V$$
	p1evtxdp1.e	$$⊢\phi \to E\in 𝒫V$$
	p1evtxdp1.n	$$⊢\phi \to U\in E$$
	p1evtxdp1.l	$$⊢\phi \to 2\le \left|E\right|$$
Assertion	p1evtxdp1	$$⊢\phi \to \mathrm{VtxDeg}\left(F\right)\left(U\right)=\mathrm{VtxDeg}\left(G\right)\left(U\right){+}_{𝑒}1$$

Proof

Step	Hyp	Ref	Expression
1		p1evtxdeq.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		p1evtxdeq.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		p1evtxdeq.f	$$⊢\phi \to \mathrm{Fun}I$$
4		p1evtxdeq.fv	$$⊢\phi \to \mathrm{Vtx}\left(F\right)=V$$
5		p1evtxdeq.fi	$$⊢\phi \to \mathrm{iEdg}\left(F\right)=I\cup \left\{⟨K,E⟩\right\}$$
6		p1evtxdeq.k	$$⊢\phi \to K\in X$$
7		p1evtxdeq.d	$$⊢\phi \to K\notin \mathrm{dom}I$$
8		p1evtxdeq.u	$$⊢\phi \to U\in V$$
9		p1evtxdp1.e	$$⊢\phi \to E\in 𝒫V$$
10		p1evtxdp1.n	$$⊢\phi \to U\in E$$
11		p1evtxdp1.l	$$⊢\phi \to 2\le \left|E\right|$$
12	1 2 3 4 5 6 7 8 9	p1evtxdeqlem	$$⊢\phi \to \mathrm{VtxDeg}\left(F\right)\left(U\right)=\mathrm{VtxDeg}\left(G\right)\left(U\right){+}_{𝑒}\mathrm{VtxDeg}\left(⟨V,\left\{⟨K,E⟩\right\}⟩\right)\left(U\right)$$
13	1	fvexi	$$⊢V\in \mathrm{V}$$
14		snex	$$⊢\left\{⟨K,E⟩\right\}\in \mathrm{V}$$
15	13 14	pm3.2i	$$⊢\left(V\in \mathrm{V}\wedge \left\{⟨K,E⟩\right\}\in \mathrm{V}\right)$$
16		opiedgfv	$$⊢\left(V\in \mathrm{V}\wedge \left\{⟨K,E⟩\right\}\in \mathrm{V}\right)\to \mathrm{iEdg}\left(⟨V,\left\{⟨K,E⟩\right\}⟩\right)=\left\{⟨K,E⟩\right\}$$
17	15 16	mp1i	$$⊢\phi \to \mathrm{iEdg}\left(⟨V,\left\{⟨K,E⟩\right\}⟩\right)=\left\{⟨K,E⟩\right\}$$
18		opvtxfv	$$⊢\left(V\in \mathrm{V}\wedge \left\{⟨K,E⟩\right\}\in \mathrm{V}\right)\to \mathrm{Vtx}\left(⟨V,\left\{⟨K,E⟩\right\}⟩\right)=V$$
19	15 18	mp1i	$$⊢\phi \to \mathrm{Vtx}\left(⟨V,\left\{⟨K,E⟩\right\}⟩\right)=V$$
20	17 19 6 8 9 10 11	1hevtxdg1	$$⊢\phi \to \mathrm{VtxDeg}\left(⟨V,\left\{⟨K,E⟩\right\}⟩\right)\left(U\right)=1$$
21	20	oveq2d	$$⊢\phi \to \mathrm{VtxDeg}\left(G\right)\left(U\right){+}_{𝑒}\mathrm{VtxDeg}\left(⟨V,\left\{⟨K,E⟩\right\}⟩\right)\left(U\right)=\mathrm{VtxDeg}\left(G\right)\left(U\right){+}_{𝑒}1$$
22	12 21	eqtrd	$$⊢\phi \to \mathrm{VtxDeg}\left(F\right)\left(U\right)=\mathrm{VtxDeg}\left(G\right)\left(U\right){+}_{𝑒}1$$